]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/CC2FO_K.ma
made executable again
[helm.git] / matita / matita / lib / pts_dummy / CC2FO_K.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "pts_dummy/degree.ma".
16 (*
17 (* TO BE PUT ELSEWERE *)
18 lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
19 // qed.
20
21 (* λPω → λω MAPPING ***********************************************************)
22 (* The idea [1] is to map a λPω-type T to a λω-type J(T) representing the
23  * structure of the saturated subset (s.s.) of the λPω-terms for the type T.
24  * To this aim, we encode:
25  * 1) SAT (the collection of the (dependent) families of s.s.) as □
26  * 2) Sat (the union of the families in SAT) as ∗
27       [ sat (the family of s.s.) does not need to be distinguisched from Sat ]
28  * 3) sn (the full saturated subset) as a constant 0 of type ∗
29  * [1] H. H.P. Barendregt (1993) Lambda Calculi with Types,
30  *     Osborne Handbooks of Logic in Computer Science (2) pp. 117-309
31  *)
32
33 (* The K interpretation of a term *********************************************)
34
35 (* the interpretation in the λPω-context G of t (should be λPω-kind or □)
36  * as a member of SAT
37  *)
38 let rec Ki G t on t ≝ match t with
39 [ Sort _     ⇒ Sort 0
40 | Prod n m   ⇒ 
41     let im ≝ Ki (n::G) m in 
42     if_then_else ? (eqb (║n║_[║G║]) 3) (Prod (Ki G n) im) im[0≝Sort 0]
43 (* this is correct if we want dummy kinds *)
44 | D _        ⇒ Sort 0
45 (* this is for the substitution lemma *)
46 | Rel i      ⇒ Rel i
47 (* this is useless but nice: see [1] Definition 5.3.3 *)
48 | Lambda n m ⇒ (Ki (n::G) m)[0≝Sort 0]
49 | App m n    ⇒ Ki G m
50 ].
51
52 interpretation "CC2FO: K interpretation (term)" 'IK t L = (Ki L t).
53
54 lemma ki_prod_3: ∀n,G. ║n║_[║G║] = 3 → 
55                  ∀m. 𝕂{Prod n m}_[G] = Prod (𝕂{n}_[G]) (𝕂{m}_[n::G]).
56 #n #G #H #m normalize >H -H //
57 qed.
58
59 lemma ki_prod_not_3: ∀n,G. ║n║_[║G║] ≠ 3 →
60                      ∀m. 𝕂{Prod n m}_[G] =  𝕂{m}_[n::G][0≝Sort 0].
61 #n #G #H #m normalize >(not_eq_to_eqb_false … H) -H //
62 qed.
63
64 (* replacement for the K interpretation *)
65 lemma ki_repl: ∀t,G1,G2. ║G1║ = ║G2║ → 𝕂{t}_[G1] = 𝕂{t}_[G2]. 
66 #t elim t -t //
67 [ #m #n #IHm #_ #G1 #G2 #HG12 >(IHm … HG12) //
68 | #n #m #_ #IHm #G1 #G2 #HG12 normalize >(IHm ? (n::G2)) //
69 | #n #m #IHn #IHm #G1 #G2 #HG12 @(eqb_elim (║n║_[║G1║]) 3) #Hdeg
70   [ >(ki_prod_3 … Hdeg) >HG12 in Hdeg #Hdeg >(ki_prod_3 … Hdeg) /3/
71   | >(ki_prod_not_3 … Hdeg) >HG12 in Hdeg #Hdeg >(ki_prod_not_3 … Hdeg) /3/
72   ]
73 ]
74 qed.
75
76 (* weakeing and thinning lemma for the K interpretation *)
77 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
78 lemma ki_lift: ∀p,G,Gp. p = |Gp| → ∀t,k,Gk. k = |Gk| →
79                               𝕂{lift t k p}_[(Lift Gk p) @ Gp @ G] =  lift (𝕂{t}_[Gk @ G]) k p.
80 #p #G #Gp #HGp #t elim t -t //
81 [ #i #k #Gk #HGk @(leb_elim (S i) k) #Hik
82   [ >(lift_rel_lt … Hik) // | >(lift_rel_not_le … Hik) // ]
83 | #m #n #IHm #_ #k #Gk #HGk >IHm //
84 | #n #m #_ #IHm #k #Gk #HGk normalize <cons_append_assoc <Lift_cons //
85   >(IHm … (? :: ?)) // >commutative_plus /2/
86 | #n #m #IHn #IHm #k #Gk #HGk >lift_prod 
87   @(eqb_elim (║lift n k p║_[║Lift Gk p @Gp@G║]) 3) #Hdeg
88   [ >(ki_prod_3 … Hdeg) <cons_append_assoc <Lift_cons //
89     >append_Deg in Hdeg >append_Deg >deg_lift /2/ >DegHd_Lift /2/
90     <append_Deg #Hdeg >(ki_prod_3 … Hdeg)
91     >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
92   | >(ki_prod_not_3 … Hdeg) <cons_append_assoc <Lift_cons //
93     >append_Deg in Hdeg >append_Deg >deg_lift /2/ >DegHd_Lift /2/
94     <append_Deg #Hdeg >(ki_prod_not_3 … Hdeg)
95     >(IHm … (? :: ?)) // >commutative_plus /2/
96   ]
97 ]
98 qed.
99
100 (* substitution lemma for the K interpretation *)
101 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
102 lemma ki_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
103                 ∀t,k,Gk. k = |Gk| →
104                                 𝕂{t[k≝v]}_[Gk @ G] =  𝕂{t}_[Lift Gk 1 @ [w] @ G][k≝𝕂{v}_[G]].
105 #v #w #G #Hvw #t elim t -t //
106 [ #i #k #Gk #HGk @(leb_elim (S i) k) #H1ik
107   [ >(subst_rel1 … H1ik) >(subst_rel1 … H1ik) //
108   | @(eqb_elim i k) #H2ik
109     [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >subst_rel2
110       >(ki_lift ? ? ? ? ? ? ([])) //
111     | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
112       >(subst_rel3 … Hik) >(subst_rel3 … Hik) //
113     ]
114   ]
115 | #m #n #IHm #_ #k #Gk #HGk >IHm //
116 | #n #m #_ #IHm #k #Gk #HGk normalize >(IHm … (? :: ?));
117   [ >subst_lemma_comm >(Lift_cons … HGk) >ki_repl /2 by Deg_lift_subst/
118   | >commutative_plus /2/
119   ]
120 | #n #m #IHn #IHm #k #Gk #HGk >subst_prod
121   @(eqb_elim (║n║_[║Lift Gk 1@[w]@G║]) 3) #Hdeg
122   [ >(ki_prod_3 … Hdeg) >append_Deg in Hdeg >append_Deg >DegHd_Lift //
123     <Hvw <(deg_subst … k); [2: /2/ ] <append_Deg #Hdeg
124     >(ki_prod_3 … Hdeg) >IHn // >(IHm … (? :: ?));
125     [ >(Lift_cons … HGk) >(ki_repl … m); /2 by Deg_lift_subst/
126     | >commutative_plus /2/
127     ]
128   | >(ki_prod_not_3 … Hdeg) >append_Deg in Hdeg >append_Deg >DegHd_Lift //
129     <Hvw <(deg_subst … k); [2: /2/ ] <append_Deg #Hdeg
130     >(ki_prod_not_3 … Hdeg) >(IHm … (? :: ?));
131     [ >subst_lemma_comm >(Lift_cons … HGk) >ki_repl /2 by Deg_lift_subst/
132     | >commutative_plus /2/
133     ]
134   ]
135 ]
136 qed.
137
138 lemma ki_subst_0: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
139                   ∀t.  𝕂{t[0≝v]}_[G] = 𝕂{t}_[w::G][0≝𝕂{v}_[G]].
140 #v #w #G #Hvw #t @(ki_subst ?????? ([])) //
141 qed.
142
143 (* The K interpretation of a context ******************************************)
144
145 (* the interpretation of a λPω-context G *)
146 let rec KI G ≝ match G with
147 [ nil      ⇒ nil …
148 | cons t F ⇒ if_then_else ? (eqb (║t║_[║F║]) 3) (𝕂{t}_[F] :: KI F) (KI F)
149 ].
150
151 interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G).
152 *)