From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 20 May 2011 14:35:59 +0000 (+0000)
Subject: - we weakened SAT3
X-Git-Tag: make_still_working~2499
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5bfc4a8069dc1b219f958a865c5f60b88dadf525;p=helm.git

- we weakened SAT3
- we simplified the specifications of the Cube
---

diff --git a/matita/matita/lib/lambda/cube.ma b/matita/matita/lib/lambda/cube.ma
index 9ddaed35c..8ac3d978c 100644
--- a/matita/matita/lib/lambda/cube.ma
+++ b/matita/matita/lib/lambda/cube.ma
@@ -17,27 +17,27 @@ 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
+inductive Cube_Ax: nat → nat → Prop ≝
+  | star_box: Cube_Ax 0 1
 .
 
 (* 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
+inductive CC_Re: nat → nat → nat → Prop ≝
+   | star_star: CC_Re 0 0 0
+   | box_star : CC_Re 1 0 0
+   | box_box  : CC_Re 1 1 1
+   | star_box : CC_Re 0 1 1
 .
 
 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
+inductive FO_Re: nat → nat → nat → Prop ≝
+   | star_star: FO_Re 0 0 0
+   | box_star : FO_Re 1 0 0
+   | box_box  : FO_Re 1 1 1
 .
 
 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index aacaaed2b..3eb04315f 100644
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -33,6 +33,7 @@ record RC : Type[0] ≝ {
    sat3: SAT3 mem;  (* we add the clusure by rev dapp *)
    sat4: SAT4 mem   (* we add the clusure by dummies *) 
 }.
+
 (* HIDDEN BUG:
  * if SAT0 and SAT1 are expanded,
  * the projections sat0 and sat1 are not generated
@@ -119,7 +120,7 @@ qed.
 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 
 lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
-#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
+#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
 qed.
 
 lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
@@ -134,7 +135,7 @@ lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 qed.
 
 lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
-#B #C #N #l1 #l2 #HN #M #HM <appl_append >associative_append /3/
+#B #C #M #N #l #H #L #HL <appl_append @sat3 /2/
 qed.
 
 lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index 9b6478455..a9fbff370 100644
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -34,8 +34,8 @@ definition SAT1 ≝ λ(P:?->Prop). ∀i,l. SNl l → P (Appl (Rel i) l).
 definition SAT2 ≝ λ(P:?→Prop). ∀N,L,M,l. SN N → SN L → 
                   P (Appl M[0:=L] l) → P (Appl (Lambda N M) (L::l)).
 
-definition SAT3 ≝ λ(P:?→Prop). ∀N,l1,l2. P (Appl (D (Appl N l1)) l2) → 
-                               P (Appl (D N) (l1@l2)).
+definition SAT3 ≝ λ(P:?→Prop). ∀M,N,l. P (Appl (D (App M N)) l) → 
+                               P (Appl (D M) (N::l)).
 
 definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M).
 
@@ -47,8 +47,8 @@ lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
 #P #i #HP @(HP i (nil ?) …) //
 qed.
 
-lemma SAT3_1: ∀P,N,M. SAT3 P → P (D (App N M)) → P (App (D N) M).
-#P #N #M #HP #H @(HP … ([?]) ([])) @H
+lemma SAT3_1: ∀P,M,N. SAT3 P → P (D (App M N)) → P (App (D M) N).
+#P #M #N #HP #H @(HP … ([])) @H
 qed.
 
 (* axiomatization *************************************************************)