subst.ma: some additions

convertibility.ma: non "conv" refers to the correct predicate
CC2FO_K.ma: CC to Fomega: first interpretation: substitution lemma

diff --git a/matita/matita/lib/lambda/CC2FO_K.ma b/matita/matita/lib/lambda/CC2FO_K.ma
new file mode 100644 (file)
index 0000000..4660483
--- /dev/null
+++ b/matita/matita/lib/lambda/CC2FO_K.ma
@@ -0,0 +1,141 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "degree.ma".
+
+(* TO BE PUT ELSEWERE *)
+lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
+// qed.
+
+(* λPω → λω MAPPING ***********************************************************)
+(* The idea [1] is to map a λPω-type T to a λω-type J(T) representing the
+ * structure of the saturated subset (s.s.) of the λPω-terms for the type T.
+ * To this aim, we encode:
+ * 1) SAT (the collection of the (dependent) families of s.s.) as □
+ * 2) Sat (the union of the families in SAT) as ∗
+      [ sat (the family of s.s.) does not need to be distinguisched from Sat ]
+ * 3) sn (the full saturated subset) as a constant 0 of type ∗
+ * [1] H. H.P. Barendregt (1993) Lambda Calculi with Types,
+ *     Osborne Handbooks of Logic in Computer Science (2) pp. 117-309
+ *)
+
+(* The K interpretation *******************************************************)
+
+(* the interpretation in the λPω-context G of t (should be λPω-kind or □)
+ * as a member of SAT
+ *)
+let rec KI G t on t ≝ match t with
+[ Sort _     ⇒ Sort 0
+| Prod n m   ⇒ 
+    let im ≝ KI (n::G) m in 
+    if_then_else ? (eqb (║n║_[║G║]) 3) (Prod (KI G n) im) im[0≝Sort 0]
+(* this is correct if we want dummy kinds *)
+| D _        ⇒ Sort 0
+(* this is for the substitution lemma *)
+| Rel i      ⇒ Rel i
+(* this is useless but nice: see [1] Definition 5.3.3 *)
+| Lambda n m ⇒ (KI (n::G) m)[0≝Sort 0]
+| App m n    ⇒ KI G m
+].
+
+interpretation "CC2FO: K interpretation (term)" 'IK1 t L = (KI L t).
+
+lemma ki_prod_3: ∀n,G. ║n║_[║G║] = 3 → 
+                 ∀m. 𝕂{Prod n m}_[G] = (Prod (KI G n) (𝕂{m}_[n::G])).
+#n #G #H #m normalize >H -H //
+qed.
+
+lemma ki_prod_not_3: ∀n,G. ║n║_[║G║] ≠ 3 →
+                     ∀m. 𝕂{Prod n m}_[G] = 𝕂{m}_[n::G][0≝Sort 0].
+#n #G #H #m normalize >(not_eq_to_eqb_false … H) -H //
+qed.
+
+(* replacement for the K interpretation *)
+lemma ki_repl: ∀t,G1,G2. ║G1║ = ║G2║ → 𝕂{t}_[G1] = 𝕂{t}_[G2]. 
+#t elim t -t //
+[ #m #n #IHm #_ #G1 #G2 #HG12 >(IHm … HG12) //
+| #n #m #_ #IHm #G1 #G2 #HG12 normalize >(IHm ? (n::G2)) //
+| #n #m #IHn #IHm #G1 #G2 #HG12 @(eqb_elim (║n║_[║G1║]) 3) #Hdeg
+  [ >(ki_prod_3 … Hdeg) >HG12 in Hdeg #Hdeg >(ki_prod_3 … Hdeg) /3/
+  | >(ki_prod_not_3 … Hdeg) >HG12 in Hdeg #Hdeg >(ki_prod_not_3 … Hdeg) /3/
+  ]
+]
+qed.
+
+(* weakeing and thinning lemma for the K interpretation *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ki_lift: ∀p,G,Gp. p = |Gp| → ∀t,k,Gk. k = |Gk| →
+                              𝕂{lift t k p}_[(Lift Gk p) @ Gp @ G] =  lift (𝕂{t}_[Gk @ G]) k p.
+#p #G #Gp #HGp #t elim t -t //
+[ #i #k #Gk #HGk @(leb_elim (S i) k) #Hik
+  [ >(lift_rel_lt … Hik) // | >(lift_rel_not_le … Hik) // ]
+| #m #n #IHm #_ #k #Gk #HGk >IHm //
+| #n #m #_ #IHm #k #Gk #HGk normalize <cons_append_assoc <Lift_cons //
+  >(IHm … (? :: ?)) // >commutative_plus /2/
+| #n #m #IHn #IHm #k #Gk #HGk >lift_prod 
+  @(eqb_elim (║lift n k p║_[║Lift Gk p @Gp@G║]) 3) #Hdeg
+  [ >(ki_prod_3 … Hdeg) <cons_append_assoc <Lift_cons //
+    >append_Deg in Hdeg >append_Deg >deg_lift /2/ >DegHd_Lift /2/
+    <append_Deg #Hdeg >(ki_prod_3 … Hdeg)
+    >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
+  | >(ki_prod_not_3 … Hdeg) <cons_append_assoc <Lift_cons //
+    >append_Deg in Hdeg >append_Deg >deg_lift /2/ >DegHd_Lift /2/
+    <append_Deg #Hdeg >(ki_prod_not_3 … Hdeg)
+    >(IHm … (? :: ?)) // >commutative_plus /2/
+  ]
+]
+qed.
+
+(* substitution lemma for the K interpretation *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ki_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
+                ∀t,k,Gk. k = |Gk| →
+                                𝕂{t[k≝v]}_[Gk @ G] =  𝕂{t}_[Lift Gk 1 @ [w] @ G][k≝𝕂{v}_[G]].
+#v #w #G #Hvw #t elim t -t //
+[ #i #k #Gk #HGk @(leb_elim (S i) k) #H1ik
+  [ >(subst_rel1 … H1ik) >(subst_rel1 … H1ik) //
+  | @(eqb_elim i k) #H2ik
+    [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >subst_rel2
+      >(ki_lift ? ? ? ? ? ? ([])) //
+    | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
+      >(subst_rel3 … Hik) >(subst_rel3 … Hik) //
+    ]
+  ]
+| #m #n #IHm #_ #k #Gk #HGk >IHm //
+| #n #m #_ #IHm #k #Gk #HGk normalize >(IHm … (? :: ?));
+  [ >subst_lemma_comm >(Lift_cons … HGk) >ki_repl /2 by Deg_lift_subst/
+  | >commutative_plus /2/
+  ]
+| #n #m #IHn #IHm #k #Gk #HGk >subst_prod
+  @(eqb_elim (║n║_[║Lift Gk 1@[w]@G║]) 3) #Hdeg
+  [ >(ki_prod_3 … Hdeg) >append_Deg in Hdeg >append_Deg >DegHd_Lift //
+    <Hvw <(deg_subst … k); [2: /2/ ] <append_Deg #Hdeg
+    >(ki_prod_3 … Hdeg) >IHn // >(IHm … (? :: ?));
+    [ >(Lift_cons … HGk) >(ki_repl … m); /2 by Deg_lift_subst/
+    | >commutative_plus /2/
+    ]
+  | >(ki_prod_not_3 … Hdeg) >append_Deg in Hdeg >append_Deg >DegHd_Lift //
+    <Hvw <(deg_subst … k); [2: /2/ ] <append_Deg #Hdeg
+    >(ki_prod_not_3 … Hdeg) >(IHm … (? :: ?));
+    [ >subst_lemma_comm >(Lift_cons … HGk) >ki_repl /2 by Deg_lift_subst/
+    | >commutative_plus /2/
+    ]
+  ]
+]
+qed.
+
+lemma ki_subst_0: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
+                  ∀t.  𝕂{t[0≝v]}_[G] = 𝕂{t}_[w::G][0≝𝕂{v}_[G]].
+#v #w #G #Hvw #t @(ki_subst ?????? ([])) //
+qed.

diff --git a/matita/matita/lib/lambda/convertibility.ma b/matita/matita/lib/lambda/convertibility.ma
index 377d3c890488a0ab5907bfa302a3aa763839decf..045463aaa3dcce25fe63eff35caccb7ec0348b90 100644 (file)
--- a/matita/matita/lib/lambda/convertibility.ma
+++ b/matita/matita/lib/lambda/convertibility.ma
@@ -22,19 +22,19 @@ inductive T : Type[0] ≝
 .
 *)
 
-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). 
+inductive conv1 : T →T → Prop ≝
+  | cbeta: ∀P,M,N. conv1 (App (Lambda P M) N) (M[0 ≝ N])
+  | cappl: ∀M,M1,N. conv1 M M1 → conv1 (App M N) (App M1 N)
+  | cappr: ∀M,N,N1. conv1 N N1 → conv1 (App M N) (App M N1)
+  | claml: ∀M,M1,N. conv1 M M1 → conv1 (Lambda M N) (Lambda M1 N)
+  | clamr: ∀M,N,N1. conv1 N N1 → conv1 (Lambda M N) (Lambda M N1)
+  | cprodl: ∀M,M1,N. conv1 M M1 → conv1 (Prod M N) (Prod M1 N)
+  | cprodr: ∀M,N,N1. conv1 N N1 → conv1 (Prod M N) (Prod M N1)
+  | cd: ∀M,M1. conv1 (D M) (D M1). 
 
-definition CO ≝ star … conv.
+definition conv ≝ star … conv1.
 
-lemma red_to_conv: ∀M,N. red M N → conv M N.
+lemma red_to_conv1: ∀M,N. red M N → conv1 M N.
 #M #N #redMN (elim redMN) /2/
 qed.
 
@@ -48,7 +48,7 @@ inductive d_eq : T →T → Prop ≝
   | 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.
+lemma conv1_to_deq: ∀M,N. conv1 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/]
@@ -61,8 +61,8 @@ lemma conv_to_deq: ∀M,N. conv M N → red M N ∨ d_eq M N.
   ]
 qed.
 
-(* FG: THIS IN NOT COMPLETE
-theorem main1: ∀M,N. CO M N → 
+(* FG: THIS IS NOT COMPLETE
+theorem main1: ∀M,N. conv 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 

diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index 4258f6a7c5575e5ae6a2ac9dbdc6560d7386b264..4f61ef5282fdcf6da367948d7c264526e7ebf87f 100644 (file)
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -142,6 +142,9 @@ lemma lift_subst_up: ∀M,N,n,i,j.
   ]
 qed.
 
+lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
+// 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/
@@ -202,3 +205,8 @@ lemma subst_lemma: ∀A,B,C.∀k,i.
     ]
   ] 
 qed.
+
+lemma subst_lemma_comm: ∀A,B,C.∀k,i.
+  (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
+#A #B #C #k #i >commutative_plus >subst_lemma //
+qed.