1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 (* TO BE PUT ELSEWERE *)
18 lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
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
33 (* The K interpretation of a term *********************************************)
35 (* the interpretation in the λPω-context G of t (should be λPω-kind or □)
38 let rec Ki G t on t ≝ match t with
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 *)
45 (* this is for the substitution lemma *)
47 (* this is useless but nice: see [1] Definition 5.3.3 *)
48 | Lambda n m ⇒ (Ki (n::G) m)[0≝Sort 0]
52 interpretation "CC2FO: K interpretation (term)" 'IK t L = (Ki L t).
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 //
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 //
64 (* replacement for the K interpretation *)
65 lemma ki_repl: ∀t,G1,G2. ║G1║ = ║G2║ → 𝕂{t}_[G1] = 𝕂{t}_[G2].
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/
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/
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║] →
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) //
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/
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/
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/
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 ?????? ([])) //
143 (* The K interpretation of a context ******************************************)
145 (* the interpretation of a λPω-context G *)
146 let rec KI G ≝ match G with
148 | cons t F ⇒ if_then_else ? (eqb (║t║_[║F║]) 3) (𝕂{t}_[F] :: KI F) (KI F)
151 interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G).