From: Andrea Asperti Date: Fri, 8 Jan 2010 08:17:37 +0000 (+0000) Subject: rebuilding the library X-Git-Tag: make_still_working~3140 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ffdcaed2ae52b27119d8d8b16eda1a28a0aac82a;p=helm.git rebuilding the library --- diff --git a/helm/software/matita/nlibrary/Plogic/connectives.ma b/helm/software/matita/nlibrary/Plogic/connectives.ma new file mode 100644 index 000000000..d840143e3 --- /dev/null +++ b/helm/software/matita/nlibrary/Plogic/connectives.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "Plogic/equality.ma". + +ninductive True: Prop ≝ +I : True. + +default "true" cic:/matita/basics/connectives/True.ind. + +ninductive False: Prop ≝ . + +default "false" cic:/matita/basics/connectives/False.ind. + +ndefinition Not: Prop → Prop ≝ +λA. A → False. + +interpretation "logical not" 'not x = (Not x). + +ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. +#A; #C; #H; #Hn; nelim (Hn H). +nqed. + +ntheorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. +/3/. +nqed. + +ninductive And (A,B:Prop) : Prop ≝ + conj : A → B → And A B. + +interpretation "logical and" 'and x y = (And x y). + +ntheorem proj1: ∀A,B:Prop. A ∧ B → A. +#A; #B; #AB; nelim AB; //. +nqed. + +ntheorem proj2: ∀ A,B:Prop. A ∧ B → B. +#A; #B; #AB; nelim AB; //. +nqed. + +ninductive Or (A,B:Prop) : Prop ≝ + or_introl : A → (Or A B) + | or_intror : B → (Or A B). + +interpretation "logical or" 'or x y = (Or x y). + +ndefinition decidable : Prop → Prop ≝ +λ A:Prop. A ∨ ¬ A. + +ninductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ + ex_intro: ∀ x:A. P x → ex A P. + +interpretation "exists" 'exists x = (ex ? x). + +ninductive ex2 (A:Type[0]) (P,Q:A \to Prop) : Prop ≝ + ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q. + +ndefinition iff := + λ A,B. (A → B) ∧ (B → A). diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma index 0b4805551..eef0806a2 100644 --- a/helm/software/matita/nlibrary/Plogic/equality.ma +++ b/helm/software/matita/nlibrary/Plogic/equality.ma @@ -14,251 +14,42 @@ include "logic/pts.ma". -ninductive peq (A:Type[3]) (x:A) : A \to Prop \def - refl_peq : peq A x x. +ninductive eq (A:Type[3]) (x:A) : A → Prop ≝ + refl_eq : eq A x x. + +interpretation "leibnitz's equality" 'eq t x y = (eq t x y). -interpretation "leibnitz's equality" 'eq t x y = (peq t x y). +nlemma eq_rect_r: + ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl_eq A a) → P x p. + #A; #a; #x; #p; ncases p; #P; #H; nassumption. +nqed. + +nlemma eq_ind_r : + ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p. + #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption. +nqed. + +(* +nlemma eq_ind_r : + ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p. + #A; #a; #P; #p; #x0; #p0; ngeneralize in match p; +ncases p0; #Heq; nassumption. +nqed. +*) ntheorem rewrite_l: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. x = y → P y. #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption. nqed. -ntheorem sym_peq: ∀A:Type[3].∀x,y:A. x = y → y = x. +ntheorem sym_eq: ∀A:Type[3].∀x,y:A. x = y → y = x. #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x)); ##[ @; ##| nassumption; ##] nqed. ntheorem rewrite_r: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. y = x → P y. -#A; #x; #P; #Hx; #y; #Heq;ncases (sym_peq ? ? ?Heq);nassumption. +#A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption. nqed. ntheorem eq_coerc: ∀A,B:Type[2].A→(A=B)→B. #A; #B; #Ha; #Heq;nelim Heq; nassumption. nqed. - -(* -theorem eq_rect': - \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type. - P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p. - intros. - exact - (match p1 return \lambda y. \lambda p.P y p with - [refl_eq \Rightarrow p]). -qed. - -variant reflexive_eq : \forall A:Type. reflexive A (eq A) -\def refl_eq. - -theorem symmetric_eq: \forall A:Type. symmetric A (eq A). -unfold symmetric.intros.elim H. apply refl_eq. -qed. - -variant sym_eq : \forall A:Type.\forall x,y:A. x=y \to y=x -\def symmetric_eq. - -theorem transitive_eq : \forall A:Type. transitive A (eq A). -unfold transitive.intros.elim H1.assumption. -qed. - -variant trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z -\def transitive_eq. - -theorem symmetric_not_eq: \forall A:Type. symmetric A (λx,y.x ≠ y). -unfold symmetric.simplify.intros.unfold.intro.apply H.apply sym_eq.assumption. -qed. - -variant sym_neq: ∀A:Type.∀x,y.x ≠ y →y ≠ x -≝ symmetric_not_eq. - -theorem eq_elim_r: - \forall A:Type.\forall x:A. \forall P: A \to Prop. - P x \to \forall y:A. y=x \to P y. -intros. elim (sym_eq ? ? ? H1).assumption. -qed. - -theorem eq_elim_r': - \forall A:Type.\forall x:A. \forall P: A \to Set. - P x \to \forall y:A. y=x \to P y. -intros. elim (sym_eq ? ? ? H).assumption. -qed. - -theorem eq_elim_r'': - \forall A:Type.\forall x:A. \forall P: A \to Type. - P x \to \forall y:A. y=x \to P y. -intros. elim (sym_eq ? ? ? H).assumption. -qed. - -theorem eq_f: \forall A,B:Type.\forall f:A\to B. -\forall x,y:A. x=y \to f x = f y. -intros.elim H.apply refl_eq. -qed. - -theorem eq_f': \forall A,B:Type.\forall f:A\to B. -\forall x,y:A. x=y \to f y = f x. -intros.elim H.apply refl_eq. -qed. -*) - -(* -coercion sym_eq. -coercion eq_f. - - -default "equality" - cic:/matita/logic/equality/eq.ind - cic:/matita/logic/equality/sym_eq.con - cic:/matita/logic/equality/transitive_eq.con - cic:/matita/logic/equality/eq_ind.con - cic:/matita/logic/equality/eq_elim_r.con - cic:/matita/logic/equality/eq_rec.con - cic:/matita/logic/equality/eq_elim_r'.con - cic:/matita/logic/equality/eq_rect.con - cic:/matita/logic/equality/eq_elim_r''.con - cic:/matita/logic/equality/eq_f.con -(* *) - cic:/matita/logic/equality/eq_OF_eq.con. -(* *) -(* - cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *) - *) - -theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C. -\forall x1,x2:A. \forall y1,y2:B. -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_rect' ? ? ? ? ? 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_rect' ? ? ? ? ? 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_rect' ? ? ? ? ? q); - fold simplify (nu ? ? (refl_eq ? x)). - generalize in match (nu ? ? (refl_eq ? x)); intro. - apply - (eq_rect' 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:intros; - split; - [ - exact (refl_eq Prop x); - | - exact I; - ] -1: - skip -] -qed. -*) *) -