Logique.v
Require Export Bool.
Lemma
de_morgan1: (b1, b2:bool)(negb (orb b1 b2))=(andb (negb b1) (negb b2)).
Destruct b1; Destruct b2; Simpl; Auto.
Qed.
Lemma
de_morgan2: (b1, b2:bool)(negb (andb b1 b2))=(orb (negb b1) (negb b2)).
Destruct b1; Destruct b2; Simpl; Auto.
Qed.
Lemma
de_morgan3: (b1, b2:bool)(andb b1 b2)=(negb (orb (negb b1) (negb b2))).
Destruct b1; Destruct b2; Simpl; Reflexivity.
Qed.
Lemma
de_morgan4: (b1, b2:bool)(orb b1 b2)=(negb (andb (negb b1) (negb b2))).
Destruct b1; Destruct b2; Simpl; Reflexivity.
Qed.
Lemma
implb_b_true: (b:bool)(implb b true)=true.
Destruct b; Simpl; Auto.
Qed.
Lemma
implb_b_false: (b:bool)(implb b false)=(negb b).
Destruct b; Simpl; Auto.
Qed.
Lemma
implb_true_b: (b:bool)(implb true b)=b.
Destruct b; Simpl; Auto.
Qed.
Lemma
implb_false_b: (b:bool)(implb false b)=true.
Destruct b; Simpl; Auto.
Qed.
Lemma
implb_elim: (b1, b2:bool)(implb b1 b2)=(negb (andb b1 (negb b2))).
Destruct b1; Destruct b2; Simpl; Auto.
Qed.
Lemma
eqb_true_b: (b:bool)(eqb true b)=b.
Destruct b; Simpl; Auto.
Qed.
Lemma
eqb_b_true: (b:bool)(eqb b true)=b.
Destruct b; Simpl; Auto.
Qed.
Lemma
eqb_b_false: (b:bool)(eqb b false)=(negb b).
Destruct b; Simpl; Auto.
Qed.
Lemma
eqb_false_b: (b:bool)(eqb false b)=(negb b).
Destruct b; Simpl; Auto.
Qed.
Lemma
eqb_com: (b1, b2:bool)(eqb b1 b2)=(eqb b2 b1).
Destruct b1; Destruct b2; Simpl; Auto.
Qed.
Lemma
orb_false_1: (b, b':bool) (orb b b')=false ->b=false.
Intros b b'; Case b; Case b'; Auto; Absurd true=false; Auto.
Qed.
Lemma
orb_false_2: (b, b':bool) (orb b b')=false ->b'=false.
Intros b b'; Case b; Case b'; Auto; Absurd true=false; Auto.
Qed.
Hints Resolve de_morgan1 de_morgan2 de_morgan3 de_morgan4.
Hints Resolve implb_b_true implb_b_false implb_true_b implb_false_b implb_elim.
Hints Resolve eqb_true_b eqb_b_true eqb_b_false eqb_false_b eqb_com.
26/01/99, 11:04