+++ /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 "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 of a term *********************************************)
-
-(* 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)" 'IK t L = (Ki L t).
-
-lemma ki_prod_3: ∀n,G. ║n║_[║G║] = 3 →
- ∀m. 𝕂{Prod n m}_[G] = Prod (𝕂{n}_[G]) (𝕂{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.
-
-(* The K interpretation of a context ******************************************)
-
-(* the interpretation of a λPω-context G *)
-let rec KI G ≝ match G with
-[ nil ⇒ nil …
-| cons t F ⇒ if_then_else ? (eqb (║t║_[║F║]) 3) (𝕂{t}_[F] :: KI F) (KI F)
-].
-
-interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G).
projects / helm.git / blobdiff