- terms.ma: we included 'is_dummy" and "neutral" (maybe "is_neutral

would be better)
- sn.ma rc_sat.ma: we introduced the axioms for dummy

diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma
index 952161107dfd30fb22381076d5128fac45a2f96a..a183047e0276482c2a791442e2e33bc234384fc2 100644 (file)
--- a/matita/matita/lib/lambda/ext_lambda.ma
+++ b/matita/matita/lib/lambda/ext_lambda.ma
@@ -17,19 +17,10 @@ include "lambda/subst.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
-(* terms **********************************************************************)
-
-(* FG: not needed for now 
-(* nautral terms *)
-inductive neutral: T → Prop ≝
-   | neutral_sort: ∀n.neutral (Sort n)
-   | neutral_rel: ∀i.neutral (Rel i)
-   | neutral_app: ∀M,N.neutral (App M N)
-.
-*)
-
 (* substitution ***************************************************************)
-
+(*
+axiom is_dummy_lift: ∀p,t,k. is_dummy (lift t k p) = is_dummy t.
+*)
 (* FG: do we need this? 
 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
 

diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index ddbafc71afc14a9ab0f2c64165d5feef69a28724..4e15b07d3124fd5d588aa55211390301b6b9ffe4 100644 (file)
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -29,7 +29,9 @@ record RC : Type[0] ≝ {
    cr1 : CR1 mem;
    sat0: SAT0 mem;
    sat1: SAT1 mem;
-   sat2: SAT2 mem
+   sat2: SAT2 mem;
+   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,
@@ -65,21 +67,21 @@ interpretation
    "extensional equality (reducibility candidate)"
    'Eq C1 C2 = (rceq C1 C2).
 
-definition rceql ≝ λl1,l2. all2 ? rceq l1 l2.
+definition rceql ≝ λl1,l2. all2 … rceq l1 l2.
 
 interpretation
    "extensional equality (context of reducibility candidates)"
    'Eq C1 C2 = (rceql C1 C2).
 
-theorem reflexive_rceq: reflexive … rceq.
+lemma reflexive_rceq: reflexive … rceq.
 /2/ qed.
 
-theorem symmetric_rceq: symmetric … rceq.
-#x #y #H #M (elim (H M)) -H /3/
+lemma symmetric_rceq: symmetric … rceq.
+#x #y #H #M elim (H M) -H /3/
 qed.
 
-theorem transitive_rceq: transitive … rceq.
-#x #y #z #Hxy #Hyz #M (elim (Hxy M)) -Hxy (elim (Hyz M)) -Hyz /4/
+lemma transitive_rceq: transitive … rceq.
+#x #y #z #Hxy #Hyz #M elim (Hxy M) -Hxy; elim (Hyz M) -Hyz /4/
 qed.
 (*
 theorem reflexive_rceql: reflexive … rceql.
@@ -90,54 +92,60 @@ qed.
  * Without the type specification, this statement has two interpretations
  * but matita does not complain
  *)
-theorem mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
-#M #C1 #C2 #H1 #H12 (elim (H12 M)) -H12 /2/
+lemma mem_rceq_trans: ∀(M:T). ∀C1,C2. M ∈ C1 → C1 ≅ C2 → M ∈ C2.
+#M #C1 #C2 #H1 #H12 elim (H12 M) -H12 /2/
 qed.
-
+(*
 (* NOTE: hd_repl and tl_repl are proved essentially by the same script *)
-theorem hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
+lemma hd_repl: ∀C1,C2. C1 ≅ C2 → ∀l1,l2. l1 ≅ l2 → hd ? l1 C1 ≅ hd ? l2 C2.
 #C1 #C2 #QC #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 #hd2 #tl2 #_ #Q elim Q //
 qed.
 
-theorem tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
+lemma tl_repl: ∀l1,l2. l1 ≅ l2 → tail ? l1 ≅ tail ? l2.
 #l1 (elim l1) -l1 [ #l2 #Q >Q // ]
 #hd1 #tl1 #_ #l2 (elim l2) -l2 [ #Q elim Q ]
 #hd2 #tl2 #_ #Q elim Q //
 qed.
 
-theorem nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
+lemma nth_repl: ∀C1,C2. C1 ≅ C2 → ∀i,l1,l2. l1 ≅ l2 →
                   nth i ? l1 C1 ≅ nth i ? l2 C2.
 #C1 #C2 #QC #i (elim i) /3/
 qed.
-
+*)
 (* the r.c for a (dependent) product type. ************************************)
 
 definition dep_mem ≝ λB,C,M. ∀N. N ∈ B → App M N ∈ C.
 
-theorem dep_cr1: ∀B,C. CR1 (dep_mem B 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 *)
 qed.
 
-theorem dep_sat0: ∀B,C. SAT0 (dep_mem B C).
+lemma dep_sat0: ∀B,C. SAT0 (dep_mem B C).
 /5/ qed.
 
-theorem dep_sat1: ∀B,C. SAT1 (dep_mem B C).
+lemma dep_sat1: ∀B,C. SAT1 (dep_mem B C).
 /5/ qed.
 
 (* NOTE: @sat2 is not needed if append_cons is enabled *)
-theorem dep_sat2: ∀B,C. SAT2 (dep_mem B C).
+lemma dep_sat2: ∀B,C. SAT2 (dep_mem B C).
 #B #C #N #L #M #l #HN #HL #HM #K #HK <appl_append @sat2 /2/
 qed.
 
+lemma dep_sat3: ∀B,C. SAT3 (dep_mem B C).
+#B #C #N #l1 #l2 #HN #M #HM <appl_append >associative_append /3/
+qed.
+
+lemma dep_sat4: ∀B,C. SAT4 (dep_mem B C).
+#B #C #N #HN #M #HM @SAT3_1 /3/ 
+qed.
+
 definition depRC: RC → RC → RC ≝ λB,C. mk_RC (dep_mem B C) ….
 /2/ qed.
 
-theorem dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
-                  depRC B1 C1 ≅ depRC B2 C2.
+lemma dep_repl: ∀B1,B2,C1,C2. B1 ≅ B2 → C1 ≅ C2 →
+                depRC B1 C1 ≅ depRC B2 C2.
 #B1 #B2 #C1 #C2 #QB #QC #M @conj #H1 #N #H2
 [ lapply (symmetric_rceq … QB) -QB | lapply (symmetric_rceq … QC) -QC ] /4/
 qed.
-
-

diff --git a/matita/matita/lib/lambda/sn.ma b/matita/matita/lib/lambda/sn.ma
index c30cfecc7619d6714779ca165ffd96d59562390f..9b6478455a22a5ed18eda8b952003b7c7695f676 100644 (file)
--- a/matita/matita/lib/lambda/sn.ma
+++ b/matita/matita/lib/lambda/sn.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
+include "lambda/ext_lambda.ma".
 
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
@@ -34,12 +34,21 @@ 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)).
 
-theorem SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
-#P #n #H @(H n (nil ?) …) //
+definition SAT3 ≝ λ(P:?→Prop). ∀N,l1,l2. P (Appl (D (Appl N l1)) l2) → 
+                               P (Appl (D N) (l1@l2)).
+
+definition SAT4 ≝ λ(P:?→Prop). ∀M. P M → P (D M).
+
+lemma SAT0_sort: ∀P,n. SAT0 P → P (Sort n).
+#P #n #HP @(HP n (nil ?) …) //
+qed.
+
+lemma SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
+#P #i #HP @(HP i (nil ?) …) //
 qed.
 
-theorem SAT1_rel: ∀P,i. SAT1 P → P (Rel i).
-#P #i #H @(H i (nil ?) …) //
+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
 qed.
 
 (* axiomatization *************************************************************)
@@ -50,10 +59,12 @@ axiom sn_rel: SAT1 SN.
 
 axiom sn_beta: SAT2 SN.
 
+axiom sn_dapp: SAT3 SN.
+
+axiom sn_dummy: SAT4 SN.
+
 axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
 
 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
 
-axiom sn_dummy: ∀M. SN M → SN (D M).
-
 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.

diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma
index 915c134462cdcf90e08be1053dc29b6674dcd135..a0d262363fc9f865b88394ecf5a317a45a7fc475 100644 (file)
--- a/matita/matita/lib/lambda/terms.ma
+++ b/matita/matita/lib/lambda/terms.ma
@@ -32,3 +32,19 @@ let rec Appl F l on l ≝ match l with
 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
+   | App M _    ⇒ is_dummy M
+   | Lambda _ M ⇒ is_dummy M
+   | Prod _ _   ⇒ false       (* not so sure yet *)
+   | D _        ⇒ true
+   ].
+
+(* nautral terms *)
+inductive neutral: T → Prop ≝
+   | neutral_sort: ∀n.neutral (Sort n)
+   | neutral_rel: ∀i.neutral (Rel i)
+   | neutral_app: ∀M,N.neutral (App M N)
+.