From 69dc6031c9e0574fa7a74ced74deeb7f9ec5695b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 2 Nov 2005 18:43:09 +0000 Subject: [PATCH] Proof of unicity of proofs for: 1. decidable equalities 2. P x = true for some function P --- helm/matita/library/datatypes/bool.ma | 23 ++++ helm/matita/library/logic/connectives.ma | 16 ++- helm/matita/library/logic/equality.ma | 128 +++++++++++++++++++++++ 3 files changed, 166 insertions(+), 1 deletion(-) diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index a223d7d0c..a4667da30 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -84,3 +84,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. diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma index a8cba2b4a..2848c08c5 100644 --- a/helm/matita/library/logic/connectives.ma +++ b/helm/matita/library/logic/connectives.ma @@ -56,7 +56,21 @@ inductive Or (A,B:Prop) : Prop \def (*CSC: the URI must disappear: there is a bug now *) interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y). - + +theorem Or_ind': + \forall A,B:Prop. + \forall P: A \lor B \to Prop. + (\forall p:A. P (or_introl ? ? p)) \to + (\forall q:B. P (or_intror ? ? q)) \to + \forall p:A \lor B. P p. + intros. + apply + ([\lambda p.P p] + match p with + [(or_introl p) \Rightarrow H p + |(or_intror q) \Rightarrow H1 q]). +qed. + definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \lnot A. inductive ex (A:Type) (P:A \to Prop) : Prop \def diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index ed257afa4..70ade5589 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -27,6 +27,16 @@ interpretation "leibnitz's non-equality" 'neq x y = (cic:/matita/logic/connectives/Not.con (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)). +theorem eq_ind': + \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Prop. + P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p. + intros. + exact + ([\lambda y:A. \lambda p:eq A x y.P y p] + match p with + [refl_eq \Rightarrow H]). +qed. + theorem reflexive_eq : \forall A:Type. reflexive A (eq A). simplify.intros.apply refl_eq. qed. @@ -69,6 +79,124 @@ x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2. intros.elim H1.elim H.reflexivity. qed. +definition comp \def + \lambda A. + \lambda x,y,y':A. + \lambda eq1:x=y. + \lambda eq2:x=y'. + eq_ind ? ? (\lambda a.a=y') eq2 ? eq1. + +lemma trans_sym_eq: + \forall A. + \forall x,y:A. + \forall u:x=y. + comp ? ? ? ? u u = refl_eq ? y. + intros. + apply (eq_ind' ? ? ? ? ? u). + reflexivity. +qed. + +definition nu \def + \lambda A. + \lambda H: \forall x,y:A. decidable (x=y). + \lambda x,y. \lambda p:x=y. + match H x y with + [ (or_introl p') \Rightarrow p' + | (or_intror K) \Rightarrow False_ind ? (K p) ]. + +theorem nu_constant: + \forall A. + \forall H: \forall x,y:A. decidable (x=y). + \forall x,y:A. + \forall u,v:x=y. + nu ? H ? ? u = nu ? H ? ? v. + intros. + unfold nu. + unfold decidable in H. + apply (Or_ind' ? ? ? ? ? (H x y)); simplify. + intro; reflexivity. + intro; elim (q u). +qed. + +definition nu_inv \def + \lambda A. + \lambda H: \forall x,y:A. decidable (x=y). + \lambda x,y:A. + \lambda v:x=y. + comp ? ? ? ? (nu ? H ? ? (refl_eq ? x)) v. + +theorem nu_left_inv: + \forall A. + \forall H: \forall x,y:A. decidable (x=y). + \forall x,y:A. + \forall u:x=y. + nu_inv ? H ? ? (nu ? H ? ? u) = u. + intros. + apply (eq_ind' ? ? ? ? ? u). + unfold nu_inv. + apply trans_sym_eq. +qed. + +theorem eq_to_eq_to_eq_p_q: + \forall A. \forall x,y:A. + (\forall x,y:A. decidable (x=y)) \to + \forall p,q:x=y. p=q. + intros. + rewrite < (nu_left_inv ? H ? ? p). + rewrite < (nu_left_inv ? H ? ? q). + elim (nu_constant ? H ? ? q). + reflexivity. +qed. + +(*CSC: alternative proof that does not pollute the environment with + technical lemmata. Unfortunately, it is a pain to do without proper + support for let-ins. +theorem eq_to_eq_to_eq_p_q: + \forall A. \forall x,y:A. + (\forall x,y:A. decidable (x=y)) \to + \forall p,q:x=y. p=q. +intros. +letin nu \def + (\lambda x,y. \lambda p:x=y. + match H x y with + [ (or_introl p') \Rightarrow p' + | (or_intror K) \Rightarrow False_ind ? (K p) ]). +cut + (\forall q:x=y. + eq_ind ? ? (\lambda z. z=y) (nu ? ? q) ? (nu ? ? (refl_eq ? x)) + = q). +focus 8. + clear q; clear p. + intro. + apply (eq_ind' ? ? ? ? ? q); + fold simplify (nu ? ? (refl_eq ? x)). + generalize in match (nu ? ? (refl_eq ? x)); intro. + apply + (eq_ind' A x + (\lambda y. \lambda u. + eq_ind A x (\lambda a.a=y) u y u = refl_eq ? y) + ? x H1). + reflexivity. +unfocus. +rewrite < (Hcut p); fold simplify (nu ? ? p). +rewrite < (Hcut q); fold simplify (nu ? ? q). +apply (Or_ind' (x=x) (x \neq x) + (\lambda p:decidable (x=x). eq_ind A x (\lambda z.z=y) (nu x y p) x + ([\lambda H1.eq A x x] + match p with + [(or_introl p') \Rightarrow p' + |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))]) = + eq_ind A x (\lambda z.z=y) (nu x y q) x + ([\lambda H1.eq A x x] + match p with + [(or_introl p') \Rightarrow p' + |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))])) + ? ? (H x x)). +intro; simplify; reflexivity. +intro q; elim (q (refl_eq ? x)). +qed. +*) + (* theorem a:\forall x.x=x\land True. [ -- 2.39.2