Setoid-Rewriting under Ex works for an arbitrary depth of Ex. Patches needed:

Index: ../components/ng_refiner/nCicUnification.ml
===================================================================
--- ../components/ng_refiner/nCicUnification.ml	(revision 10941)
+++ ../components/ng_refiner/nCicUnification.ml	(working copy)
@@ -97,7 +97,7 @@
    let time2 = Unix.gettimeofday () in
    let time1 =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
-   prerr_endline ("}}} " ^ string_of_float (time2 -. time1));
+   prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
@@ -730,6 +730,32 @@
               | Uncertain _ as exn -> raise exn
               | _ -> assert false
     in
+    let fo_unif_heads_and_cont_or_unwind_and_hints
+      test_eq_only metasenv subst m1 m2 cont hm1 hm2
+     =
+      let ms, continuation =
+        (* calling the continuation inside the outermost try is an option
+           and makes unification stronger, but looks not frequent to me
+           that heads unify but not the arguments and that an hints can fix
+           that *)
+        try fo_unif test_eq_only metasenv subst m1 m2, cont
+        with
+        | UnificationFailure _
+        | KeepReducing _ | Uncertain _ as exn ->
+           let (t1,norm1),(t2,norm2) = hm1, hm2 in
+           match
+             try_hints metasenv subst
+              (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+           with
+            | Some x -> x, fun x -> x
+            | None ->
+                match exn with
+                | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+                | UnificationFailure _ | Uncertain _ as exn -> raise exn
+                | _ -> assert false
+      in
+        continuation ms
+    in
     let height_of = function
      | NCic.Const (Ref.Ref (_,Ref.Def h))
      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
@@ -767,7 +793,7 @@
             match t1 with
             | C.Const r -> NCicEnvironment.get_relevance r
             | _ -> [] *) in
-          let unif_from_stack t1 t2 b metasenv subst =
+          let unif_from_stack (metasenv, subst) (t1, t2, b) =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
@@ -784,14 +810,19 @@
                 NCicReduction.unwind (k2,e2,t2,List.rev l2),
                 todo
           in
-        let hh1,hh2,todo=check_stack (List.rev s1) (List.rev s2) relevance [] in
+          let check_stack l1 l2 r =
+            match t1, t2 with
+            | NCic.Meta _, _ | _, NCic.Meta _ ->
+                (NCicReduction.unwind (k1,e1,t1,s1)),
+                (NCicReduction.unwind (k2,e2,t2,s2)),[]
+            | _ -> check_stack l1 l2 r []
+          in
+        let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
         try
-         let metasenv,subst =
-          fo_unif_w_hints test_eq_only metasenv subst (norm1,hh1) (norm2,hh2) in
-         List.fold_left
-          (fun (metasenv,subst) (x1,x2,r) ->
-            unif_from_stack x1 x2 r metasenv subst
-          ) (metasenv,subst) todo
+          fo_unif_heads_and_cont_or_unwind_and_hints
+            test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
+            (fun ms -> List.fold_left unif_from_stack ms todo)
+            m1 m2
         with
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->

diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index ced520b05abf2276999e04ad0409131b9742cc9b..ef533aab3586e7be0b6932440d91e5cec7900fba 100644 (file)
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -16,8 +16,10 @@ include "datatypes/pairs.ma".
 include "datatypes/bool.ma".
 include "sets/sets.ma".
 
+(*
 ninductive Admit : CProp[0] ≝ .
 naxiom admit : Admit.
+*)
 
 (* single = is for the abstract equality of setoids, == is for concrete 
    equalities (that may be lifted to the setoid level when needed *)
@@ -124,7 +126,7 @@ nqed.
 interpretation "bool eq" 'eq_low a b = (eq bool a b). 
 
 ndefinition BOOL : setoid.
-@bool; @(eq bool); ncases admit.nqed.
+@bool; @(eq bool); nnormalize; //; #x y; ##[ #E; ncases E; ##| #y H; ncases H; ##] //; nqed.
 
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)".
@@ -413,43 +415,158 @@ unification hint 0 ≔ SS : setoid;
 (*-----------------------------------------------------------------*) ⊢ 
   list S ≡ carr1 TT.
 
+(* not as morphism *)
+nlemma Not_morphism : CProp[0] ⇒_1 CProp[0].
+@(λx:CProp[0].¬ x); #a b; *; #; @; /3/; nqed.
+
+unification hint 0 ≔ P : CProp[0];
+   A ≟ CPROP, 
+   B ≟ CPROP,
+   M ≟ mk_unary_morphism1 ?? (λP.¬ P) (prop11 ?? Not_morphism)
+(*------------------------*)⊢
+  fun11 A B M P ≡ ¬ P.
+
 (* XXX Ex setoid support *)
-nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
-  ∀y,z:T.y = z → (∀x.y=z → P x y = P x z)  → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
-#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
+nlemma Ex_morphism : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: S ⇒_1 CProp[0].Ex S P); #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : S ⇒_1 CProp[0];
+   A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
+   B ≟ CPROP,
+   M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S P) 
+        (prop11 ?? (Ex_morphism S))
+(*------------------------*)⊢
+  fun11 A B M P ≡ Ex S (fun11 S CPROP P).
+
+nlemma Ex_morphism_eta : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: S ⇒_1 CProp[0].Ex S (λx.P x)); #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : S ⇒_1 CProp[0];
+   A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP, 
+   B ≟ CPROP,
+   M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S (λx.P x)) 
+        (prop11 ?? (Ex_morphism_eta S))
+(*------------------------*)⊢
+  fun11 A B M P ≡ Ex S (λx.fun11 S CPROP P x).
+
+nlemma Ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
+#T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
+
+unification hint 0 ≔ T,P ; 
+   S ≟ (Ex_setoid T P) 
+(*---------------------------*) ⊢
+   Ex T (λx:T.P x) ≡ carr S.
+
+(* couts how many Ex we are traversing *)
+ninductive counter : Type[0] ≝ 
+ | End : counter 
+ | Next : (bool → bool) → (* dummy arg please the notation mechanism *)
+          counter → counter. 
+
+(* to rewrite terms (live in setoid) *)
+nlet rec mk_P (S, T : setoid) (n : counter) on n ≝ 
+  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
+
+nlet rec mk_F (S, T : setoid) (n : counter) on n ≝ 
+  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
+  
+nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λf,g:T. f = g 
+  | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
+
+nlet rec mk_H (S, T : setoid) (n : counter) on n : 
+∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g 
+  | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m). 
+              ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex (S, T : setoid) (n : counter) on n : 
+∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λP:mk_P S T End.λf:T. P f 
+  | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m). 
+              ∃x:S.mk_Ex S T m (P x) (f x) ].
+
+nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
+  mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.
 
-notation "∑" non associative with precedence 90 for @{Sig ?????}.
+(* to rewrite propositions (live in setoid1) *)
+nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
+  match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
 
-nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
-#S m x y E;
-napply (.=_1 (∑ E (λw,H.(H ╪_1 #)╪_1 #))).
-napply #.
+nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝ 
+  match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
+  
+nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λf,g:T. f =_1 g 
+  | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
+
+nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n : 
+∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝ 
+  match n with 
+  [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g 
+  | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m). 
+              ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n : 
+∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝ 
+  match n with 
+  [ End ⇒ λP:mk_P1 S T End.λf:T. P f 
+  | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m). 
+              ∃x:S.mk_Ex1 S T m (P x) (f x) ].
+
+nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
+  mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
 nqed.
 
+(* notation "∑x1,...,xn. E / H ; P" were:
+   - x1...xn are bound in E and P, H is bound in P
+   - H is an identifier that will have the type of E in P
+   - P is the proof that the two existentially quantified predicates are equal*)
+notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20 
+for @{ 'Sig_gen 
+  ${ fold right @{ 'End }  rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
+  ${ fold right @{ $E }              rec acc @{ λ${ident x}.$acc } } 
+  ${ fold right @{ λ${ident nE}.$H } rec acc @{ λ${ident x}.$acc } }
+}.
+
+interpretation "next" 'Next x y = (Next x y).
+interpretation "end" 'End = End.
+(*interpretation "sig_gen" 'Sig_gen n E H = (Sig_generic  ?? n ??? E H).*)
+interpretation "sig_gen1" 'Sig_gen n E H = (Sig_generic1 ?? n ??? E H).
+
+nlemma test0 : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w))) =_1 (Ex S (λw.P (g w))).
+#S P f g E; napply (∑w. E w / H ; ┼_1H); nqed.
+
+nlemma test : ∀S:setoid. ∀P: S ⇒_1 CPROP.∀f,g:S → S.
+ (∀x:S.f x = g x) → (Ex S (λw.P (f w)∧ True)) =_1 (Ex S (λw.P (g w)∧ True)).
+#S P f g E; napply (∑w. E w / H ; (┼_1H)╪_1#); nqed. 
+
+nlemma test_bound : ∀S:setoid. ∀e,f: S ⇒_1 CPROP. e = f → 
+   (Ex S (λw.e w ∧ True)) =_1 (Ex S (λw.f w ∧ True)).
+#S f g E; napply (.=_1 ∑x. E x x # / H ; (H ╪_1 #)); //; nqed.
+
 nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
  ∀x,y:setoid1_of_setoid S.x =_1 y → 
    (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
-#S m x y E;
-napply (.=_1 #╪_1(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
-napply #.
-nqed.
-
-nlemma ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
-#T P; @ (Ex T (λx:T.P x)); @;
-##[ #H1 H2; napply True |##*: //; ##]
-nqed.
-
-unification hint 0 ≔ T,P ; S ≟ (ex_setoid T P) ⊢
- Ex T (λx:T.P x) ≡ carr S.
+#S m x y E; napply (.=_1 #╪_1(∑w. E / E ; ((E ╪_1 #) ╪_1 #))). //; nqed.
 
 nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
  ∀x,y:setoid1_of_setoid S.x =_1 y → 
    ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
-#S m x y E;
-napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
-napply #.
-nqed.
+#S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
+
 (* Ex setoid support end *)
 
 ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
@@ -458,24 +575,20 @@ ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
 ##| #x; @; *;
 ##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
     napply ((.=_0 H) E^-1);
-##| #e1 e2 H1 H2; 
+##| #e1 e2 H1 H2; (*
     nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
-    nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+    nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?); good! *)
     napply (.= (#‡H2));
-    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))╪_1 #); ##[
-      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
-        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
-      napply ( (X‡#)‡#); ##]
-    napply #;
-##| #e1 e2 H1 H2;
-    nnormalize in ⊢ (???%%);
-    napply (H1‡H2);
-##| #e H; nnormalize in ⊢ (???%%);
-    napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))); ##[
-      ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
-        @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
-      napply ((X‡#)‡#); ##]
-    napply #;##] 
+    ncut (∀x1,x2. (w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+      #x1 x2; @; #X; ##[ napply ((.= E^-1) X) | napply ((.= E) X) ] ##] #X;
+    napply ((∑w1,w2. X w1 w2 / H ; (H╪_1#)╪_1#) ╪_1 #); 
+##| #e1 e2 H1 H2; napply (H1‡H2); (* good! *)
+##| #e H; 
+    ncut (∀x1,x2.(w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+      #x1 x2; @; #X; ##[ napply ((.= E^-1) X) | napply ((.= E) X) ] ##] #X;
+    (* nnormalize in ⊢ (???%%); good! (but a bit too hard) *)
+    napply (∑w1,w2. X w1 w2 / H ; (H╪_1#)╪_1#); 
+##]
 nqed.
 
 unification hint 0 ≔ S : Alpha,e : pitem S; 
@@ -588,10 +701,10 @@ ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to
 
 (* theorem 16: 2 *)
 nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2.
-#S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2;
+#S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2; (* oh my!
 nwhd in ⊢ (???(??%)?);
 nchange in ⊢(???%?) with (𝐋\p (e1 + e2) ∪ ϵ (b1 || b2));
-nchange in ⊢(???(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2));
+nchange in ⊢(???(??%?)?) with (𝐋\p (e1) ∪ 𝐋\p (e2)); *)
 napply (.=_1 #╪_1 (epsilon_or ???));
 napply (.=_1 (cupA…)^-1);
 napply (.=_1 (cupA…)╪_1#);