From 5bfc4a8069dc1b219f958a865c5f60b88dadf525 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 20 May 2011 14:35:59 +0000 Subject: [PATCH] - we weakened SAT3 - we simplified the specifications of the Cube --- matita/matita/lib/lambda/cube.ma | 22 +++++++++++----------- matita/matita/lib/lambda/rc_sat.ma | 5 +++-- matita/matita/lib/lambda/sn.ma | 8 ++++---- 3 files changed, 18 insertions(+), 17 deletions(-) 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 associative_append /3/ +#B #C #M #N #l #H #L #HL 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 *************************************************************) -- 2.39.2