From 15190ed1fb47989f2d50261db7991186ec3d5e47 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 17 Jun 2011 09:01:29 +0000 Subject: [PATCH] Added a copy of lambdaN to extend the syntax of dummies with types --- matita/matita/lib/basics/logic.ma | 5 + matita/matita/lib/lambdaN/arity.ma | 220 ++++++++++++ matita/matita/lib/lambdaN/arity_eval.ma | 228 ++++++++++++ matita/matita/lib/lambdaN/convertibility.ma | 73 ++++ matita/matita/lib/lambdaN/cube.ma | 43 +++ matita/matita/lib/lambdaN/ext.ma | 116 ++++++ matita/matita/lib/lambdaN/ext_lambda.ma | 81 +++++ matita/matita/lib/lambdaN/inversion.ma | 100 ++++++ matita/matita/lib/lambdaN/lambda_notation.ma | 94 +++++ matita/matita/lib/lambdaN/par_reduction.ma | 307 ++++++++++++++++ matita/matita/lib/lambdaN/rc_eval.ma | 163 +++++++++ matita/matita/lib/lambdaN/rc_hsat.ma | 63 ++++ matita/matita/lib/lambdaN/rc_sat.ma | 181 ++++++++++ matita/matita/lib/lambdaN/reduction.ma | 359 +++++++++++++++++++ matita/matita/lib/lambdaN/sn.ma | 70 ++++ matita/matita/lib/lambdaN/subject.ma | 225 ++++++++++++ matita/matita/lib/lambdaN/subst.ma | 298 +++++++++++++++ matita/matita/lib/lambdaN/subterms.ma | 156 ++++++++ matita/matita/lib/lambdaN/terms.ma | 51 +++ matita/matita/lib/lambdaN/types.ma | 192 ++++++++++ 20 files changed, 3025 insertions(+) create mode 100644 matita/matita/lib/lambdaN/arity.ma create mode 100644 matita/matita/lib/lambdaN/arity_eval.ma create mode 100644 matita/matita/lib/lambdaN/convertibility.ma create mode 100644 matita/matita/lib/lambdaN/cube.ma create mode 100644 matita/matita/lib/lambdaN/ext.ma create mode 100644 matita/matita/lib/lambdaN/ext_lambda.ma create mode 100644 matita/matita/lib/lambdaN/inversion.ma create mode 100644 matita/matita/lib/lambdaN/lambda_notation.ma create mode 100644 matita/matita/lib/lambdaN/par_reduction.ma create mode 100644 matita/matita/lib/lambdaN/rc_eval.ma create mode 100644 matita/matita/lib/lambdaN/rc_hsat.ma create mode 100644 matita/matita/lib/lambdaN/rc_sat.ma create mode 100644 matita/matita/lib/lambdaN/reduction.ma create mode 100644 matita/matita/lib/lambdaN/sn.ma create mode 100644 matita/matita/lib/lambdaN/subject.ma create mode 100644 matita/matita/lib/lambdaN/subst.ma create mode 100644 matita/matita/lib/lambdaN/subterms.ma create mode 100644 matita/matita/lib/lambdaN/terms.ma create mode 100644 matita/matita/lib/lambdaN/types.ma diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 6723cf2cc..261cd77a8 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -27,6 +27,11 @@ lemma eq_ind_r : ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed. +lemma eq_rect_Type0_r: + ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + #A #a #P #H #x #p (generalize in match H) (generalize in match P) + cases p; //; qed. + lemma eq_rect_Type2_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. #A #a #P #H #x #p (generalize in match H) (generalize in match P) diff --git a/matita/matita/lib/lambdaN/arity.ma b/matita/matita/lib/lambdaN/arity.ma new file mode 100644 index 000000000..3df7811c0 --- /dev/null +++ b/matita/matita/lib/lambdaN/arity.ma @@ -0,0 +1,220 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/ext.ma". + +(* ARITIES ********************************************************************) + +(* An arity is a normal term representing the functional structure of a term. + * Arities can be freely applied as lon as the result is typable in λ→. + * we encode an arity with a family of meta-linguistic functions typed by λ→ + * Such a family contains one member for each type of λ→ + *) + +(* type of arity members ******************************************************) + +(* the type of an arity member *) +inductive MEM: Type[0] ≝ + | TOP: MEM + | FUN: MEM → MEM → MEM +. + +definition pred ≝ λC. match C with + [ TOP ⇒ TOP + | FUN _ A ⇒ A + ]. + +definition decidable_MEq: ∀C1,C2:MEM. (C1 = C2) + (C1 ≠ C2). +#C1 (elim C1) -C1 + [ #C2 elim C2 -C2 + [ /2/ + | #B2 #A2 #_ #_ @inr @nmk #false destruct + ] + | #B1 #A1 #IHB1 #IHA1 #C2 elim C2 -C2 + [ @inr @nmk #false destruct + | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1 #HB + [ elim (IHA1 A2) - IHA1 #HA + [ /2/ | @inr @nmk #false destruct elim HA /2/ ] + | @inr @nmk #false destruct elim HB /2/ + ] +qed. + +lemma fun_neq_sym: ∀A,C,B. pred C ≠ A → C ≠ FUN B A. +#A #C #B #HA elim HA -HA #HA @nmk #H @HA -HA >H // +qed. + +(* arity members **************************************************************) + +(* the arity members of type TOP *) +inductive Top: Type[0] ≝ + | SORT: Top +. + +(* the arity members of type A *) +let rec Mem A ≝ match A with + [ TOP ⇒ Top + | FUN B A ⇒ Mem B → Mem A + ]. + +(* the members of the arity "sort" *) +let rec sort_mem A ≝ match A return λA. Mem A with + [ TOP ⇒ SORT + | FUN B A ⇒ λ_.sort_mem A + ]. + +(* arities ********************************************************************) + +(* the type of arities *) +definition Arity ≝ ∀A. Mem A. + +(* the arity "sort" *) +definition sort ≝ λA. sort_mem A. + +(* the arity "constant" *) +definition const: ∀B. Mem B → Arity. +#B #x #A. elim (decidable_MEq B A) #H [ elim H @x | @(sort_mem A) ] +qed. + +(* application of arities *) +definition aapp: MEM → Arity → Arity → Arity ≝ λB,a,b,C. a (FUN B C) (b B). + +(* abstraction of arities *) +definition aabst: (Arity → Arity) → Arity ≝ + λf,C. match C return λC. Mem C with + [ TOP ⇒ sort_mem TOP + | FUN B A ⇒ λx. f (const B x) A + ]. + +(* extensional equality of arity members **************************************) + +(* Extensional equality of arity members (extensional equalty of functions). + * The functions may not respect extensional equality so reflexivity fails + * in general but may hold for specific arity members. + *) +let rec ameq A ≝ match A return λA. Mem A → Mem A → Prop with + [ TOP ⇒ λa1,a2. a1 = a2 + | FUN B A ⇒ λa1,a2. ∀b1,b2. ameq B b1 b2 → ameq A (a1 b1) (a2 b2) + ]. + +interpretation + "extensional equality (arity member)" + 'Eq1 A a1 a2 = (ameq A a1 a2). + +(* reflexivity of extensional equality for an arity member *) +definition invariant_mem ≝ λA,m. m ≅^A m. + +interpretation + "invariance (arity member)" + 'Invariant1 a A = (invariant_mem A a). + + +interpretation + "invariance (arity member with implicit type)" + 'Invariant a = (invariant_mem ? a). + +lemma symmetric_ameq: ∀A. symmetric ? (ameq A). +#A elim A -A /4/ +qed. + +lemma transitive_ameq: ∀A. transitive ? (ameq A). +#A elim A -A /5/ +qed. + +lemma invariant_sort_mem: ∀A. ! sort_mem A. +#A elim A normalize // +qed. + +axiom const_eq: ∀A,x. const A x A ≅^A x. + +axiom const_neq: ∀A,B,x. A ≠ B → const A x B ≅^B (sort_mem B). + +(* extensional equality of arities ********************************************) + +definition aeq: Arity → Arity → Prop ≝ λa1,a2. ∀A. a1 A ≅^A a2 A. + +interpretation + "extensional equality (arity)" + 'Eq a1 a2 = (aeq a1 a2). + +definition invariant: Arity → Prop ≝ λa. a ≅ a. + +interpretation + "invariance (arity)" + 'Invariant a = (invariant a). + +lemma symmetric_aeq: symmetric … aeq. +/2/ qed. + +lemma transitive_aeq: transitive … aeq. +/2/ qed. + +lemma const_comp: ∀A,x1,x2. x1 ≅^A x2 → const … x1 ≅ const … x2. +#A #x1 #x2 #Hx #C elim (decidable_MEq A C) #H + [ H // ] +@transitive_ameq; [2: @(const_neq … H) | skip ] +lapply (transitive_ameq ????? (Ha (FUN B C))) -Ha [3: #Ha @Ha // |2: skip ] +@symmetric_ameq @const_neq /2/ +qed. + +(* extensional equality of arity contexts *************************************) + +definition aceq ≝ λE1,E2. all2 … aeq E1 E2. + +interpretation + "extensional equality (arity context)" + 'Eq E1 E2 = (aceq E1 E2). + +definition invariant_env: list Arity → Prop ≝ λE. E ≅ E. + +interpretation + "invariance (arity context)" + 'Invariant E = (invariant_env E). + +lemma symmetric_aceq: symmetric … aceq. +/2/ qed. + +lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 → + ∀i. nth i ? E1 sort ≅ nth i ? E2 sort. +#E1 #E2 #H #i @(all2_nth … aeq) // +qed. diff --git a/matita/matita/lib/lambdaN/arity_eval.ma b/matita/matita/lib/lambdaN/arity_eval.ma new file mode 100644 index 000000000..6fcf0e0c0 --- /dev/null +++ b/matita/matita/lib/lambdaN/arity_eval.ma @@ -0,0 +1,228 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/arity.ma". + +(* ARITY ASSIGNMENT ***********************************************************) + +(* the arity type *************************************************************) + +(* arity type assigned to the term t in the environment E *) +let rec ata K t on t ≝ match t with + [ Sort _ ⇒ TOP + | Rel i ⇒ nth i … K TOP + | App M N ⇒ pred (ata K M) + | Lambda N M ⇒ let C ≝ ata K N in FUN C (ata (C::K) M) + | Prod _ _ ⇒ TOP + | D M ⇒ TOP (* ??? not so sure yet *) + ]. + +interpretation "arity type assignment" 'IInt1 t K = (ata K t). + +lemma ata_app: ∀M,N,K. 〚App M N〛_[K] = pred (〚M〛_[K]). +// qed. + +lemma ata_lambda: ∀M,N,K. 〚Lambda N M〛_[K] = FUN (〚N〛_[K]) (〚M〛_[〚N〛_[K]::K]). +// qed. + +lemma ata_rel_lt: ∀H,K,i. (S i) ≤ |K| → 〚Rel i〛_[K @ H] = 〚Rel i〛_[K]. +#H #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ] +#A #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie +qed. + +lemma ata_rel_ge: ∀H,K,i. (S i) ≰ |K| → + 〚Rel i〛_[K @ H] = 〚Rel (i-|K|)〛_[H]. +#H #K elim K -K [ normalize // ] +#A #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ] +normalize #i #_ #Hie @IHK /2/ +qed. + +(* weakeing and thinning lemma for the arity type assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma ata_lift: ∀p,K,Kp. p = |Kp| → ∀t,k,Kk. k = |Kk| → + 〚lift t k p〛_[Kk @ Kp @ K] = 〚t〛_[Kk @ K]. +#p #K #Kp #HKp #t elim t -t // + [ #i #k #Kk #HKk @(leb_elim (S i) k) #Hik + [ >(lift_rel_lt … Hik) >HKk in Hik #Hik + >(ata_rel_lt … Hik) >(ata_rel_lt … Hik) // + | >(lift_rel_ge … Hik) >HKk in Hik #Hik + >(ata_rel_ge … Hik) (ata_rel_ge …) >length_append >HKp; + [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ] + ] + | #M #N #IHM #_ #k #Kk #HKk >lift_app >ata_app /3/ + | #N #M #IHN #IHM #k #Kk #HKk >lift_lambda >ata_lambda + >IHN // >(IHM … (? :: ?)) // >commutative_plus /2/ + ] +qed. + +(* substitution lemma for the arity type assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma ata_subst: ∀v,K,t,k,Kk. k = |Kk| → + 〚t[k≝v]〛_[Kk @ K] = 〚t〛_[Kk @ 〚v〛_[K]::K]. +#v #K #t elim t -t // + [ #i #k #Kk #HKk @(leb_elim (S i) k) #H1ik + [ >(subst_rel1 … H1ik) >HKk in H1ik #H1ik + >(ata_rel_lt … H1ik) >(ata_rel_lt … H1ik) // + | @(eqb_elim i k) #H2ik + [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HKk in H1ik #H1ik + >(ata_rel_ge … H1ik) (ata_lift ? ? ? ? ? ? ([])) // + | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik) + >ata_rel_ge; [2: /2/ ] <(associative_append ? ? ([?]) ?) + >ata_rel_ge >length_append >commutative_plus; + [ subst_app >ata_app /3/ + | #N #M #IHN #IHM #k #Kk #HKk >subst_lambda > ata_lambda + >IHN // >commutative_plus >(IHM … (? :: ?)) /2/ + ] +qed. + +(* the arity ******************************************************************) + +(* arity assigned to the term t in the environments E and K *) +let rec aa K E t on t ≝ match t with + [ Sort _ ⇒ sort + | Rel i ⇒ nth i … E sort + | App M N ⇒ aapp (〚N〛_[K]) (aa K E M) (aa K E N) + | Lambda N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M) + | Prod N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M) + | D M ⇒ sort (* ??? not so sure yet *) + ]. + +interpretation "arity assignment" 'IInt2 t E K = (aa K E t). + +lemma aa_app: ∀M,N,E,K. 〚App M N〛_[E,K] = aapp (〚N〛_[K]) (〚M〛_[E,K]) (〚N〛_[E,K]). +// qed. + +lemma aa_lambda: ∀N,M,E,K. 〚Lambda N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]). +// qed. + +lemma aa_prod: ∀N,M,E,K. 〚Prod N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]). +// qed. + +lemma aa_rel_lt: ∀K2,K1,D,E,i. (S i) ≤ |E| → + 〚Rel i〛_[E @ D, K1] = 〚Rel i〛_[E, K2]. +#K1 #K1 #D #E elim E -E [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ] +#C #E #IHE #i elim i -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie +qed. + +lemma aa_rel_lt_id: ∀K,D,E,i. (S i) ≤ |E| → + 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E, K]. +#K @(aa_rel_lt K) qed. + +lemma aa_rel_ge: ∀K2,K1,D,E,i. (S i) ≰ |E| → + 〚Rel i〛_[E @ D, K1] = 〚Rel (i-|E|)〛_[D, K2]. +#K2 #K1 #D #E elim E -E [ normalize // ] +#C #E #IHE #i elim i -i [1: -IHE #Hie elim Hie -Hie #Hie elim (Hie ?) /2/ ] +normalize #i #_ #Hie @IHE /2/ +qed. + +lemma aa_rel_ge_id: ∀K,D,E,i. (S i) ≰ |E| → + 〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D, K]. +#K @(aa_rel_ge K) qed. + +(* weakeing and thinning lemma for the arity assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma aa_lift: ∀K,E1,E2. E1 ≅ E2 → ∀p,Kp,Ep. p=|Kp| → p = |Ep| → + ∀t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k → + 〚lift t k p〛_[E1k @ Ep @ E1, Kk @ Kp @ K] ≅ 〚t〛_[E2k @ E2, Kk @ K]. +#K #E1 #E2 #HE #p #Kp #Ep #HKp #HEp #t elim t -t /2 by invariant_sort/ + [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #Hik + [ >(lift_rel_lt … Hik) >HE1k in Hik #Hik >(aa_rel_lt_id … Hik) + >(all2_length … HEk) in Hik #Hik >(aa_rel_lt_id … Hik) /2 by nth_sort_comp/ + | >(lift_rel_ge … Hik) >HE1k in Hik #Hik <(associative_append … E1k) + >(aa_rel_ge_id …) >length_append >HEp; [2: @(arith3 … Hik) ] + >(all2_length … HEk) in Hik #Hik >(aa_rel_ge_id … Hik) >arith2; + [ /2 by nth_sort_comp/ | @not_lt_to_le /2/ ] + ] + | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_app >aa_app + >ata_lift /3/ + | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_lambda >aa_lambda + @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus + @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/ + | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_prod >aa_prod + @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus + @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/ + ] +qed. + +lemma aa_comp: ∀E1,E2. E1 ≅ E2 → ∀t,K. 〚t〛_[E1, K] ≅ 〚t〛_[E2, K]. +#E1 #E2 #HE #t #K <(lift_0 t 0) in ⊢ (? % ?) +@(aa_lift … ([]) ([]) … ([]) ([]) ([])) // +qed. + +(* the assigned arity is invariant *) +lemma aa_invariant: ∀t,E,K. !E → !〚t〛_[E, K]. +/2/ qed. + +(* substitution lemma for the arity assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma aa_subst: ∀K,E1,E2. E1 ≅ E2 → + ∀v,t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k → + 〚t[k≝v]〛_[E1k@E1, Kk@K] ≅ 〚t〛_[E2k@〚v〛_[E2,K]::E2, Kk@〚v〛_[K]::K]. +#K #E1 #E2 #HE #v #t elim t -t /2 by invariant_sort/ + [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #H1ik + [ >(subst_rel1 … H1ik) >HE1k in H1ik #H1ik >(aa_rel_lt_id … H1ik) + >(all2_length … HEk) in H1ik #H1ik >(aa_rel_lt_id … H1ik) /2/ + | @(eqb_elim i k) #H2ik + [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HE1k in H1ik #H1ik + >(all2_length … HEk) in H1ik #H1ik >(aa_rel_ge_id … H1ik) HE1k in HKk #HKk -HE1k k >(all2_length … HEk) in HKk #HKk + @(aa_lift … ([]) ([]) ([])) /3/ + | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik + >(subst_rel3 … Hik) >aa_rel_ge_id; [2: /2/ ] + <(associative_append ? ? ([?]) ?) in ⊢ (? ? (? ? % ?)) + >HE1k in Hik #Hik >(aa_rel_ge (Kk@K)) + >length_append >commutative_plus <(all2_length … HEk); + [ subst_app >aa_app + >ata_subst /3/ + | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_lambda >aa_lambda + @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus + @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/ + | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_prod >aa_prod + @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus + @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/ + ] +qed. + +(* the assigned arity is constant *) +lemma aa_isc: ∀t,E,K. !E → all2 … isc E K → isc (〚t〛_[E,K]) (〚t〛_[K]). +#t elim t -t /2 by isc_sort/ + [ #i #E #K #HE #H @(all2_nth … isc) // + | /3/ + | #N #M #IHN #IHM #E #K #HE #H >aa_lambda >ata_lambda + + + +(* +const ? (〚v〛_[E1,K] (〚v〛_[K])) ≅ 〚v〛_[E1,K]. + +theorem aa_beta: ∀K,E1,E2. E1 ≅ E2 → ∀w,t,v. 〚v〛_[K] = 〚w〛_[K] → + 〚App (Lambda w t) v〛_[E1,K] ≅ 〚t[0≝v]〛_[E2,K]. +#K #E1 #E2 #HE #w #t #v #H > aa_app >aa_lambda +@transitive_aeq; [3: @symmetric_aeq @(aa_subst … E1 … ([]) ([]) ([])) /2/ | skip ] +>H @aa_comp -H v; #C whd in ⊢ (? ? % ?) +*) + +(* +axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 :: E2. + +axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c. +@A qed. +*) diff --git a/matita/matita/lib/lambdaN/convertibility.ma b/matita/matita/lib/lambdaN/convertibility.ma new file mode 100644 index 000000000..377d3c890 --- /dev/null +++ b/matita/matita/lib/lambdaN/convertibility.ma @@ -0,0 +1,73 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/reduction.ma". + +(* +inductive T : Type[0] ≝ + | Sort: nat → T + | Rel: nat → T + | App: T → T → T + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) + | D: T →T +. +*) + +inductive conv : T →T → Prop ≝ + | cbeta: ∀P,M,N. conv (App (Lambda P M) N) (M[0 ≝ N]) + | cappl: ∀M,M1,N. conv M M1 → conv (App M N) (App M1 N) + | cappr: ∀M,N,N1. conv N N1 → conv (App M N) (App M N1) + | claml: ∀M,M1,N. conv M M1 → conv (Lambda M N) (Lambda M1 N) + | clamr: ∀M,N,N1. conv N N1 → conv (Lambda M N) (Lambda M N1) + | cprodl: ∀M,M1,N. conv M M1 → conv (Prod M N) (Prod M1 N) + | cprodr: ∀M,N,N1. conv N N1 → conv (Prod M N) (Prod M N1) + | cd: ∀M,M1. conv (D M) (D M1). + +definition CO ≝ star … conv. + +lemma red_to_conv: ∀M,N. red M N → conv M N. +#M #N #redMN (elim redMN) /2/ +qed. + +inductive d_eq : T →T → Prop ≝ + | same: ∀M. d_eq M M + | ed: ∀M,M1. d_eq (D M) (D M1) + | eapp: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 → + d_eq (App M1 N1) (App M2 N2) + | elam: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 → + d_eq (Lambda M1 N1) (Lambda M2 N2) + | eprod: ∀M1,M2,N1,N2. d_eq M1 M2 → d_eq N1 N2 → + d_eq (Prod M1 N1) (Prod M2 N2). + +lemma conv_to_deq: ∀M,N. conv M N → red M N ∨ d_eq M N. +#M #N #coMN (elim coMN) + [#P #B #C %1 // + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 #N1 #coPM1 * [#redP %1 /2/ | #eqPM1 %2 /3/] + |#P #M1 %2 // + ] +qed. + +(* FG: THIS IN NOT COMPLETE +theorem main1: ∀M,N. CO M N → + ∃P,Q. star … red M P ∧ star … red N Q ∧ d_eq P Q. +#M #N #coMN (elim coMN) + [#B #C #rMB #convBC * #P1 * #Q1 * * #redMP1 #redBQ1 + #deqP1Q1 (cases (conv_to_deq … convBC)) + [ + |@(ex_intro … M) @(ex_intro … M) % // % // + ] +*) diff --git a/matita/matita/lib/lambdaN/cube.ma b/matita/matita/lib/lambdaN/cube.ma new file mode 100644 index 000000000..8ac3d978c --- /dev/null +++ b/matita/matita/lib/lambdaN/cube.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "convertibility.ma". +include "types.ma". + +(* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************) + +inductive Cube_Ax: nat → nat → Prop ≝ + | star_box: Cube_Ax 0 1 +. + +(* The λPω pure type system (a.k.a. λC or CC) *********************************) + +inductive CC_Re: nat → nat → nat → Prop ≝ + | star_star: CC_Re 0 0 0 + | box_star : CC_Re 1 0 0 + | box_box : CC_Re 1 1 1 + | star_box : CC_Re 0 1 1 +. + +definition CC: pts ≝ mk_pts Cube_Ax CC_Re conv. + +(* The λω pure type system (a.k.a. Fω) ****************************************) + +inductive FO_Re: nat → nat → nat → Prop ≝ + | star_star: FO_Re 0 0 0 + | box_star : FO_Re 1 0 0 + | box_box : FO_Re 1 1 1 +. + +definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv. diff --git a/matita/matita/lib/lambdaN/ext.ma b/matita/matita/lib/lambdaN/ext.ma new file mode 100644 index 000000000..7e64aba31 --- /dev/null +++ b/matita/matita/lib/lambdaN/ext.ma @@ -0,0 +1,116 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/list.ma". + +(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) + +(* arithmetics ****************************************************************) + +lemma arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y. +#x #y #HS @nmk (elim HS) -HS /3/ +qed. + +lemma arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k. +#i #p #k #H @plus_to_minus +>commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/ +qed. + +lemma arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z. +#x #y #z #H @nmk (elim H) -H /3/ +qed. + +lemma arith4: ∀x,y. S x ≰ y → x≠y → y < x. +#x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/ +qed. + +lemma arith5: ∀x,y. x < y → S (y - 1) ≰ x. +#x #y #H @lt_to_not_le H // ] +#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H -H; normalize /3/ +qed. + +lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b → + ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b). +#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ] +#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H -H // +qed. + +lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop. + ∀l1,l2. all2 … P l1 l2 → all2 … P (tail … l1) (tail … l2). +#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ] +#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H -H // +qed. + +lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b → + ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b). +#A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ] +qed. + +lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 → + ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2). +#A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ] +#x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ] +#x2 #m2 #_ #H elim H -H /3/ +qed. + +lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … (all2 … P). +#A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ] +#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ] +#x2 #l2 #_ #H elim H -H /3/ +qed. diff --git a/matita/matita/lib/lambdaN/ext_lambda.ma b/matita/matita/lib/lambdaN/ext_lambda.ma new file mode 100644 index 000000000..a183047e0 --- /dev/null +++ b/matita/matita/lib/lambdaN/ext_lambda.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/ext.ma". +include "lambda/subst.ma". + +(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) + +(* substitution ***************************************************************) +(* +axiom is_dummy_lift: ∀p,t,k. is_dummy (lift t k p) = is_dummy t. +*) +(* FG: do we need this? +definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *) + +lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k = + Appl (lift F p k) (map … (lift0 p k) l). +#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl // +qed. +*) + +lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i. +#i #p #k #Hik normalize >(le_to_leb_true … Hik) // +qed. + +lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p). +#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/ +qed. + +lemma lift_app: ∀M,N,k,p. + lift (App M N) k p = App (lift M k p) (lift N k p). +// qed. + +lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p = + Lambda (lift N k p) (lift M (k + 1) p). +// qed. + +lemma lift_prod: ∀N,M,k,p. + lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p). +// qed. + +lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L]. +// qed. + +lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L]. +// qed. + +lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L]. +// qed. + + +axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i = + (lift B (j+k+1) i)[j≝lift A k i]. + +(* telescopic delifting substitution of l in M. + * Rel 0 is replaced with the head of l + *) +let rec tsubst M l on l ≝ match l with + [ nil ⇒ M + | cons A D ⇒ (tsubst M[0≝A] D) + ]. + +interpretation "telescopic substitution" 'Subst M l = (tsubst M l). + +lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[/l] = t. +#l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *) +qed. + +lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n. +// qed. diff --git a/matita/matita/lib/lambdaN/inversion.ma b/matita/matita/lib/lambdaN/inversion.ma new file mode 100644 index 000000000..0c2c2a98b --- /dev/null +++ b/matita/matita/lib/lambdaN/inversion.ma @@ -0,0 +1,100 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/types.ma". + +(* +inductive TJ (p: pts): list T → T → T → Prop ≝ + | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j) + | start: ∀G.∀A.∀i.TJ p G A (Sort i) → + TJ p (A::G) (Rel 0) (lift A 0 1) + | weak: ∀G.∀A,B,C.∀i. + TJ p G A B → TJ p G C (Sort i) → + TJ p (C::G) (lift A 0 1) (lift B 0 1) + | prod: ∀G.∀A,B.∀i,j,k. Re p i j k → + TJ p G A (Sort i) → TJ p (A::G) B (Sort j) → + TJ p G (Prod A B) (Sort k) + | app: ∀G.∀F,A,B,a. + TJ p G F (Prod A B) → TJ p G a A → + TJ p G (App F a) (subst B 0 a) + | abs: ∀G.∀A,B,b.∀i. + TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) → + TJ p G (Lambda A b) (Prod A B) + | conv: ∀G.∀A,B,C.∀i. Co p B C → + TJ p G A B → TJ p G C (Sort i) → TJ p G A C + | dummy: ∀G.∀A,B.∀i. + TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B. +*) + +axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C → +∃P,Q. A = Lambda P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C. + +axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C → +∃P,Q. A = Prod P Q ∧ lift P 0 1 = B ∧ lift Q 1 1 = C. + +axiom conv_lift: ∀P,M,N. Co P M N → Co P (lift M 0 1) (lift N 0 1). + +axiom weak_in: ∀P,G,A,B,M,N, i. + A::G ⊢_{P} M : N → G ⊢_{P} B : Sort i → + (lift A 0 1)::B::G ⊢_{P} lift M 1 1 : lift N 1 1. + +axiom refl_conv: ∀P,A. Co P A A. +axiom sym_conv: ∀P,A,B. Co P A B → Co P B A. +axiom trans_conv: ∀P,A,B,C. Co P A B → Co P B C → Co P A C. + +theorem prod_inv: ∀P,G,M,N. G ⊢_{P} M : N → ∀A,B.M = Prod A B → + ∃i,j,k. Co P N (Sort k) ∧ G ⊢_{P} A : Sort i ∧ A::G ⊢_{P} B : Sort j. +#Pts #G #M #N #t (elim t); + [#i #j #Aij #A #b #H destruct + |#G1 #P #i #t #_ #A #b #H destruct + |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #B #Hl + cases (prod_lift … Hl) #A1 * #B1 * * #eqP #eqA #eqB + cases (H1 … eqP) #i * #j * #k * * #c1 #t3 #t4 + @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) lift_subst_up @beta; // + |// + |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k + normalize @appl; [@Hind1 |@Hind2] + |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k + normalize @lam; [@Hind1 |@Hind2] + |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k + normalize @prod; [@Hind1 |@Hind2] + |#M1 #M2 #pr2 #Hind #k normalize @d // + ] +qed. + +theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → + pr M[n≝N] M1[n≝N1]. +@Telim_size #P (cases P) + [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) // + |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1) + (cases (true_or_false (leb i n))) + [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein))) + [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) // + |#eqin >eqin >subst_rel2 >subst_rel2 /2/ + ] + |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni + >(subst_rel3 … ltni) >(subst_rel3 … ltni) // + ] + |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 + (cases (true_or_false (is_lambda Q))) + [#islambda (cases (is_lambda_to_exists … islambda)) + #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3)) + #M3 * #N3 * + [* * #eqM1 #pr4 #pr5 >eqM1 + >(plus_n_O n) in ⊢ (??%) >subst_lemma @beta; + [eqQ + @(transitive_lt ? (size (Lambda M2 N2))) normalize // + |@Hind // normalize // + ] + |* * #eqM1 #pr4 #pr5 >eqM1 @appl; + [@Hind // eqM1 @appl; + [@Hind // normalize // |@Hind // normalize // ] + ] + |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 + (cases (prLambda … pr1)) + #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam; + [@Hind // normalize // | @Hind // normalize // ] + |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2 + (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 + @prod; [@Hind // normalize // | @Hind // normalize // ] + |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1)) + #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize // + ] +qed. + +lemma pr_full_app: ∀M,N,N1. pr N N1 → + (∀S.subterm S M → pr S (full S)) → + pr (App M N) (full_app M N1). +#M (elim M) normalize /2/ + [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/ + |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/ + |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/ + |#P #Hind #N1 #N2 #prN #H @appl // @d /2/ + ] +qed. + +theorem pr_full: ∀M. pr M (full M). +@Telim #M (cases M) normalize + [// + |// + |#M1 #N1 #H @pr_full_app /3/ + |#M1 #N1 #H normalize /3/ + |#M1 #N1 #H @prod /2/ + |#P #H @d /2/ + ] +qed. + +lemma complete_app: ∀M,N,P. + (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) → + pr (App M N) P → pr P (full_app M (full N)). +#M (elim M) normalize + [#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // + #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@(subH (Sort n)) // |@subH //] + |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // + #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@(subH (Rel n)) // |@subH //] + |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH + cases (prApp_not_lambda … prH ?) // + #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@Hind1 /3/ |@subH //] + |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH + cases (prApp_lambda … prH) #M2 * #N2 * + [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/ + |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1)) + #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/ + ] + |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH + cases (prApp_not_lambda … prH ?) // + #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; + [@(subH (Prod P Q)) // |@subH //] + |#P #Hind #N1 #N2 #subH #pr1 + cases (prApp_not_lambda … pr1 ?) // + #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl; + [@(subH (D P) M1) // |@subH //] + ] +qed. + +theorem complete: ∀M,N. pr M N → pr N (full M). +@Telim #M (cases M) + [#n #Hind #N #prH normalize >(prSort … prH) // + |#n #Hind #N #prH normalize >(prRel … prH) // + |#M #N #Hind #Q @complete_app + #S #P #subS @Hind // + |#P #P1 #Hind #N #Hpr + (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/ + |#P #P1 #Hind #N #Hpr + (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/ + |#N #Hind #P #prH normalize cases (prD … prH) + #Q * #eqP >eqP #prN @d @Hind // + ] +qed. + +theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S. +pr Q S ∧ pr P S. +#P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/ +qed. + diff --git a/matita/matita/lib/lambdaN/rc_eval.ma b/matita/matita/lib/lambdaN/rc_eval.ma new file mode 100644 index 000000000..3fdeed410 --- /dev/null +++ b/matita/matita/lib/lambdaN/rc_eval.ma @@ -0,0 +1,163 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/rc_hsat.ma". + +(* THE EVALUATION *************************************************************) + +(* The arity of a term t in an environment E *) +let rec aa E t on t ≝ match t with + [ Sort _ ⇒ SORT + | Rel i ⇒ nth i … E SORT + | App M N ⇒ pred (aa E M) + | Lambda N M ⇒ let Q ≝ aa E N in ABST Q (aa (Q::E) M) + | Prod N M ⇒ aa ((aa E N)::E) M + | D M ⇒ aa E M + ]. + +interpretation "arity assignment (term)" 'Eval1 t E = (aa E t). + +(* The arity of a type context *) +let rec caa E G on G ≝ match G with + [ nil ⇒ E + | cons t F ⇒ let D ≝ caa E F in 〚t〛_[D] :: D + ]. + +interpretation "arity assignment (type context)" 'Eval1 G E = (caa E G). + +lemma aa_app: ∀M,N,E. 〚App M N〛_[E] = pred (〚M〛_[E]). +// qed. + +lemma aa_lambda: ∀M,N,E. 〚Lambda N M〛_[E] = ABST (〚N〛_[E]) (〚M〛_[〚N〛_[E]::E]). +// qed. + +lemma aa_prod: ∀M,N,E. 〚Prod N M〛_[E] = 〚M〛_[〚N〛_[E]::E]. +// qed. + +lemma aa_rel_lt: ∀D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D] = 〚Rel i〛_[E]. +#D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ] +#C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie +qed. + +lemma aa_rel_ge: ∀D,E,i. (S i) ≰ |E| → + 〚Rel i〛_[E @ D] = 〚Rel (i-|E|)〛_[D]. +#D #E (elim E) -E [ normalize // ] +#C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ] +normalize #i #_ #Hie @IHE /2/ +qed. + +(* weakeing and thinning lemma arity assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma aa_lift: ∀E,Ep,t,Ek. + 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E] = 〚t〛_[Ek @ E]. +#E #Ep #t (elim t) -t + [ #n // + | #i #Ek @(leb_elim (S i) (|Ek|)) #Hik + [ >(lift_rel_lt … Hik) >(aa_rel_lt … Hik) >(aa_rel_lt … Hik) // + | >(lift_rel_ge … Hik) >(aa_rel_ge … Hik) (aa_rel_ge …) (>length_append) + [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ] + ] + | /4/ + | #N #M #IHN #IHM #Ek >lift_lambda >aa_lambda + >commutative_plus >(IHM (? :: ?)) /3/ + | #N #M #IHN #IHM #Ek >lift_prod >aa_prod + >commutative_plus >(IHM (? :: ?)) /3/ + | #M #IHM #Ek @IHM + ] +qed. + +(* substitution lemma arity assignment *) +(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *) +lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E]. +#v #E #t (elim t) -t + [ // + | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik + [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) // + | @(eqb_elim i (|Ek|)) #H2ik + [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2 + >(aa_lift ? ? ? ([])) (subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ] + <(associative_append ? ? ([?]) ?) + >aa_rel_ge >length_append (>commutative_plus) + [ subst_lambda > aa_lambda + >commutative_plus >(IHM (? :: ?)) /3/ + | #N #M #IHN #IHM #Ek >subst_prod > aa_prod + >commutative_plus >(IHM (? :: ?)) /4/ + | #M #IHM #Ek @IHM +qed. + + + + + + + + + + + + + + + + + + + + +(* +(* extensional equality of the interpretations *) +definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K]. + +interpretation + "extensional equality of the type interpretations" + 'napart t1 t2 = (eveq t1 t2). +*) + +axiom ev_lift_0_S: ∀t,p,C,E,K. 〚lift t 0 (S p)〛_[C::E, K] ≅ 〚lift t 0 p〛_[E, K]. + +theorem tj_ev: ∀G,t,u. G ⊢t:u → ∀E,l. l ∈ 〚G〛_[E] → t[l] ∈ 〚u[l]〛_[[], []]. +#G #t #u #tjtu (elim tjtu) -G t u tjtu + [ #i #j #_ #E #l #_ >tsubst_sort >tsubst_sort /2 by SAT0_sort/ + | #G #u #n #tju #IHu #E #l (elim l) -l (normalize) + [ #_ /2 by SAT1_rel/ + | #hd #tl #_ #H (elim H) -H #Hhd #Htl + >lift_0 >delift // >lift_0 + + + + (@mem_rceq_trans) [3: @symmetric_rceq @ev_lift_0_S | skip ] + +*) +(* +theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A. +#G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/ +qed. +*) + +(* +theorem tev_rel_S: ∀i,R,H. 〚Rel (S i)〛_(R::H) = 〚Rel i〛_(H). +// qed. +*) +(* +theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a. + (a :: l1) @ l2 = a :: (l1 @ l2). +// qed. +*) diff --git a/matita/matita/lib/lambdaN/rc_hsat.ma b/matita/matita/lib/lambdaN/rc_hsat.ma new file mode 100644 index 000000000..7426d812b --- /dev/null +++ b/matita/matita/lib/lambdaN/rc_hsat.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/rc_sat.ma". + +(* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************) + +(* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *) + +(* The type of the higher order r.c.'s having a given carrier. + * a h.o. r.c is implemented as an inductively defined metalinguistic function + * [ a CIC function in the present case ]. + *) +let rec HRC P ≝ match P with + [ SORT ⇒ RC + | ABST Q P ⇒ HRC Q → HRC P + ]. + +(* The default h.o r.c. + * This is needed to complete the partial interpretation of types. + *) +let rec defHRC P ≝ match P return λP. HRC P with + [ SORT ⇒ snRC + | ABST Q P ⇒ λ_. defHRC P + ]. + +(* extensional equality *******************************************************) + +(* This is the extensional equalty of functions + * modulo the extensional equality on the domain. + * The functions may not respect extensional equality so reflexivity fails. + *) +let rec hrceq P ≝ match P return λP. HRC P → HRC P → Prop with + [ SORT ⇒ λC1,C2. C1 ≅ C2 + | ABST Q P ⇒ λC1,C2. ∀B1,B2. hrceq Q B1 B2 → hrceq P (C1 B1) (C2 B2) + ]. + +interpretation + "extensional equality (h.o. reducibility candidate)" + 'Eq1 P C1 C2 = (hrceq P C1 C2). + +lemma symmetric_hrceq: ∀P. symmetric ? (hrceq P). +#P (elim P) -P /4/ +qed. + +lemma transitive_hrceq: ∀P. transitive ? (hrceq P). +#P (elim P) -P /5/ +qed. + +lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P. +#P (elim P) -P (normalize) /2/ +qed. diff --git a/matita/matita/lib/lambdaN/rc_sat.ma b/matita/matita/lib/lambdaN/rc_sat.ma new file mode 100644 index 000000000..3eb04315f --- /dev/null +++ b/matita/matita/lib/lambdaN/rc_sat.ma @@ -0,0 +1,181 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/sn.ma". + +(* REDUCIBILITY CANDIDATES ****************************************************) + +(* The reducibility candidate (r.c.) ******************************************) + +(* We use saturated subsets of strongly normalizing terms [1] + * rather than standard reducibility candidates [2]. + * The benefit is that reduction is not needed to define such subsets. + * [1] Geuvers, H. 1994. A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions. + * [2] Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA. + *) +record RC : Type[0] ≝ { + mem : T → Prop; + cr1 : CR1 mem; + sat0: SAT0 mem; + sat1: SAT1 mem; + sat2: SAT2 mem; + sat3: SAT3 mem; (* we add the clusure by rev dapp *) + sat4: SAT4 mem (* we add the clusure by dummies *) +}. + +(* HIDDEN BUG: + * if SAT0 and SAT1 are expanded, + * the projections sat0 and sat1 are not generated + *) + +interpretation "membership (reducibility candidate)" 'mem A R = (mem R A). + +(* the r.c. of all s.n. terms *) +definition snRC: RC ≝ mk_RC SN …. +/2/ qed. + +(* +(* a generalization of mem on lists *) +let rec memc E l on l : Prop ≝ match l with + [ nil ⇒ True + | cons hd tl ⇒ match E with + [ nil ⇒ hd ∈ snRC ∧ memc E tl + | cons C D ⇒ hd ∈ C ∧ memc D tl + ] + ]. + +interpretation + "componentwise membership (context of reducibility candidates)" + 'mem l H = (memc H l). +*) +(* extensional equality of r.c.'s *********************************************) + +definition rceq: RC → RC → Prop ≝ + λC1,C2. ∀M. (M ∈ C1 → M ∈ C2) ∧ (M ∈ C2 → M ∈ C1). + +interpretation + "extensional equality (reducibility candidate)" + 'Eq C1 C2 = (rceq C1 C2). + +definition rceql ≝ λl1,l2. all2 … rceq l1 l2. + +interpretation + "extensional equality (context of reducibility candidates)" + 'Eq C1 C2 = (rceql C1 C2). + +lemma reflexive_rceq: reflexive … rceq. +/2/ qed. + +lemma symmetric_rceq: symmetric … rceq. +#x #y #H #M elim (H M) -H /3/ +qed. + +lemma transitive_rceq: transitive … rceq. +#x #y #z #Hxy #Hyz #M elim (Hxy M) -Hxy; elim (Hyz M) -Hyz /4/ +qed. +(* +theorem reflexive_rceql: reflexive … rceql. +#l (elim l) /2/ +qed. +*) +(* HIDDEN BUG: + * Without the type specification, this statement has two interpretations + * but matita does not complain + *) +lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2. +#M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/ +qed. +(* +(* NOTE: hd_repl and tl_repl are proved essentially by the same script *) +lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2. +#C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ] +#hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ] +#hd2 #tl2 #_ #Q elim Q // +qed. + +lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2. +#l1 (elim l1) -l1 [ #l2 #Q >Q // ] +#hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ] +#hd2 #tl2 #_ #Q elim Q // +qed. + +lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 → + nth i ? l1 C1 ≅ nth i ? l2 C2. +#C1 #C2 #QC #i (elim i) /3/ +qed. +*) +(* the r.c. for a (dependent) product type. ***********************************) + +definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C. + +lemma dep_cr1: ∀B,C. CR1 (dep_mem B C). +#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort // +qed. + +lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C). +/5/ qed. + +lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C). +/5/ qed. + +(* NOTE: @sat2 is not needed if append_cons is enabled *) +lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C). +#B #C #N #L #M #l #HN #HL #HM #K #HK eqP normalize + >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i) + (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta + |* #M2 * #eqM1 #rP >eqM1 normalize @rappl @Hind /2/ + ] + |* #N2 * #eqM1 #rQ >eqM1 normalize @rappr @Hind /2/ + ] + |#P #Q #Hind #M1 #i #r1 (cases (red_lambda …r1)) + [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/ + |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/ + ] + |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1)) + [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/ + |* #P1 * #eqM1 #redP >eqM1 normalize @rprodr @Hind /2/ + ] + |#P #Hind #M1 #i #r1 (cases (red_d …r1)) + #P1 * #eqM1 #redP >eqM1 normalize @d @Hind /2/ + ] +qed. + +lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n). +#N #N1 #n #r1 (elim r1) normalize /2/ +qed. + +(* star red *) +lemma star_appl: ∀M,M1,N. star … red M M1 → + star … red (App M N) (App M1 N). +#M #M1 #N #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_appr: ∀M,N,N1. star … red N N1 → + star … red (App M N) (App M N1). +#M #N #N1 #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → + star … red (App M N) (App M1 N1). +#M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/ +qed. + +lemma star_laml: ∀M,M1,N. star … red M M1 → + star … red (Lambda M N) (Lambda M1 N). +#M #M1 #N #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_lamr: ∀M,N,N1. star … red N N1 → + star … red (Lambda M N) (Lambda M N1). +#M #N #N1 #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → + star … red (Lambda M N) (Lambda M1 N1). +#M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/ +qed. + +lemma star_prodl: ∀M,M1,N. star … red M M1 → + star … red (Prod M N) (Prod M1 N). +#M #M1 #N #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_prodr: ∀M,N,N1. star … red N N1 → + star … red (Prod M N) (Prod M N1). +#M #N #N1 #star1 (elim star1) // +#B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → + star … red (Prod M N) (Prod M1 N1). +#M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/ +qed. + +lemma star_d: ∀M,M1. star … red M M1 → + star … red (D M) (D M1). +#M #M1 #redM (elim redM) // #B #C #starMB #redBC #H @(inj … H) /2/ +qed. + +lemma red_subst1 : ∀M,N,N1,i. red N N1 → + (star … red) M[i≝N] M[i≝N1]. +#M (elim M) + [// + |#i #P #Q #n #r1 (cases (true_or_false (leb i n))) + [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein))) + [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) // + |#eqin >eqin >subst_rel2 >subst_rel2 @R_to_star /2/ + ] + |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni + >(subst_rel3 … ltni) >(subst_rel3 … ltni) // + ] + |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/ + |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/ + |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/ + |#P #Hind #M #N #i #r1 normalize @star_d /2/ + ] +qed. + +lemma SN_d : ∀M. SN M → SN (D M). +#M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd)) +#Q * #eqa #redbQ >eqa @Hind // +qed. + +lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M. +#N * #b #H #M #red @H //. +qed. + +lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M. +#M #N #rstar (elim rstar) // +#Q #P #HbQ #redQP #snNQ #snN @(SN_step …redQP) /2/ +qed. + +lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 → +∃M1.subterm N1 M1 ∧ red M M1. +#M #N #subN (elim subN) /4/ +(* trsansitive case *) +#P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP)) +#B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC +@(ex_intro … C) /3/ +qed. + +axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 → +∃M1.subterm N1 M1 ∧ red M M1. + +lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N. +#M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN +(cases (sub_red … subNM ? redN)) #M1 * +#subN1M1 #redMM1 @(HindM … redMM1) // +qed. + +lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N. +#M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H +lapply (H Hstar) #Hstari (elim Hstari) // +#M #N #_ #subNM #snM @(SN_subterm …subNM) // +qed. + +definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M. + +definition SH ≝ WF ? shrink. + +lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N. +#M #snM (elim snM) #M +#snM #HindM #N #subNM (cases (star_case ???? subNM)) + [#eqNM >eqNM % /2/ + |#subsNM % #N1 * + [#redN (cases (sub_star_red … subNM ? redN)) #M1 * + #subN1M1 #redMM1 @(HindM M1) /2/ + |#subN1 @(HindM N) /2/ + ] + ] +qed. + +theorem SN_to_SH: ∀N. SN N → SH N. +#N #snN (elim snN) (@Telim_size) +#b #Hsize #snb #Hind % #a * /2/ #subab @Hsize; + [(elim subab) + [#c #subac @size_subterm // + |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm // + ] + |@SN_step @(SN_subterm_star b); + [% /2/ |@TC_to_star @subab] % @snb + |#a1 #reda1 cases(sub_star_red b a ?? reda1); + [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ] + ] +qed. + +lemma SH_to_SN: ∀N. SH N → SN N. +@WF_antimonotonic /2/ qed. + +lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M). +#N #snN (elim snN) #P #shP #HindP #M #snM +(* for M we proceed by induction on SH *) +(lapply (SN_to_SH ? snM)) #shM (elim shM) +#Q #shQ #HindQ % #a #redH (cases (red_lambda … redH)) + [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // + @SH_to_SN % /2/ + |* #S * #eqa #redQS >eqa @(HindQ S) /2/ + ] +qed. + +lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M). +#N #snN (elim snN) #P #shP #HindP #M #snM (elim snM) +#Q #snQ #HindQ % #a #redH (cases (red_prod … redH)) + [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // + % /2/ + |* #S * #eqa #redQS >eqa @(HindQ S) /2/ + ] +qed. + +lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M. +#i #N (cut (∀P.SN P → ∀M.P=M[i ≝ N] → SN M)); + [#P #H (elim H) #Q #snQ #Hind #M #eqM % #M1 #redM + @(Hind M1[i:=N]) // >eqM /2/ + |#Hcut #M #snM @(Hcut … snM) // +qed. + +(* +lemma SN_DAPP: ∀N,M. SN (App M N) → SN (App (D M) N). +cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/] +#P #snP (elim snP) #Q #snQ #Hind +#M #N #eqQ % #A #rA (cases (red_app … rA)) + [* + [* + [* #M1 * #N1 * #eqH destruct + |* #M1 * #eqH destruct #eqA >eqA @SN_d % @snQ + ] + |* #M1 * #eqA #red1 (cases (red_d …red1)) + #M2 * #eqM1 #r2 >eqA >eqM1 @(Hind (App M2 N)) /2/ + ] + |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/ + ] +qed. *) + +lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M. + SN M[0:=N] → SN (App (Lambda P M) N). +#P #snP (elim snP) #A #snA #HindA +#N #snN (elim snN) #B #snB #HindB +#M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM +(generalize in match snM1) (elim shM) +#C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ)) + [* + [* #M2 * #N2 * #eqlam destruct #eqQ // + |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam)) + [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/ + |* #M3 * #eqM2 #r2 >eqM2 @HindC; + [%1 // |@(SN_step … snC1) /2/] + ] + ] + |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1) + @red_subst1 // + ] +qed. + + + + diff --git a/matita/matita/lib/lambdaN/sn.ma b/matita/matita/lib/lambdaN/sn.ma new file mode 100644 index 000000000..a9fbff370 --- /dev/null +++ b/matita/matita/lib/lambdaN/sn.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "lambda/ext_lambda.ma". + +(* STRONGLY NORMALIZING TERMS *************************************************) + +(* SN(t) holds when t is strongly normalizing *) +(* FG: we axiomatize it for now because we dont have reduction yet *) +axiom SN: T → Prop. + +(* lists of strongly normalizing terms *) +definition SNl ≝ all ? SN. + +(* saturation conditions ******************************************************) + +definition CR1 ≝ λ(P:?→Prop). ∀M. P M → SN M. + +definition SAT0 ≝ λ(P:?→Prop). ∀n,l. SNl l → P (Appl (Sort n) l). + +definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l). + +definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → + P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)). + +definition SAT3 ≝ λ(P:?→Prop). ∀M,N,l. P (Appl (D (App M N)) l) → + P (Appl (D M) (N::l)). + +definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M). + +lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n). +#P #n #HP @(HP n (nil ?) …) // +qed. + +lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i). +#P #i #HP @(HP i (nil ?) …) // +qed. + +lemma SAT3_1: ∀P,M,N. SAT3 P → P (D (App M N)) → P (App (D M) N). +#P #M #N #HP #H @(HP … ([])) @H +qed. + +(* axiomatization *************************************************************) + +axiom sn_sort: SAT0 SN. + +axiom sn_rel: SAT1 SN. + +axiom sn_beta: SAT2 SN. + +axiom sn_dapp: SAT3 SN. + +axiom sn_dummy: SAT4 SN. + +axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M). + +axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M). + +axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M. diff --git a/matita/matita/lib/lambdaN/subject.ma b/matita/matita/lib/lambdaN/subject.ma new file mode 100644 index 000000000..be34cb07f --- /dev/null +++ b/matita/matita/lib/lambdaN/subject.ma @@ -0,0 +1,225 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/reduction.ma". +include "lambda/inversion.ma". + +(* +inductive T : Type[0] ≝ + | Sort: nat → T + | Rel: nat → T + | App: T → T → T + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) + | D: T →T +. + +inductive red : T →T → Prop ≝ + | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N]) + | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N) + | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1) + | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N) + | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1) + | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N) + | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1) + | d: ∀M,M1. red M M1 → red (D M) (D M1). *) + +lemma lift_D: ∀M,N. lift M 0 1 = D N → + ∃P. N = lift P 0 1 ∧ M = D P. +#M (cases M) normalize + [#i #N #H destruct + |#i #N #H destruct + |#A #B #N #H destruct + |#A #B #N #H destruct + |#A #B #N #H destruct + |#A #N #H destruct @(ex_intro … A) /2/ + ] +qed. + +theorem type_of_type: ∀P,G,A,B. G ⊢_{P} A : B → (∀i. B ≠ Sort i) → + ∃i. G ⊢_{P} B : Sort i. +#Pts #G #A #B #t (elim t) + [#i #j #Aij #j @False_ind /2/ + |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1) + |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) ) + [#i #Bi @(ex_intro … i) @(weak … Bi t2) + |#i @(not_to_not … (H3 i)) // + ] + |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/ + |#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?); + [#i #t3 cases (prod_inv … t3 … (refl …)) + #s1 * #s2 * #s3 * * #Ci #H4 #H5 @(ex_intro … s2) + @(tj_subst_0 … t2 … H5) + |#i % #H destruct + ] + |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 /2/ + |#G1 #A #B #C #i #ch #t1 #t2 #H1 #H2 #H3 /2/ + |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #H /2/ + ] +qed. + +lemma prod_sort : ∀Pts,G,M,P,Q. G ⊢_{Pts} M :Prod P Q → + ∃i. P::G ⊢_{Pts} Q : Sort i. +#Pts #G #M #P #Q #t cases(type_of_type …t ?); + [#s #t2 cases(prod_inv … t2 …(refl …)) #s1 * #s2 * #s3 * * + #_ #_ #H @(ex_intro … s2) // + | #i % #H destruct + ] +qed. + +axiom red_lift: ∀M,N. red (lift M 0 1) N → + ∃P. N = lift P 0 1 ∧ red M P. + +theorem tj_d : ∀P,G,M,N. G ⊢_{P} D M : N → G ⊢_{P} M : N. +#Pts #G (cut (∀M,N. G ⊢_{Pts} M : N → ∀P. M = D P → G ⊢_{Pts} P : N)) [2: /2/] +#M #N #t (elim t) + [#i #j #Aij #P #H destruct + |#G1 #A #i #t1 #_ #P #H destruct + |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #H3 + cases (lift_D … H3) #P * #eqP #eqA >eqP @(weak … i) /2/ + |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P #H destruct + |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct + |#G1 #A #B #C #D #t1 #t2 #_ #_ #P #H destruct + |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #H + @(conv… ch …t2) /2/ + |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #H destruct // + ] +qed. + +definition red0 ≝ λM,N. M = N ∨ red M N. + +axiom conv_lift: ∀P,i,M,N. Co P M N → + Co P (lift M 0 i) (lift N 0 i). +axiom red_to_conv : ∀P,M,N. red M N → Co P M N. +axiom red0_to_conv : ∀P,M,N. red0 M N → Co P M N. +axiom conv_prod: ∀P,A,B,M,N. Co P A B → Co P M N → + Co P (Prod A M) (Prod B N). +axiom conv_subst_1: ∀Pts,M,P,Q. red P Q → Co Pts (M[0≝Q]) (M[0≝P]). + +inductive redG : list T → list T → Prop ≝ + | rnil : redG (nil T) (nil T) + | rstep : ∀A,B,G1,G2. red0 A B → redG G1 G2 → + redG (A::G1) (B::G2). + +lemma redG_inv: ∀A,G,G1. redG (A::G) G1 → + ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2. +#A #G #G1 #rg (inversion rg) + [#H destruct + |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct + #H1 @(ex_intro … B1) @(ex_intro … G3) % // % // + ] +qed. + +lemma redG_nil: ∀G. redG (nil T) G → G = nil T. +#G #rg (inversion rg) // +#A #B #G1 #G2 #r1 #r2 #_ #H destruct +qed. + +axiom conv_prod_split: ∀P,A,A1,B,B1. + Co P(Prod A B) (Prod A1 B1) → Co P A A1 ∧ Co P B B1. + +axiom red0_prod : ∀M,N,P. red0 (Prod M N) P → + (∃Q. P = Prod Q N ∧ red0 M Q) ∨ + (∃Q. P = Prod M Q ∧ red0 N Q). + +theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N → + ∀M1. red0 M M1 → ∀G1. redG G G1 → G1 ⊢_{P} M1:N. +#Pts #G #M #N #d (elim d) + [#i #j #Aij #M1 * + [#eqM1 (redG_nil …H) /2/ + |#H @False_ind /2/ + ] + |#G1 #A #i #t1 #Hind #M1 * + [#eqM1 eqG2 + @(conv ??? (lift P O 1) ? i); + [@conv_lift @sym_conv @red0_to_conv // + |@(start … i) @Hind // + |@(weak … (Sort i) ? i); [@Hind /2/ | @Hind //] + ] + |#H @False_ind /2/ + ] + |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #M1 + #H cases H; + [#eqM1 eqG2 @(weak … i); + [@H1 /2/ | @H2 //] + |#H (elim (red_lift … H)) #P * #eqM1 >eqM1 #redAP + #G2 #rg (cases (redG_inv … rg)) #Q * #G3 * * #r2 + #rg1 #eqG2 >eqG2 @(weak … i); + [@H1 /2/ | @H2 //] + ] + |#G #A #B #i #j #k #Rjk #t1 #t2 #Hind1 #Hind2 #M1 #redP + (cases (red0_prod … redP)) + [* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk); + [@Hind1 // | @Hind2 /2/] + |* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk); + [@Hind1 /2/ | @Hind2 /3/] + ] + |#G #A #B #C #P #t1 #t2 #Hind1 #Hind2 #M1 #red0a + (cases red0a) + [#eqM1 eqM1 #G1 #rg + cut (G1 ⊢_{Pts} A: Prod B C); [@Hind1 /2/] #H1 + (cases (abs_inv … H1 … eqA)) #i * #N2 * * + #cProd #t3 #t4 + (cut (Co Pts B M2 ∧ Co Pts C N2) ) [/2/] * #convB #convC + (cases (prod_inv … t3 … (refl …) )) #i * #j * #k * * + #cik #t5 #t6 (cut (G1 ⊢_{Pts} P:B)) + [@Hind2 /2/ + |#Hcut cut (G1 ⊢_{Pts} N1[0:=P] : N2 [0:=P]); + [@(tj_subst_0 … M2) // @(conv … convB Hcut t5) + |#Hcut1 cases (prod_sort … H1) #s #Csort + @(conv … s … Hcut1); + [@conv_subst /2/ | @(tj_subst_0 … Csort) //] + ] + ] + |* #M2 * #eqM1 >eqM1 #H #G1 #rg @(app … B); + [@Hind1 /2/ | @Hind2 /2/] + ] + |* #M2 * #eqM1 >eqM1 #H #G1 #rg + cut (G1 ⊢_{Pts} A:Prod B C); [@Hind1 /2/] #t3 + cases (prod_sort …t3) #i #Csort @(conv ??? C[O≝ M2] … i); + [@conv_subst_1 // + |@(app … B) // @Hind2 /2/ + |@(tj_subst_0 … Csort) @Hind2 /2/ + ] + ] + ] + |#G #A #B #C #i #t1 #t2 #Hind1 #Hind2 #M2 #red0l #G1 #rg + cut (A::G1⊢_{Pts} C:B); [@Hind1 /3/] #t3 + cut (G1 ⊢_{Pts} Prod A B : Sort i); [@Hind2 /2/] #t4 + cases red0l; + [#eqM2 eqM2 + @(conv ??? (Prod M3 B) … t4); + [@conv_prod /2/ + |@(abs … i); [@Hind1 /3/ |@Hind2 /3/] + ] + |* #M3 * #eqM3 #redC >eqM3 + @(abs … t4) @Hind1 /3/ + ] + ] + |#G #A #B #C #i #convBC #t1 #t2 #Hind1 #Hind2 #M1 #redA + #G1 #rg @(conv … i … convBC); [@Hind1 // |@Hind2 /2/] + |#G #A #B #i #t1 #t2 #Hind1 #Hind2 #M1 #red0d #G1 #rg + cases red0d; + [#eqM1 eqM1 + @(dummy … i);[@Hind1 /2/ |@Hind2 /2/] + ] +qed. + diff --git a/matita/matita/lib/lambdaN/subst.ma b/matita/matita/lib/lambdaN/subst.ma new file mode 100644 index 000000000..ac0480224 --- /dev/null +++ b/matita/matita/lib/lambdaN/subst.ma @@ -0,0 +1,298 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/terms.ma". + +(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *) +let rec lift t k p ≝ + match t with + [ Sort n ⇒ Sort n + | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p)) + | App m n ⇒ App (lift m k p) (lift n k p) + | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p) + | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p) + | D n ⇒ D (lift n k p) + ]. + +(* +ndefinition lift ≝ λt.λp.lift_aux t 0 p. + +notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}. +notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}. +*) +(* interpretation "Lift" 'Lift n M = (lift M n). *) +interpretation "Lift" 'Lift n k M = (lift M k n). + +let rec subst t k a ≝ + match t with + [ Sort n ⇒ Sort n + | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) + (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1))) + | App m n ⇒ App (subst m k a) (subst n k a) + | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a) + | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a) + | D n ⇒ D (subst n k a) + ]. + +(* meglio non definire +ndefinition subst ≝ λa.λt.subst_aux t 0 a. +notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}. +*) + +(* interpretation "Subst" 'Subst N M = (subst N M). *) +interpretation "Subst" 'Subst1 M k N = (subst M k N). + +(*** properties of lift and subst ***) + +lemma lift_0: ∀t:T.∀k. lift t k 0 = t. +#t (elim t) normalize // #n #k cases (leb (S n) k) normalize // +qed. + +(* nlemma lift_0: ∀t:T. lift t 0 = t. +#t; nelim t; nnormalize; //; nqed. *) + +lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i. +// qed. + +lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n). +// qed. + +lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i). +#i (change with (lift (Rel i) 0 1 = Rel (1 + i))) // +qed. + +lemma lift_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i. +#n #k #i #ltik change with +(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel i) +>(le_to_leb_true … ltik) // +qed. + +lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n). +#n #k #i #leki change with +(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel (i+n)) +>lt_to_leb_false // @le_S_S // +qed. + +lemma lift_lift: ∀t.∀m,j.j ≤ m → ∀n,k. + lift (lift t k m) (j+k) n = lift t k (m+n). +#t #i #j #h (elim t) normalize // #n #h #k +@(leb_elim (S n) k) #Hnk normalize + [>(le_to_leb_true (S n) (j+k) ?) normalize /2/ + |>(lt_to_leb_false (S n+i) (j+k) ?) + normalize // @le_S_S >(commutative_plus j k) + @le_plus // @not_lt_to_le /2/ + ] +qed. + +lemma lift_lift_up: ∀n,m,t,k,i. + lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m. +#n #m #N (elim N) + [1,3,4,5,6: normalize // + |#p #k #i @(leb_elim i p); + [#leip >lift_rel_ge // @(leb_elim (k+i) p); + [#lekip >lift_rel_ge; + [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) // + |>associative_plus >commutative_plus @monotonic_le_plus_l // + ] + |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki + >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //] + >lift_rel_lt // >lift_rel_ge // + ] + |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi + >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] + >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] + >lift_rel_lt // + ] + ] +qed. + +lemma lift_lift1: ∀t.∀i,j,k. + lift(lift t k j) k i = lift t k (j+i). +/2/ qed. + +lemma lift_lift2: ∀t.∀i,j,k. + lift (lift t k j) (j+k) i = lift t k (j+i). +/2/ qed. + +(* +nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i). +nnormalize; //; nqed. *) + +lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B. +#A #B (elim B) normalize /2/ #n #k +@(leb_elim (S n) k) normalize #Hnk + [>(le_to_leb_true ?? Hnk) normalize // + |>(lt_to_leb_false (S (n + 1)) k ?) normalize + [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/ + |@le_S (applyS (not_le_to_lt (S n) k Hnk)) + ] + ] +qed. + +(* +nlemma subst_lift: ∀A,B. subst A (lift B 1) = B. +nnormalize; //; nqed. *) + +lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n. +// qed. + +lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A. +normalize // qed. + +lemma subst_rel1: ∀A.∀k,i. i < k → + (Rel i) [k ≝ A] = Rel i. +#A #k #i normalize #ltik >(le_to_leb_true (S i) k) // +qed. + +lemma subst_rel2: ∀A.∀k. + (Rel k) [k ≝ A] = lift A 0 k. +#A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) // +qed. + +lemma subst_rel3: ∀A.∀k,i. k < i → + (Rel i) [k ≝ A] = Rel (i-1). +#A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/ +>(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq // +qed. + +lemma lift_subst_ijk: ∀A,B.∀i,j,k. + lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A]. +#A #B #i #j (elim B) normalize /2/ #n #k +@(leb_elim (S n) (j + k)) normalize #Hnjk + [(elim (leb (S n) k)) + [>(subst_rel1 A (j+k+i) n) /2/ + |>(subst_rel1 A (j+k+i) (n+i)) /2/ + ] + |@(eqb_elim n (j+k)) normalize #Heqnjk + [>(lt_to_leb_false (S n) k); + [(cut (j+k+i = n+i)) [//] #Heq + >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) // + |/2/ + ] + |(cut (j + k < n)) + [@not_eq_to_le_to_lt; + [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ] + |#ltjkn + (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn + >(lt_to_leb_false (S (n-1)) k) normalize + [>(lt_to_leb_false … (le_S_S … lekn)) + >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/] + |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b // + ] + ] + ] +qed. + +lemma lift_subst_up: ∀M,N,n,i,j. + lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)]. +#M (elim M) + [// + |#p #N #n #i #j (cases (true_or_false (leb p i))) + [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi))) + [#ltpi >(subst_rel1 … ltpi) + (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij + >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?); + [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //] + |#eqpi >eqpi >subst_rel2 >lift_rel_lt; + [>subst_rel2 >(plus_n_O (i+j)) + applyS lift_lift_up + |@(le_to_lt_to_lt ? (i+j)) // + ] + ] + |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip + (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp + >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1)))) + [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt + >lift_rel_lt; + [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //] + |#Hfalse >lift_rel_ge; + [>lift_rel_ge; + [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //] + |@not_lt_to_le @(leb_false_to_not_le … Hfalse) + ] + |@le_plus_to_minus_r @not_lt_to_le + @(leb_false_to_not_le … Hfalse) + ] + ] + ] + |#P #Q #HindP #HindQ #N #n #i #j normalize + @eq_f2; [@HindP |@HindQ ] + |#P #Q #HindP #HindQ #N #n #i #j normalize + @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1) + associative_plus >(commutative_plus j 1) + (le_to_leb_true (S n) j) /2/ + |>(lt_to_leb_false (S (n+S k)) j); + [normalize >(not_eq_to_eqb_false (n+S k) j)normalize + /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize // + |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/ + ] + ] + ] +qed. + +(********************* substitution lemma ***********************) + +lemma subst_lemma: ∀A,B,C.∀k,i. + (A [i ≝ B]) [k+i ≝ C] = + (A [S (k+i) := C]) [i ≝ B [k ≝ C]]. +#A #B #C #k (elim A) normalize // (* WOW *) +#n #i @(leb_elim (S n) i) #Hle + [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len + >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) // + |@(eqb_elim n i) #eqni + [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …); + normalize @sym_eq (applyS (lift_subst_ijk C B i k O)) + |@(leb_elim (S (n-1)) (k+i)) #nk + [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i)); + [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt; + [/2/ |@not_lt_to_le /2/] + |@(transitive_le … nk) // + ] + |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)] + #ltin (cut (O < n)) [/2/] #posn + @(eqb_elim (n-1) (k+i)) #H + [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i)); + [>(eq_to_eqb_true n (S(k+i))); + [normalize |delift normalize /2/ + |(lt_to_leb_false n (k+i)); + [>(not_eq_to_eqb_false n (S(k+i))); + [>(subst_rel3 C (k+i) (n-1) Hlt); + >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) // + |@(not_to_not … H) #Hn >Hn normalize // + ] + |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize // + ] + ] + ] + ] + ] +qed. diff --git a/matita/matita/lib/lambdaN/subterms.ma b/matita/matita/lib/lambdaN/subterms.ma new file mode 100644 index 000000000..d2b7bee30 --- /dev/null +++ b/matita/matita/lib/lambdaN/subterms.ma @@ -0,0 +1,156 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/subst.ma". + +inductive subterm : T → T → Prop ≝ + | appl : ∀M,N. subterm M (App M N) + | appr : ∀M,N. subterm N (App M N) + | lambdal : ∀M,N. subterm M (Lambda M N) + | lambdar : ∀M,N. subterm N (Lambda M N) + | prodl : ∀M,N. subterm M (Prod M N) + | prodr : ∀M,N. subterm N (Prod M N) + | sub_b : ∀M. subterm M (D M) + | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P. + +inverter subterm_myinv for subterm (?%). + +lemma subapp: ∀S,M,N. subterm S (App M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [#M1 #N1 #eqapp destruct /4/ + |#M1 #N1 #eqapp destruct /4/ + |3,4,5,6: #M1 #N1 #eqapp destruct + |#M1 #eqapp destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqapp + (cases (H2 eqapp)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma sublam: ∀S,M,N. subterm S (Lambda M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [1,2,5,6: #M1 #N1 #eqH destruct + |3,4:#M1 #N1 #eqH destruct /4/ + |#M1 #eqH destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH + (cases (H2 eqH)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma subprod: ∀S,M,N. subterm S (Prod M N) → + S = M ∨ S = N ∨ subterm S M ∨ subterm S N. +#S #M #N #subH (@(subterm_myinv … subH)) + [1,2,3,4: #M1 #N1 #eqH destruct + |5,6:#M1 #N1 #eqH destruct /4/ + |#M1 #eqH destruct + |#M1 #N1 #P #sub1 #sub2 #H1 #H2 #eqH + (cases (H2 eqH)) + [* [* /3/ | #subN1 %1 %2 /2/ ] + |#subN1 %2 /2/ + ] + ] +qed. + +lemma subd: ∀S,M. subterm S (D M) → + S = M ∨ subterm S M. +#S #M #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqH destruct /2/ + |#M1 #N1 #P #sub1 #sub2 #_ #H #eqH + (cases (H eqH)) /2/ + #subN1 %2 /2/ + ] +qed. + +lemma subsort: ∀S,n. ¬ subterm S (Sort n). +#S #n % #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqa destruct + |/2/ + ] +qed. + +lemma subrel: ∀S,n. ¬ subterm S (Rel n). +#S #n % #subH (@(subterm_myinv … subH)) + [1,2,3,4,5,6: #M1 #N1 #eqH destruct + |#M1 #eqa destruct + |/2/ + ] +qed. + +theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) → + ∀M. P M. +#P #H #M (cut (P M ∧ (∀N. subterm N M → P N))) + [2: * //] +(elim M) + [#n % + [@H #N1 #subN1 @False_ind /2/ + |#N #subN1 @False_ind /2/ + ] + |#n % + [@H #N1 #subN1 @False_ind /2/ + |#N #subN1 @False_ind /2/ + ] + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (App M1 M2) → P N)) + [#N1 #subN1 (cases (subapp … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (Lambda M1 M2) → P N)) + [#N1 #subN1 (cases (sublam … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 #M2 * #PM1 #Hind1 * #PM2 #Hind2 + (cut (∀N.subterm N (Prod M1 M2) → P N)) + [#N1 #subN1 (cases (subprod … subN1)) + [* [* // | @Hind1 ] | @Hind2 ]] + #Hcut % /3/ + |#M1 * #PM1 #Hind1 + (cut (∀N.subterm N (D M1) → P N)) + [#N1 #subN1 (cases (subd … subN1)) /2/] + #Hcut % /3/ + ] +qed. + +let rec size M ≝ +match M with + [Sort N ⇒ 1 + |Rel N ⇒ 1 + |App P Q ⇒ size P + size Q + 1 + |Lambda P Q ⇒ size P + size Q + 1 + |Prod P Q ⇒ size P + size Q + 1 + |D P ⇒ size P + 1 + ] +. + +(* axiom pos_size: ∀M. 1 ≤ size M. *) + +theorem Telim_size: ∀P: T → Prop. + (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M. +#P #H #M (cut (∀p,N. size N = p → P N)) + [2: /2/] +#p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) // +qed. + +(* size of subterms *) + +lemma size_subterm : ∀N,M. subterm N M → size N < size M. +#N #M #subH (elim subH) normalize // +#M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2) +qed. diff --git a/matita/matita/lib/lambdaN/terms.ma b/matita/matita/lib/lambdaN/terms.ma new file mode 100644 index 000000000..554f8099c --- /dev/null +++ b/matita/matita/lib/lambdaN/terms.ma @@ -0,0 +1,51 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "basics/list.ma". +include "lambda/lambda_notation.ma". + +inductive T : Type[0] ≝ + | Sort: nat → T (* starts from 0 *) + | Rel: nat → T (* starts from 0 *) + | App: T → T → T (* function, argument *) + | Lambda: T → T → T (* type, body *) + | Prod: T → T → T (* type, body *) + | D: T → T (* dummifier *) +. + +(* Appl F l generalizes App applying F to a list of arguments + * The head of l is applied first + *) +let rec Appl F l on l ≝ match l with + [ nil ⇒ F + | cons A D ⇒ Appl (App F A) D + ]. + +lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N. +#N #l elim l -l // #hd #tl #IHl #M >IHl // +qed. + +(* +let rec is_dummy t ≝ match t with + [ Sort _ ⇒ false + | Rel _ ⇒ false + | App M _ ⇒ is_dummy M + | Lambda _ M ⇒ is_dummy M + | Prod _ _ ⇒ false (* not so sure yet *) + | D _ ⇒ true + ]. +*) +(* nautral terms *) +inductive neutral: T → Prop ≝ + | neutral_sort: ∀n.neutral (Sort n) + | neutral_rel: ∀i.neutral (Rel i) + | neutral_app: ∀M,N.neutral (App M N) +. diff --git a/matita/matita/lib/lambdaN/types.ma b/matita/matita/lib/lambdaN/types.ma new file mode 100644 index 000000000..0c07d2e70 --- /dev/null +++ b/matita/matita/lib/lambdaN/types.ma @@ -0,0 +1,192 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda/subst.ma". +include "basics/list.ma". + + +(*************************** substl *****************************) + +let rec substl (G:list T) (N:T) : list T ≝ + match G with + [ nil ⇒ nil T + | cons A D ⇒ ((subst A (length T D) N)::(substl D N)) + ]. + +(* +nlemma substl_cons: ∀A,N.∀G. +substl (A::G) N = (subst_aux A (length T G) N)::(substl G N). +//; nqed. +*) + +(*start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1) + | +nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1. +/2/; nqed.*) + +(****************************************************************) + +(* +axiom A: nat → nat → Prop. +axiom R: nat → nat → nat → Prop. +axiom conv: T → T → Prop.*) + +record pts : Type[0] ≝ { + Ax: nat → nat → Prop; + Re: nat → nat → nat → Prop; + Co: T → T → Prop + }. + +inductive TJ (p: pts): list T → T → T → Prop ≝ + | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j) + | start: ∀G.∀A.∀i.TJ p G A (Sort i) → + TJ p (A::G) (Rel 0) (lift A 0 1) + | weak: ∀G.∀A,B,C.∀i. + TJ p G A B → TJ p G C (Sort i) → + TJ p (C::G) (lift A 0 1) (lift B 0 1) + | prod: ∀G.∀A,B.∀i,j,k. Re p i j k → + TJ p G A (Sort i) → TJ p (A::G) B (Sort j) → + TJ p G (Prod A B) (Sort k) + | app: ∀G.∀F,A,B,a. + TJ p G F (Prod A B) → TJ p G a A → + TJ p G (App F a) (subst B 0 a) + | abs: ∀G.∀A,B,b.∀i. + TJ p (A::G) b B → TJ p G (Prod A B) (Sort i) → + TJ p G (Lambda A b) (Prod A B) + | conv: ∀G.∀A,B,C.∀i. Co p B C → + TJ p G A B → TJ p G C (Sort i) → TJ p G A C + | dummy: ∀G.∀A,B.∀i. + TJ p G A B → TJ p G B (Sort i) → TJ p G (D A) B. + +interpretation "generic type judgement" 'TJT P G A B = (TJ P G A B). + +notation "hvbox( G break ⊢ _{P} A break : B)" + non associative with precedence 45 + for @{'TJT $P $G $A $B}. + +(* ninverter TJ_inv2 for TJ (%?%) : Prop. *) + +(**** definitions ****) + +inductive Glegal (P:pts) (G: list T) : Prop ≝ +glegalk : ∀A,B. G ⊢_{P} A : B → Glegal P G. + +inductive Gterm (P:pts) (G: list T) (A:T) : Prop ≝ + | is_term: ∀B.G ⊢_{P} A:B → Gterm P G A + | is_type: ∀B.G ⊢_{P} B:A → Gterm P G A. + +inductive Gtype (P:pts) (G: list T) (A:T) : Prop ≝ +gtypek: ∀i.G ⊢_{P} A : Sort i → Gtype P G A. + +inductive Gelement (P:pts) (G:list T) (A:T) : Prop ≝ +gelementk: ∀B.G ⊢_{P} A:B → Gtype P G B → Gelement P G A. + +inductive Tlegal (P:pts) (A:T) : Prop ≝ +tlegalk: ∀G. Gterm P G A → Tlegal P A. + +(* +ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B . + +ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A. + +ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i). + +ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B. + +ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A. +*) + +(* +ntheorem free_var1: ∀G.∀A,B,C. TJ G A B → +subst C A +#G; #i; #j; #axij; #Gleg; ncases Gleg; +#A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed. +*) + +theorem start_lemma1: ∀P,G,i,j. +Ax P i j → Glegal P G → G ⊢_{P} Sort i: Sort j. +#P #G #i #j #axij #Gleg (cases Gleg) +#A #B #tjAB (elim tjAB) /2/ +(* bello *) qed. + +theorem start_rel: ∀P,G,A,C,n,i,q. +G ⊢_{P} C: Sort q → G ⊢_{P} Rel n: lift A 0 i → + C::G ⊢_{P} Rel (S n): lift A 0 (S i). +#P #G #A #C #n #i #p #tjC #tjn + (applyS (weak P G (Rel n))) //. +qed. + +theorem start_lemma2: ∀P,G. +Glegal P G → ∀n. n < |G| → G ⊢_{P} Rel n: lift (nth n T G (Rel O)) 0 (S n). +#P #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/ + [#i #j #axij #p normalize #abs @(False_ind) @(absurd … abs) // + |#G #A #i #tjA #Hind #m (cases m) /2/ + #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle + |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m) + /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle + ] +qed. + +axiom conv_subst: ∀T,P,Q,N,i.Co T P Q → Co T P[i := N] Q[i := N]. + +theorem substitution_tj: +∀P,E.∀A,B,M. E ⊢_{P} M:B → ∀G,D.∀N. E = D@A::G → G ⊢_{P} N:A → + ((substl D N)@G) ⊢_{P} M[|D| := N]: B[|D| := N]. +#Pts #E #A #B #M #tjMB (elim tjMB) + [normalize #i #j #k #G #D #N (cases D) + [normalize #isnil destruct + |#P #L normalize #isnil destruct + ] + |#G #A1 #i #tjA #Hind #G1 #D (cases D) + [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) // + (normalize in Heq) destruct /2/ + |#H #L #N1 #Heq (normalize in Heq) + #tjN1 normalize destruct; (applyS start) /2/ + ] + |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N + (cases D) normalize + [#Heq destruct #tjN // + |#H #L #Heq #tjN1 destruct; + (* napplyS weak non va *) + (cut (S (length T L) = (length T L)+0+1)) [//] + #Hee (applyS weak) /2/ + ] + |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN normalize @(prod … Ax); + [/2/ + |(cut (S (length T D) = (length T D)+1)) [//] + #Heq1 (plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?)) + >(subst_lemma R S N ? 0) (applyS app) /2/ + |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2 + #G1 #D #N #Heq #tjN normalize + (applyS abs) + [normalize in Hind2 /2/ + |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *) + generalize in match (Hind1 G1 (P::D) N ? tjN); + [#H (normalize in H) (applyS H) | normalize // ] + ] + |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN + @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 // + |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2 + #G1 #D #N #Heq #tjN @dummy /2/ + ] +qed. + +lemma tj_subst_0: ∀P,G,v,w. G ⊢_{P} v : w → ∀t,u. w :: G ⊢_{P} t : u → + G ⊢_{P} t[0≝v] : u[0≝v]. +#P #G #v #w #Hv #t #u #Ht +lapply (substitution_tj … Ht ? ([]) … Hv) normalize // +qed. -- 2.39.2