∀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)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_eq | skip ]
+ @transitive_ameq; [2: @Hx | skip ]
+ @symmetric_ameq //
+ | @transitive_ameq; [2: @(const_neq … H) | skip ]
+ @transitive_ameq; [2: @invariant_sort_mem | skip ]
+ @symmetric_ameq /2/
+ ]
+qed.
+
+lemma aapp_comp: ∀C,a1,a2,b1,b2. a1 ≅ a2 → b1 ≅ b2 → aapp C a1 b1 ≅ aapp C a2 b2.
+#C #a1 #a2 #b1 #b2 #Ha #Hb #D @(Ha (FUN C D)) //
+qed.
+
+lemma aabst_comp: ∀f1,f2. (∀a1,a2. a1 ≅ a2 → f1 a1 ≅ f2 a2) →
+ aabst f1 ≅ aabst f2.
+#f1 #f2 #H #C elim C -C // #B #A #_ #_ #b1 #b2 #Hb @H /2/
+qed.
+
+lemma invariant_sort: ! sort.
+normalize //
+qed.
+
+(* "is a constant arity" *)
+definition isc ≝ λa,A. const ? (a A) ≅ a.
+
+lemma isc_sort: ∀A. isc sort A.
+#A #C elim (decidable_MEq A C) #H [ <H // | /2 by const_neq/ ].
+qed.
+
+lemma isc_aapp: ∀B,A,b,a. ! b B → isc a A → isc (aapp B a b) (pred A).
+#B #A #b #a #Hb #Ha #C elim (decidable_MEq (pred 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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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) <associative_append
+ >(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) <minus_n_n >(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;
+ [ <minus_plus // | <HKk -HKk Kk @not_le_to_not_le_S_S /3/ ]
+ ]
+ ]
+ | #M #N #IHM #_ #k #Kk #HKk >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) <minus_n_n
+ >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);
+ [ <minus_plus /2/ | @not_le_to_not_le_S_S /3/ ]
+ ]
+ ]
+ | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #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.
+*)
--- /dev/null
+(*
+ ||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) % // % //
+ ]
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 <minus_Sn_m /2/
+qed.
+
+(* lists **********************************************************************)
+
+lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
+#A #l2 #l1 elim l1 -l1; normalize //
+qed.
+
+(* all(?,P,l) holds when P holds for all members of l *)
+let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with
+ [ nil ⇒ True
+ | cons hd tl ⇒ P hd ∧ all A P tl
+ ].
+
+lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
+#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl // ]
+qed.
+
+lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l → all … P (tail … l).
+#A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl //
+qed.
+
+lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
+#A #P #a #Ha #i elim i -i [ @all_hd // | #i #IH #l #Hl @IH /2/ ]
+qed.
+
+lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
+#A #P #l2 #l1 elim l1 -l1; normalize // #hd #tl #IH1 #H elim H -H /3/
+qed.
+
+(* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
+let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with
+ [ nil ⇒ l2 = nil ?
+ | cons hd1 tl1 ⇒ match l2 with
+ [ nil ⇒ False
+ | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2
+ ]
+ ].
+
+lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop.
+ ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
+#A #B #P #l1 elim l1 -l1 [ #l2 #H >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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(*
+ ||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) <eqA <eqB %
+ [% [@(conv_lift … c1) |@(weak … t3 t2)]
+ |@(weak_in … t4 t2)
+ ]
+ |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #B1 #H destruct
+ @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % // % //
+ |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #B1 #H destruct
+ |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #B1 #H destruct
+ |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #B1 #eqA
+ cases (H1 … eqA) #i * #j * #k * * #c1 #t3 #t4
+ @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % //
+ % // @(trans_conv Pts C B … c1) @sym_conv //
+ |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #B1 #eqA destruct
+ ]
+qed.
+
+theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b →
+ ∃i,B. Co P N (Prod A B) ∧ G ⊢_{P} Prod A B: Sort i ∧ A::G ⊢_{P} b : B.
+#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 (lambda_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
+ cases (H1 … eqP) #i * #B1 * * #c1 #t3 #t4
+ @(ex_intro … i) @(ex_intro … (lift B1 1 1)) <eqA <eqb %
+ [% [@(conv_lift … c1) |@(weak … t3 t2)]
+ |@(weak_in … t4 t2)
+ ]
+ |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
+ |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
+ @(ex_intro … i) @(ex_intro … A) % // % //
+ |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
+ cases (H1 … eqA) #i * #B1 * * #c1 #t3 #t4
+ @(ex_intro … i) @(ex_intro … B1) % //
+ % // @(trans_conv Pts C B … c1) @sym_conv //
+ |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
+ ]
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE LAMBDA CALCULUS *)
+(* equivalence, invariance *)
+
+notation "hvbox(a break ≅ b)"
+ non associative with precedence 45
+ for @{'Eq $a $b}.
+
+notation "hvbox(a break (≅ ^ term 90 c) b)"
+ non associative with precedence 45
+ for @{'Eq1 $c $a $b}.
+
+notation "hbox(! term 50 a)"
+ non associative with precedence 50
+ for @{'Invariant $a}.
+
+notation "hbox((! ^ term 90 b) term 50 a)"
+ non associative with precedence 50
+ for @{'Invariant1 $a $b}.
+
+(* lifting, substitution *)
+
+notation "hvbox(↑ [ p break , k ] break t)"
+ non associative with precedence 50
+ for @{'Lift1 $p $k $t}.
+
+notation "hvbox(M break [ / l ])"
+ non associative with precedence 90
+ for @{'Subst $M $l}.
+
+notation "hvbox(M break [ k ≝ N ])"
+ non associative with precedence 90
+ for @{'Subst1 $M $k $N}.
+
+(* type judgements *)
+
+notation "hvbox(G break ⊢ A break : B)"
+ non associative with precedence 45
+ for @{'TJ $G $A $B}.
+
+notation "hvbox(G break ⊢ A break ÷ B)"
+ non associative with precedence 45
+ for @{'TJ0 $G $A $B}.
+
+(* interpretations *)
+
+notation "hvbox(║T║)"
+ non associative with precedence 50
+ for @{'IInt $T}.
+
+notation "hvbox(║T║ break _ [E])"
+ non associative with precedence 50
+ for @{'IInt1 $T $E}.
+
+notation "hvbox(║T║ break _ [E1 break , E2])"
+ non associative with precedence 50
+ for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(〚T〛)"
+ non associative with precedence 50
+ for @{'EInt $T}.
+
+notation "hvbox(〚T〛 break _ [E])"
+ non associative with precedence 50
+ for @{'EInt1 $T $E}.
+
+notation "hvbox(〚T〛 break _ [E1 break , E2])"
+ non associative with precedence 50
+ for @{'EInt2 $T $E1 $E2}.
+
+notation "hvbox(《T》)"
+ non associative with precedence 50
+ for @{'XInt $T}.
+
+notation "hvbox(《T》 break _ [E])"
+ non associative with precedence 50
+ for @{'XInt1 $T $E}.
+
+notation "hvbox(《T》 break _ [E1 break , E2])"
+ non associative with precedence 50
+ for @{'XInt2 $T $E1 $E2}.
--- /dev/null
+(*
+ ||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/subterms.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
+. *)
+
+(*
+let rec is_dummy M ≝
+match M with
+ [D P ⇒ true
+ |_ ⇒ false
+ ]. *)
+
+let rec is_lambda M ≝
+match M with
+ [Lambda P Q ⇒ true
+ |_ ⇒ false
+ ].
+
+(*
+theorem is_dummy_to_exists: ∀M. is_dummy M = true →
+∃N. M = D N.
+#M (cases M) normalize
+ [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
+ |#N #_ @(ex_intro … N) //
+ ]
+qed.*)
+
+theorem is_lambda_to_exists: ∀M. is_lambda M = true →
+∃P,N. M = Lambda P N.
+#M (cases M) normalize
+ [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
+ |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
+ ]
+qed.
+
+inductive pr : T →T → Prop ≝
+ | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
+ pr (App (Lambda P M) N) (M1[0 ≝ N1])
+ | none: ∀M. pr M M
+ | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
+ | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 →
+ pr (Lambda P M) (Lambda P1 M1)
+ | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 →
+ pr (Prod P M) (Prod P1 M1)
+ | d: ∀M,M1. pr M M1 → pr (D M) (D M1).
+
+lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
+#M #n #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |//
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
+#M #n #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |//
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
+#M #N #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |#M #eqM #_ @(ex_intro … N) /2/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
+ ]
+qed.
+
+lemma prApp_not_lambda:
+∀M,N,P. pr (App M N) P → is_lambda M = false →
+ ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
+#M #N #P #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #H1 destruct
+ |#M1 #eqM1 #_ #_ @(ex_intro … M) @(ex_intro … N) /3/
+ |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ destruct
+ @(ex_intro … N1) @(ex_intro … N2) /3/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prApp_lambda:
+∀Q,M,N,P. pr (App (Lambda Q M) N) P →
+ ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
+ (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
+#Q #M #N #P #prH (inversion prH)
+ [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_
+ @(ex_intro … M1) @(ex_intro … N1) /4/
+ |#M1 #eqM1 #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/
+ |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
+ @(ex_intro … N1) @(ex_intro … N2) /4/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
+ ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
+#M #N #P #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
+ @(ex_intro … Q1) @(ex_intro … S1) /3/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma prProd: ∀M,N,P. pr (Prod M N) P →
+ ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
+#M #N #P #prH (inversion prH)
+ [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
+ |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
+ |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
+ @(ex_intro … Q1) @(ex_intro … S1) /3/
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+let rec full M ≝
+ match M with
+ [ Sort n ⇒ Sort n
+ | Rel n ⇒ Rel n
+ | App P Q ⇒ full_app P (full Q)
+ | Lambda P Q ⇒ Lambda (full P) (full Q)
+ | Prod P Q ⇒ Prod (full P) (full Q)
+ | D P ⇒ D (full P)
+ ]
+and full_app M N ≝
+ match M with
+ [ Sort n ⇒ App (Sort n) N
+ | Rel n ⇒ App (Rel n) N
+ | App P Q ⇒ App (full_app P (full Q)) N
+ | Lambda P Q ⇒ (full Q) [0 ≝ N]
+ | Prod P Q ⇒ App (Prod (full P) (full Q)) N
+ | D P ⇒ App (D (full P)) N
+ ]
+.
+
+lemma pr_lift: ∀N,N1,n. pr N N1 →
+ ∀k. pr (lift N k n) (lift N1 k n).
+#N #N1 #n #pr1 (elim pr1)
+ [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
+ normalize >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;
+ [<plus_n_Sm <plus_n_O @Hind // >eqQ
+ @(transitive_lt ? (size (Lambda M2 N2))) normalize //
+ |@Hind // normalize //
+ ]
+ |* * #eqM1 #pr4 #pr5 >eqM1 @appl;
+ [@Hind // <eqQ normalize //
+ |@Hind // normalize //
+ ]
+ ]
+ |#notlambda (cases (prApp_not_lambda … pr1 ?)) //
+ #M2 * #N2 * * #eqM1 #pr3 #pr4 >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.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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) <associative_append
+ >(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 ? ? ? ([])) <minus_n_n /2/
+ | (lapply (arith4 … H1ik H2ik)) -H1ik H2ik #Hik
+ (>(subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ]
+ <(associative_append ? ? ([?]) ?)
+ >aa_rel_ge >length_append (>commutative_plus)
+ [ <minus_plus // | @not_le_to_not_le_S_S /2/ ]
+ ]
+ ]
+ | //
+ | #N #M #IHN #IHM #Ek >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.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 <appl_append @sat2 /2/
+qed.
+
+lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
+#B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
+qed.
+
+lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
+#B #C #N #HN #M #HM @SAT3_1 /3/
+qed.
+
+definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
+/2/ qed.
+
+lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
+ depRC B1 C1 ≅ depRC B2 C2.
+#B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
+[ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
+qed.
+
+(* the union of two r.c.'s. ***************************************************)
+
+definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
+
+lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
+#B #C #M #Hlor elim Hlor -Hlor #HM /2/
+qed.
+
+lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
+#B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
+qed.
+
+lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
+#B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
+qed.
+
+lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
+#B #C #N #HN elim HN -HN #HN /3/
+qed.
+
+definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
+/2/ qed.
--- /dev/null
+(*
+ ||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/par_reduction.ma".
+include "basics/star.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 red_to_pr: ∀M,N. red M N → pr M N.
+#M #N #redMN (elim redMN) /2/
+qed.
+
+lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
+#M #P #redMP (inversion redMP)
+ [#P1 #M1 #N1 #eqH destruct
+ |2,3,4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
+ |#Q1 #M1 #red1 #_ #eqH destruct #eqP @(ex_intro … M1) /2/
+ ]
+qed.
+
+lemma red_lambda : ∀M,N,P. red (Lambda M N) P →
+ (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨
+ (∃N1. P = (Lambda M N1) ∧ red N N1).
+#M #N #P #redMNP (inversion redMNP)
+ [#P1 #M1 #N1 #eqH destruct
+ |2,3,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
+ (@(ex_intro … M1)) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
+ (@(ex_intro … N1)) % //
+ |#Q1 #M1 #red1 #_ #eqH destruct
+ ]
+qed.
+
+lemma red_prod : ∀M,N,P. red (Prod M N) P →
+ (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
+ (∃N1. P = (Prod M N1) ∧ red N N1).
+#M #N #P #redMNP (inversion redMNP)
+ [#P1 #M1 #N1 #eqH destruct
+ |2,3,4,5:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
+ (@(ex_intro … M1)) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
+ (@(ex_intro … N1)) % //
+ |#Q1 #M1 #red1 #_ #eqH destruct
+ ]
+qed.
+
+lemma red_app : ∀M,N,P. red (App M N) P →
+ (∃M1,N1. M = (Lambda M1 N1) ∧ P = N1[0:=N]) ∨
+ (∃M1. P = (App M1 N) ∧ red M M1) ∨
+ (∃N1. P = (App M N1) ∧ red N N1).
+#M #N #P #redMNP (inversion redMNP)
+ [#P1 #M1 #N1 #eqH destruct #eqP %1 %1
+ @(ex_intro … P1) @(ex_intro … M1) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
+ (@(ex_intro … M1)) % //
+ |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
+ (@(ex_intro … N1)) % //
+ |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
+ |#Q1 #M1 #red1 #_ #eqH destruct
+ ]
+qed.
+
+definition reduct ≝ λn,m. red m n.
+
+definition SN ≝ WF ? reduct.
+
+definition NF ≝ λM. ∀N. ¬ (reduct N M).
+
+theorem NF_to_SN: ∀M. NF M → SN M.
+#M #nfM % #a #red @False_ind /2/
+qed.
+
+lemma NF_Sort: ∀i. NF (Sort i).
+#i #N % #redN (inversion redN)
+ [1: #P #N #M #H destruct
+ |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma NF_Rel: ∀i. NF (Rel i).
+#i #N % #redN (inversion redN)
+ [1: #P #N #M #H destruct
+ |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct
+ |#M #N #_ #_ #H destruct
+ ]
+qed.
+
+lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
+#N @Telim_size #P (cases P)
+ [1,2:#j #Hind #M1 #i #r1 @False_ind /2/
+ |#P #Q #Hind #M1 #i #r1 (cases (red_app … r1))
+ [*
+ [* #M2 * #N2 * #eqP #eqM1 >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.
+
+
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(*
+ ||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 <eqM1 #G1 #H >(redG_nil …H) /2/
+ |#H @False_ind /2/
+ ]
+ |#G1 #A #i #t1 #Hind #M1 *
+ [#eqM1 <eqM1 #G2 #H cases (redG_inv … H)
+ #P * #G3 * * #r1 #r2 #eqG2 >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 <eqM1 #G2 #rg (cases (redG_inv … rg))
+ #Q * #G3 * * #r2 #rg1 #eqG2 >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 @(app … B);
+ [@Hind1 /2/ | @Hind2 /2/ ]
+ |#reda (cases (red_app …reda))
+ [*
+ [*
+ #M2 * #N1 * #eqA #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 @(abs … t3 t4)
+ |#redl (cases (red_lambda … redl))
+ [* #M3 * #eqM2 #redA >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/]
+ |#redd (cases (red_d … redd)) #Q * #eqM1 #redA >eqM1
+ @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+ ]
+qed.
+
--- /dev/null
+(*
+ ||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 @HindQ]
+ |#P #Q #HindP #HindQ #N #n #i #j normalize
+ @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+ <associative_plus @HindQ]
+ |#P #HindP #N #n #i #j normalize
+ @eq_f @HindP
+ ]
+qed.
+
+theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
+ (lift B i (S k)) [j ≝ A] = lift B i k.
+#A #B (elim B) normalize /2/
+ [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
+ @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
+ |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind //
+ |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len
+ [>(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 |<H (applyS plus_minus_m_m) // ]
+ (generalize in match ltin)
+ <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
+ |<H @(lt_O_n_elim … posn) #m normalize //
+ ]
+ |(cut (k+i < n-1))
+ [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
+ #Hlt >(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.
--- /dev/null
+(*
+ ||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.
--- /dev/null
+(*
+ ||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)
+.
--- /dev/null
+(*
+ ||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 <Heq1 @(Hind2 ? (P::D)) normalize //
+ ]
+ |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
+ #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
+ >(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.
projects / helm.git / commitdiff