From: Andrea Asperti Date: Mon, 17 Sep 2007 13:27:41 +0000 (+0000) Subject: Some new lemmas. X-Git-Tag: 0.4.95@7852~160 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=64c3512c9af4f7120c23722f7cf21146ce3e3bae;p=helm.git Some new lemmas. --- diff --git a/matita/library/datatypes/bool.ma b/matita/library/datatypes/bool.ma index 3292e6789..b5abbb35d 100644 --- a/matita/library/datatypes/bool.ma +++ b/matita/library/datatypes/bool.ma @@ -78,6 +78,14 @@ reflexivity. assumption. qed. +theorem andb_true_true_r: \forall b1,b2. (b1 \land b2) = true \to b2 = true. +intro. elim b1 + [assumption + |apply False_ind.apply not_eq_true_false. + apply sym_eq.assumption + ] +qed. + definition orb : bool \to bool \to bool\def \lambda b1,b2:bool. match b1 with @@ -123,4 +131,43 @@ theorem P_x_to_P_x_to_eq: intros. apply eq_to_eq_to_eq_p_q. exact bool_to_decidable_eq. -qed. +qed. + + +(* some basic properties of and - or*) +theorem andb_sym: \forall A,B:bool. +(A \land B) = (B \land A). +intros. +elim A; + elim B; + simplify; + reflexivity. +qed. + +theorem andb_assoc: \forall A,B,C:bool. +(A \land (B \land C)) = ((A \land B) \land C). +intros. +elim A; + elim B; + elim C; + simplify; + reflexivity. +qed. + +theorem orb_sym: \forall A,B:bool. +(A \lor B) = (B \lor A). +intros. +elim A; + elim B; + simplify; + reflexivity. +qed. + +theorem andb_t_t_t: \forall A,B,C:bool. +A = true \to B = true \to C = true \to (A \land (B \land C)) = true. +intros. +rewrite > H. +rewrite > H1. +rewrite > H2. +reflexivity. +qed. \ No newline at end of file