From 57580552302fed78b66a674eb5cb5fd70abdac99 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Sep 2010 13:45:41 +0000
Subject: [PATCH] hints for \epsilon

---
 .../software/matita/nlibrary/re/re-setoids.ma | 83 ++++++++++++-------
 1 file changed, 54 insertions(+), 29 deletions(-)

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index 47295f3fd..03c830538 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -546,6 +546,51 @@ interpretation "epsilon" 'epsilon = (epsilon ?).
 notation < "ϵ b" non associative with precedence 90 for @{'app_epsilon $b}.
 interpretation "epsilon lang" 'app_epsilon b = (epsilon ? b).
 
+(* hints for epsilon *)
+nlemma epsilon_is_morph : ∀A:Alpha. (setoid1_of_setoid bool) ⇒_1 (lang A).
+#X; @; ##[#b; napply(ϵ b)] #a1 a2; ncases a1; ncases a2; //; *; nqed.
+
+nlemma epsilon_is_ext: ∀A:Alpha. (setoid1_of_setoid bool) → (Elang A).
+ #S b; @(ϵ b); #w1 w2 E; ncases b; @; ##[##3,4:*] 
+nchange in match (w1 ∈ ϵ true) with ([] =_0 w1);
+nchange in match (w2 ∈ ϵ true) with ([] =_0 w2); #H; napply (.= H); /2/;
+nqed.
+
+alias symbol "hint_decl" = "hint_decl_Type1".
+unification hint 0 ≔ A : Alpha, B :  bool;
+   AA ≟ LIST (acarr A),
+   R ≟ mk_ext_powerclass ? 
+         (ϵ B) (ext_prop ? (epsilon_is_ext ? B))
+(*--------------------------------------------------------------------*)  ⊢
+    ext_carr AA R ≡ epsilon A B.
+    
+unification hint 0 ≔ S:Alpha, A:bool;
+    B ≟ setoid1_of_setoid BOOL,
+    T ≟ powerclass_setoid (list (carr (acarr S))),
+    MM ≟ mk_unary_morphism1 B T 
+               (λB.ϵ B) (prop11 B T (epsilon_is_morph S))
+(*--------------------------------------------------------------------------*) ⊢
+   fun11 B T MM A ≡ epsilon S A.
+   
+nlemma epsilon_is_ext_morph:∀A:Alpha. (setoid1_of_setoid bool) ⇒_1 (Elang A).
+#A; @(epsilon_is_ext …);
+#x1 x2 Ex; napply (prop11 … (epsilon_is_morph A)); nassumption.
+nqed.
+
+unification hint 1 ≔ AA : Alpha, B : bool;
+  AAS ≟ LIST (acarr AA), 
+  BB ≟ setoid1_of_setoid BOOL,
+  T ≟ ext_powerclass_setoid AAS,
+  R ≟ mk_unary_morphism1 BB T
+            (λS.
+              mk_ext_powerclass AAS (epsilon AA S) 
+                (ext_prop AAS (epsilon_is_ext AA S)))
+            (prop11 BB T (epsilon_is_ext_morph AA))
+(*------------------------------------------------------*) ⊢
+   ext_carr AAS (fun11 BB T R B) ≡ epsilon AA B.
+
+(* end hints for epsilon *)
+
 ndefinition L_pr ≝ λS : Alpha.λp:pre S.  𝐋\p\ (\fst p) ∪ ϵ (\snd p).
   
 interpretation "L_pr" 'L_pi E = (L_pr ? E).
@@ -774,37 +819,17 @@ nlemma sub_dot_star :
     *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
     @ (w1 :: lw); @; ##[ napply (.=_0 # ╪_0 flx); napply (?^-1); //]
     @; //; napply (subW … sube);
-##| *; #wl; *; #defw Pwl; (*  STOP manca ext_carr vs epsilon. *)     
-ncases b; ##[ nchange in match (ϵtrue) with {[]}.
-napply (. (defw^-1 ╪_1 #)); nelim wl in Pwl; /2/;
-#s tl IH; *; #Xs Ptl; ncases s in Xs; ##[ #; napply IH; //] #x xs Xxxs;
-@; @(x :: xs); @(flatten ? tl); @; ##[ @; ##[ napply #] @; //; nassumption; ##]
-nelim tl in Ptl; ##[ #; @[]; /2/] #w ws IH; *; #Xw Pws; @(w :: ws); @; ##[ napply #]
-@; //;
-
-
-
- nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
-    #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
-    ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
-        @; ncases b in H1; #H1; 
-        ##[##2: nrewrite > (sub0…); @w'; @(w1@w2);
-                nrewrite > (associative_append ? w' w1 w2);
-                nrewrite > defwl'; @; ##[@;//] @(wl'); @; //;
-           ##| ncases w' in Pw';
-               ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //;
-               ##| #x xs Px; @(x::xs); @(w1@w2); 
-                   nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct]
-                   @wl'; @; //; ##] ##]
-        ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl');
-            nrewrite < (wlnil); nrewrite > (append_nil…); ncases b;
-            ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]);
-                nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct]
-                @[]; @; //;
-            ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //] 
-                @; //; @; //; @; *;##]##]##] 
+##| *; #wl; *; #defw Pwl; napply (. (defw^-1 ╪_1 #));
+    nelim wl in Pwl; /2/;
+    #s tl IH; *; #Xs Ptl; ncases s in Xs; ##[ #; napply IH; //] #x xs Xxxs;
+    @; @(x :: xs); @(flatten ? tl); @; 
+      ##[ @; ##[ napply #] @; ##[nassumption] ncases b; *; ##]
+    nelim tl in Ptl; ##[ #; @[]; /2/] #w ws IH; *; #Xw Pws; @(w :: ws); @; ##[ napply #]
+    @; //;##]
 nqed.
 
+STOP
+
 (* theorem 16: 1 *)
 alias symbol "pc" (instance 13) = "cat lang".
 alias symbol "in_pl" (instance 23) = "in_pl".
-- 
2.39.2