X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Frc_sat.ma;h=aacaaed2b3e487c50119af2092b5906482baaa3c;hb=eac90ccb93a94f03df9ba5ad853cbd5d8c60b4f2;hp=06cdb7d90992169dfefda455403e7b1812affecb;hpb=87d894fbd1d1c6ae4f9a8421ffa39af838b72e9f;p=helm.git

diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index 06cdb7d90..aacaaed2b 100644
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -18,18 +18,20 @@ include "lambda/sn.ma".
 
 (* The reducibility candidate (r.c.) ******************************************)
 
-(* We use saturated subsets of strongly normalizing terms
- * (see for instance [Cescutti 2001], but a better citation is required)
- * rather than standard reducibility candidates.
+(* We use saturated subsets of strongly normalizing terms [1]
+ * rather than standard reducibility candidates [2].
  * The benefit is that reduction is not needed to define such subsets.
- * Also, this approach was never tried on a system with dependent types.
+ * [1] Geuvers, H. 1994. A Short and Flexible Proof of Strong Normalization for the Calculus of Constructions.
+ * [2] Barras, B. 1996. Coq en Coq. Rapport de Recherche 3026, INRIA.
  *)
 record RC : Type[0] ≝ {
    mem : T → Prop;
    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,
@@ -42,6 +44,7 @@ interpretation "membership (reducibility candidate)" 'mem A R = (mem R A).
 definition snRC: RC ≝ mk_RC SN ….
 /2/ qed.
 
+(*
 (* a generalization of mem on lists *)
 let rec memc E l on l : Prop ≝ match l with
    [ nil ⇒ True
@@ -54,7 +57,7 @@ let rec memc E l on l : Prop ≝ match l with
 interpretation
    "componentwise membership (context of reducibility candidates)"
    'mem l H = (memc H l).
-
+*)
 (* extensional equality of r.c.'s *********************************************)
 
 definition rceq: RC → RC → Prop ≝ 
@@ -62,79 +65,116 @@ definition rceq: RC → RC → Prop ≝
 
 interpretation
    "extensional equality (reducibility candidate)"
-   'napart C1 C2 = (rceq C1 C2).
+   '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)"
-   'napart C1 C2 = (rceql C1 C2).
+   '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.
 #l (elim l) /2/
 qed.
-
+*)
 (* HIDDEN BUG:
  * 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 →
-                  nth i ? l1 C1 ≈ nth i ? l2 C2.
+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. ************************************)
+*)
+(* 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.
+
+(* the union of two r.c.'s. ***************************************************)
+
+definition lor_mem ≝ λB,C,M. M ∈ B ∨ M ∈ C.
+
+lemma lor_cr1: ∀B,C. CR1 (lor_mem B C).
+#B #C #M #Hlor elim Hlor -Hlor #HM /2/
+qed.
+
+lemma lor_sat0: ∀B,C. SAT0 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat1: ∀B,C. SAT1 (lor_mem B C).
+/3/ qed.
+
+lemma lor_sat2: ∀B,C. SAT2 (lor_mem B C).
+#B #C #N #L #M #l #HN #HL #HM elim HM -HM #HM /3/
+qed.
+
+lemma lor_sat3: ∀B,C. SAT3 (lor_mem B C).
+#B #C #N #l1 #l2 #HN elim HN -HN #HN /3/
+qed.
+
+lemma lor_sat4: ∀B,C. SAT4 (lor_mem B C).
+#B #C #N #HN elim HN -HN #HN /3/
+qed.
+
+definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
+/2/ qed.