From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 19 May 2011 14:12:22 +0000 (+0000)
Subject: cube.ma: some pts specifications of the lambda-cube
X-Git-Tag: make_still_working~2512
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f4d8aee837eb33a5598aa0977fc67ec21e8dbf8;p=helm.git

cube.ma: some pts specifications of the lambda-cube
---

diff --git a/matita/matita/lib/lambda/convertibility.ma b/matita/matita/lib/lambda/convertibility.ma
index 0cf913111..4e4b9e8e4 100644
--- a/matita/matita/lib/lambda/convertibility.ma
+++ b/matita/matita/lib/lambda/convertibility.ma
@@ -64,7 +64,7 @@ lemma conv_to_deq: ∀M,N. conv M N → red M N ∨ d_eq M N.
   |#P #M1 %2 //
   ]
 qed.
- 
+(* FG: THIS IN NOT COMPLETE
 theorem main1: ∀M,N. CO M N → 
   ∃P,Q. star … red M P ∧ star … red N Q ∧ d_eq P Q.
 #M #N #coMN (elim coMN)
@@ -73,7 +73,7 @@ theorem main1: ∀M,N. CO M N →
     [
   |@(ex_intro … M) @(ex_intro … M) % // % //
   ]
-
+*)
 lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
 #M #P #redMP (inversion redMP)
   [#P1 #M1 #N1 #eqH destruct
@@ -287,7 +287,7 @@ lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M.
 #M #N #rstar (elim rstar) //
 #Q #P #HbQ  #redQP #snNQ #snN @(SN_step …redQP) /2/
 qed. 
-
+(* FG: THIS EXPLODES 
 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 → 
 ∃M1.subterm N1 M1 ∧ red M M1.
 #M #N #subN (elim subN) /4/
@@ -296,7 +296,7 @@ lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
 @(ex_intro … C) /3/
 qed.
-
+*)
 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 → 
 ∃M1.subterm N1 M1 ∧ red M M1.
   
diff --git a/matita/matita/lib/lambda/cube.ma b/matita/matita/lib/lambda/cube.ma
new file mode 100644
index 000000000..9ddaed35c
--- /dev/null
+++ b/matita/matita/lib/lambda/cube.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "convertibility.ma".
+include "types.ma".
+
+(* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
+
+inductive Cube_Ax (i,j:nat): Prop ≝
+  | star_box: i = 0 → j = 1 → Cube_Ax i j
+.
+
+(* The λPω pure type system (a.k.a. λC or CC) *********************************)
+
+inductive CC_Re (i,j,k:nat): Prop ≝
+   | star_star: i = 0 → j = 0 → k = 0 → CC_Re i j k
+   | box_star : i = 1 → j = 0 → k = 0 → CC_Re i j k
+   | box_box  : i = 1 → j = 1 → k = 1 → CC_Re i j k
+   | star_box : i = 0 → j = 1 → k = 1 → CC_Re i j k
+.
+
+definition CC: pts ≝ mk_pts Cube_Ax CC_Re conv.
+
+(* The λω pure type system (a.k.a. Fω) ****************************************)
+
+inductive FO_Re (i,j,k:nat): Prop ≝
+   | star_star: i = 0 → j = 0 → k = 0 → FO_Re i j k
+   | box_star : i = 1 → j = 0 → k = 0 → FO_Re i j k
+   | box_box  : i = 1 → j = 1 → k = 1 → FO_Re i j k
+.
+
+definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma
index a0d262363..554f8099c 100644
--- a/matita/matita/lib/lambda/terms.ma
+++ b/matita/matita/lib/lambda/terms.ma
@@ -33,6 +33,7 @@ lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
 #N #l elim l -l // #hd #tl #IHl #M >IHl //
 qed.
 
+(*
 let rec is_dummy t ≝ match t with
    [ Sort _     ⇒ false
    | Rel _      ⇒ false
@@ -41,7 +42,7 @@ let rec is_dummy t ≝ match t with
    | Prod _ _   ⇒ false       (* not so sure yet *)
    | D _        ⇒ true
    ].
-
+*)
 (* nautral terms *)
 inductive neutral: T → Prop ≝
    | neutral_sort: ∀n.neutral (Sort n)