some more work

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 41a43894d7a8ae8afb02355cf513f60a3c064b10..ced520b05abf2276999e04ad0409131b9742cc9b 100644 (file)
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -166,6 +166,8 @@ nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝
   | c r1 r2 ⇒ match b with [ c s1 s2 ⇒ eq_re ? r1 s1 ∧ eq_re ? r2 s2 | _ ⇒ False]
   | o r1 r2 ⇒ match b with [ o s1 s2  ⇒ eq_re ? r1 s1 ∧ eq_re ? r2 s2 | _ ⇒ False] 
   | k r1 ⇒ match b with [ k r2 ⇒ eq_re ? r1 r2 | _ ⇒ False]].
+  
+interpretation "eq_re" 'eq_low a b = (eq_re ? a b).
 
 ndefinition RE : Alpha → setoid.
 #A; @(re A); @(eq_re A);
@@ -229,8 +231,10 @@ notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S)
 nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
 match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
 
+(*
 ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
 interpretation "sing lang" 'singl x = (sing_lang ? x).
+*)
 
 interpretation "subset construction with type" 'comprehension t \eta.x = 
   (mk_powerclass t x).
@@ -622,32 +626,34 @@ nlemma erase_plus : ∀S:Alpha.∀e1,e2:pitem S.𝐋 |e1 + e2| =  𝐋 |e1| ∪
 
 nlemma erase_star : ∀S:Alpha.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
 
-ndefinition substract := λS:Alpha.λp,q:lang S.{ w | w ∈ p ∧ ¬ w ∈ q }.
-interpretation "substract" 'minus a b = (substract ? a b).
-
-FINQUI: manca ext per substract
+nlemma mem_single : ∀S:setoid.∀a,b:S. a ∈ {(b)} → a = b.
+#S a b; nnormalize; /2/; nqed.
 
-nlemma memnil : ∀S:Alpha.∀a:list S. a ∈ {[]} → a = [ ].
-#S a; ncases a; //; nqed.
+notation < "[\setoid\emsp\of\emsp term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
+interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
 
-nlemma cup_sub: ∀S:Alpha.∀a,b:Elang S. ¬ ([]∈ a) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
-#S a b c; napply ext_set; #w; @; 
-##[ *; ##[ #wa; @; ##[@;//] #H; napply c; napply (. ?╪_0?); 
-    napply (. (memnil ?? H)^-1‡#); 
-/4/; *; /4/; nqed.
+nlemma cup_sub: ∀S.∀A,B:𝛀^S.∀x. ¬ (x ∈ A) → A ∪ (B - {(x)}) = (A ∪ B) - {(x)}.
+#S A B x H; napply ext_set; #w; @; 
+##[ *; ##[ #wa; @; ##[@;//] #H2; napply H; napply (. (mem_single ??? H2)^-1╪_1#); //]
+    *; #wb nwn; @; ##[@2;//] //;
+##| *; *; ##[ #wa nwn; @; //] #wb nwn; @2; @; //;##]
+nqed.
 
-nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
-#S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
+nlemma sub0 : ∀S.∀a:Ω^S. a - ∅ = a.
+#S a; napply ext_set; #w; nnormalize; @; /3/; *; //; nqed.
 
-nlemma subK : ∀S.∀a:word S → Prop. a - a = {}.
-#S a; napply extP; #w; nnormalize; @; *; /2/; nqed.
+nlemma subK : ∀S.∀a:Ω^S. a - a = ∅.
+#S a; napply ext_set; #w; nnormalize; @; *; /2/; nqed.
 
-nlemma subW : ∀S.∀a,b:word S → Prop.∀w.(a - b) w → a w.
+nlemma subW : ∀S.∀a,b:Ω^S.∀w.w ∈ (a - b) → w ∈ a.
 #S a b w; nnormalize; *; //; nqed.
 
-nlemma erase_bull : ∀S.∀a:pitem S. .|\fst (•a)| = .|a|.
+nlemma erase_bull : ∀S:Alpha.∀a:pitem S. |\fst (•a)| = |a|.
 #S a; nelim a; // by {};
-##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| · .|e2|);
+##[ #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (|e1| · |e2|);
+
+finqui: manca · morfismo, oppure un lemma che dice che == è come Leibnitz.
+
     nrewrite < IH1; nrewrite < IH2;  
     nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊙ 〈e2,false〉));
     ncases (•e1); #e3 b; ncases b; nnormalize;
@@ -655,7 +661,7 @@ nlemma erase_bull : ∀S.∀a:pitem S. .|\fst (•a)| = .|a|.
 ##| #e1 e2 IH1 IH2; nchange in ⊢ (???%) with (.|e1| + .|e2|);
     nrewrite < IH2; nrewrite < IH1;
     nchange in ⊢ (??(??%)?) with (\fst (•e1 ⊕ •e2));
-    ncases (•e1); ncases (•e2); //;
+    ncases (•e1); ncases (•e2); //]
 ##| #e IH; nchange in ⊢ (???%) with (.|e|^* ); nrewrite < IH;
     nchange in ⊢ (??(??%)?) with (\fst (•e))^*; //; ##]
 nqed.