X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fdatatypes%2Fbool.ma;h=f4aec8167476b0d88204a06d3d23aaa798a323ac;hb=c5e94d35e8f36f868c5a1f02d80a419bfe802ba1;hp=d99456dc89e1b02ee4522c26ee90cc5ab6930ded;hpb=03fcee16d9c262aad38a47d0a409b684a965cc3f;p=helm.git diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index d99456dc8..f4aec8167 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -19,9 +19,20 @@ include "logic/equality.ma". inductive bool : Set \def | true : bool | false : bool. - -theorem not_eq_true_false : \lnot true = false. -simplify.intro. + +theorem bool_elim: \forall P:bool \to Prop. \forall b:bool. + (b = true \to P true) + \to (b = false \to P false) + \to P b. + intros 2 (P b). + elim b; + [ apply H; reflexivity + | apply H1; reflexivity + ] +qed. + +theorem not_eq_true_false : true \neq false. +unfold Not.intro. change with match true with [ true \Rightarrow False @@ -84,3 +95,26 @@ match b with | false \Rightarrow Q]. (*CSC: missing notation for if_then_else *) + +theorem bool_to_decidable_eq: + \forall b1,b2:bool. decidable (b1=b2). + intros. + unfold decidable. + elim b1. + elim b2. + left. reflexivity. + right. exact not_eq_true_false. + elim b2. + right. unfold Not. intro. + apply not_eq_true_false. + symmetry. exact H. + left. reflexivity. +qed. + +theorem P_x_to_P_x_to_eq: + \forall A:Set. \forall P: A \to bool. + \forall x:A. \forall p1,p2:P x = true. p1 = p2. + intros. + apply eq_to_eq_to_eq_p_q. + exact bool_to_decidable_eq. +qed.