From e28e86e04bb5b8b98f5e2f86555347a280c49983 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 1 Jun 2011 14:18:46 +0000
Subject: [PATCH] CC2FO_K_cube: soundness of the K interpretation stated

---
 matita/matita/lib/lambda/CC2FO_K.ma         | 28 ++++++++++++++-------
 matita/matita/lib/lambda/CC2FO_K_cube.ma    | 24 ++++++++++++++++++
 matita/matita/lib/lambda/lambda_notation.ma |  8 ++++--
 3 files changed, 49 insertions(+), 11 deletions(-)
 create mode 100644 matita/matita/lib/lambda/CC2FO_K_cube.ma

diff --git a/matita/matita/lib/lambda/CC2FO_K.ma b/matita/matita/lib/lambda/CC2FO_K.ma
index 466048303..752ed00c0 100644
--- a/matita/matita/lib/lambda/CC2FO_K.ma
+++ b/matita/matita/lib/lambda/CC2FO_K.ma
@@ -30,34 +30,34 @@ lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
  *     Osborne Handbooks of Logic in Computer Science (2) pp. 117-309
  *)
 
-(* The K interpretation *******************************************************)
+(* 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
+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]
+    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
+| 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).
+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 (KI G n) (𝕂{m}_[n::G])).
+                 ∀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].
+                     ∀m. 𝕂{Prod n m}_[G] =  𝕂{m}_[n::G][0≝Sort 0].
 #n #G #H #m normalize >(not_eq_to_eqb_false … H) -H //
 qed.
 
@@ -139,3 +139,13 @@ 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).
diff --git a/matita/matita/lib/lambda/CC2FO_K_cube.ma b/matita/matita/lib/lambda/CC2FO_K_cube.ma
new file mode 100644
index 000000000..814ce59fe
--- /dev/null
+++ b/matita/matita/lib/lambda/CC2FO_K_cube.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "CC2FO_K.ma".
+include "cube.ma".
+include "inversion.ma".
+
+(* The K interpretation in the λ-Cube *****************************************)
+
+lemma ki_type: ∀G,t,u. G ⊢_{CC} t : u → u = Sort 1 → 𝕂{G} ⊢_{FO} 𝕂{t}_[G] : u.
+#G #t #u #H elim H -H G t u
+[ #i #j * #_ @ax //
+| #G #A #i #HA #IHA #Heq  
\ No newline at end of file
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 4f2f4f1dc..8063634d0 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -97,6 +97,10 @@ notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
 
-notation "hvbox(𝕂{T} break _ [E])"
+notation "hvbox(𝕂{G})"
    non associative with precedence 50
-   for @{'IK1 $T $E}.
+   for @{'IK $G}.
+
+notation "hvbox(𝕂{T} break _ [G])"
+   non associative with precedence 50
+   for @{'IK $T $G}.
-- 
2.39.2