X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Frc_sat.ma;h=3eb04315f4f471a07e314b14086a574dc1cc0067;hb=d2b59bd89f761a16a2dbc663f446b4f95c767b83;hp=ddbafc71afc14a9ab0f2c64165d5feef69a28724;hpb=bfafdf7d8313ddd24c06d8ce3bba874f780403a9;p=helm.git

diff --git a/matita/matita/lib/lambda/rc_sat.ma b/matita/matita/lib/lambda/rc_sat.ma
index ddbafc71a..3eb04315f 100644
--- a/matita/matita/lib/lambda/rc_sat.ma
+++ b/matita/matita/lib/lambda/rc_sat.ma
@@ -29,8 +29,11 @@ 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,
  * the projections sat0 and sat1 are not generated
@@ -65,21 +68,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 +93,89 @@ 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. ************************************)
+*)
+(* 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).
-#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) /2 by SAT0_sort/ /3/ (**) (* adiacent auto *)
+lemma dep_cr1: ∀B,C. CR1 (dep_mem B C).
+#B #C #M #Hdep (lapply (Hdep (Sort 0) ?)) -Hdep /3/ @SAT0_sort //
 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 #M #N #l #H #L #HL <appl_append @sat3 /2/
+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.