From 7d7f1e8403bebcfc759d0955bd2f5a4837c414b2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 12 Sep 2010 16:55:11 +0000
Subject: [PATCH] Change (or better define) the order of hints premises.

They are now processed top to bottom, and not viceversa as before. This seems
to be right thing, since rules like:

  X := carr T
  ....
  R := mk_foo ... (P X) ... T ...
 --------------------------------- |-
  carr R = (P X)

can't be written putting X := carr T last, but you really want to be sure that
the needed assumptions to obtain a foo (in that case, that X is the carrier of
a setoid T) are available _before_ you even try to typecheck the bigger
unification problem (that may not be well typed if X and carr T are not
_convertible_, since in the fix function called in instantiate we call the
typechecker and not the refiner).
---
 .../components/ng_refiner/nCicUnification.ml  |   2 +-
 .../matita/nlibrary/hints_declaration.ma      |   3 +
 .../software/matita/nlibrary/re/re-setoids.ma | 212 ++++++++++++++----
 3 files changed, 171 insertions(+), 46 deletions(-)

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index cc103a8ab..deb743d90 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -694,7 +694,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
                 List.fold_left 
                   (fun (metasenv, subst) (x,y) ->
                      unify rdb test_eq_only metasenv subst context x y false)
-                  (metasenv, subst) premises
+                  (metasenv, subst) (List.rev premises)
               in
               pp(lazy("FUNZIONA!"));
               Some (metasenv, subst)
diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index 3df2db001..99aca7fa6 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -34,6 +34,9 @@ With unidoce and some ASCII art it looks like the following:
  (*---------------------*) ⊢
          T1 ≡ T2       
 
+The order of premises is relevant, since they are processed in order
+(left to right).
+
 *)
    
 (* it seems unbelivable, but it works! *)
diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma
index a340fadf7..41a43894d 100644
--- a/helm/software/matita/nlibrary/re/re-setoids.ma
+++ b/helm/software/matita/nlibrary/re/re-setoids.ma
@@ -19,6 +19,13 @@ 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 *)
+notation < "hvbox(a break mpadded width -50% (=)= b)" non associative with precedence 45 for @{ 'eq_low $a $b }.
+notation > "a == b" non associative with precedence 45 for @{ 'eq_low $a $b }.
+
+
+(* XXX move to lists.ma *)
 ninductive list (A:Type[0]) : Type[0] ≝ 
   | nil: list A
   | cons: A -> list A -> list A.
@@ -28,24 +35,31 @@ match l1 with
 [ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
 | cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
    
+interpretation "eq_list" 'eq_low a b = (eq_list ? a b).
+   
 ndefinition LIST : setoid → setoid.
-#S; @(list S); @(eq_list S); ncases admit; nqed.  
+#S; @(list S); @(eq_list S);
+##[ #l; nelim l; //; #; @; //;
+##| #l1; nelim l1; ##[ #y; ncases y; //] #x xs H y; ncases y; ##[*] #y ys; *; #; @; /2/;
+##| #l1; nelim l1; ##[ #l2 l3; ncases l2; ncases l3; /3/; #z zs y ys; *] 
+    #x xs H l2 l3; ncases l2; ncases l3; /2/; #z zs y yz; *; #H1 H2; *; #H3 H4; @; /3/;##]
+nqed.
 
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 unification hint 0 ≔ S : setoid;
+  T ≟ carr S,
   P1 ≟ refl ? (eq0 (LIST S)),
   P2 ≟ sym ? (eq0 (LIST S)),
   P3 ≟ trans ? (eq0 (LIST S)),
-  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3),
-  T ≟ carr S
+  X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
      carr X ≡ list T.
 
-unification hint 0 ≔ S,a,b;
-   R ≟ LIST S,
+unification hint 0 ≔ S:setoid,a,b:list S;
+   R ≟ eq0 (LIST S),
    L ≟ (list S)
 (* -------------------------------------------- *) ⊢
-   eq_list S a b ≡ eq_rel L (eq0 R) a b.
+   eq_list S a b ≡ eq_rel L R a b.
 
 notation "hvbox(hd break :: tl)"
   right associative with precedence 47
@@ -74,9 +88,13 @@ ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l.
 
 ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z. 
 
-
 ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply (refl ???) |#a;#x1;#H;nnormalize;/2/]nqed.
+
+nlet rec flatten S (l : list (list S)) on l : list S ≝ 
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+(* end move to list *)
 
 interpretation "iff" 'iff a b = (iff a b).  
 
@@ -102,8 +120,8 @@ nlemma eq_rect_CProp0_r:
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
 nqed.
 
-notation < "a = b" non associative with precedence 45 for @{ 'eqpp $a $b}.
-interpretation "bool eq" 'eqpp a b = (eq bool a b). 
+(* XXX move to bool *)
+interpretation "bool eq" 'eq_low a b = (eq bool a b). 
 
 ndefinition BOOL : setoid.
 @bool; @(eq bool); ncases admit.nqed.
@@ -119,10 +137,10 @@ unification hint 0 ≔ ;
      carr X ≡ bool.
 
 unification hint 0 ≔ a,b;
-   R ≟ BOOL,
+   R ≟ eq0 BOOL,
    L ≟ bool
 (* -------------------------------------------- *) ⊢
-   eq bool a b ≡ eq_rel L (eq0 R) a b.
+   eq bool a b ≡ eq_rel L R a b.
 
 nrecord Alpha : Type[1] ≝ { 
    acarr :> setoid;
@@ -130,8 +148,7 @@ nrecord Alpha : Type[1] ≝ {
    eqb_true: ∀x,y. (eqb x y = true) = (x = y)
 }.
  
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
+interpretation "eqb" 'eq_low a b = (eqb ? a b).
 
 ninductive re (S: Type[0]) : Type[0] ≝
    z: re S
@@ -141,26 +158,49 @@ ninductive re (S: Type[0]) : Type[0] ≝
  | o: re S → re S → re S
  | k: re S → re S.
  
-naxiom eq_re : ∀S:Alpha.re S → re S → CProp[0].
+nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝ 
+  match a with
+  [ z ⇒ match b with [ z ⇒ True | _ ⇒ False]
+  | e ⇒ match b with [ e ⇒ True | _ ⇒ False]
+  | s x ⇒ match b with [ s y ⇒ x = y | _ ⇒ False]
+  | 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]].
+
 ndefinition RE : Alpha → setoid.
-#A; @(re A); @(eq_re A); ncases admit. nqed.
+#A; @(re A); @(eq_re A);
+##[ #p; nelim p; /2/;
+##| #p1; nelim p1; ##[##1,2: #p2; ncases p2; /2/;
+    ##|##2,3: #x p2; ncases p2; /2/;
+    ##|##4,5: #e1 e2 H1 H2 p2; ncases p2; /3/; #e3 e4; *; #; @; /2/;
+    ##|#r H p2; ncases p2; /2/;##]
+##| #p1; nelim p1;
+    ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+    ##| ##3: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+    ##| ##4,5: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+        ##[##1,3,4,5,6,8: #; ncases (?:False); //;##]
+        #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+    ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3: #; ncases (?:False); //]
+        #r2 r3; /3/; ##]##]
+nqed.
 
 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
 alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
 unification hint 0 ≔ A : Alpha;
+  S ≟ acarr A,
+  T ≟ carr S,
   P1 ≟ refl ? (eq0 (RE A)),
   P2 ≟ sym ? (eq0 (RE A)),
   P3 ≟ trans ? (eq0 (RE A)),
-  X ≟ mk_setoid (re A) (mk_equivalence_relation ? (eq_re A) P1 P2 P3),
-  T ≟ acarr A
+  X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
 (*-----------------------------------------------------------------------*) ⊢
-     carr X ≡ (re T).
+     carr X ≡ re T.
 
-unification hint 0 ≔ A,a,b;
-   R ≟ RE A,
+unification hint 0 ≔ A:Alpha,a,b:re A;
+   R ≟ eq0 (RE A),
    L ≟ re A
 (* -------------------------------------------- *) ⊢
-   eq_re A a b ≡ eq_rel L (eq0 R) a b.
+   eq_re A a b ≡ eq_rel L R a b.
 
 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
 notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
@@ -186,9 +226,6 @@ interpretation "empty" 'empty_r = (z ?).
 notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
 notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
 
-nlet rec flatten S (l : list (list S)) on l : list S ≝ 
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
 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 ].
 
@@ -231,6 +268,85 @@ ninductive pitem (S: Type[0]) : Type[0] ≝
  | po: pitem S → pitem S → pitem S
  | pk: pitem S → pitem S.
  
+nlet rec eq_pitem  (S : Alpha) (p1, p2 : pitem S) on p1 : CProp[0] ≝ 
+ match p1 with
+ [ pz ⇒ match p2 with [ pz ⇒ True | _ ⇒ False]
+ | pe ⇒ match p2 with [ pe ⇒ True | _ ⇒ False]
+ | ps x ⇒ match p2 with [ ps y ⇒ x = y | _ ⇒ False]
+ | pp x ⇒ match p2 with [ pp y ⇒ x = y | _ ⇒ False]
+ | pc a1 a2 ⇒ match p2 with [ pc b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | po a1 a2 ⇒ match p2 with [ po b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | pk a ⇒ match p2 with [ pk b ⇒ eq_pitem ? a b | _ ⇒ False]].
+ 
+interpretation "eq_pitem" 'eq_low a b = (eq_pitem ? a b). 
+ 
+nlemma PITEM : ∀S:Alpha.setoid.
+#S; @(pitem S); @(eq_pitem …);
+##[ #p; nelim p; //; nnormalize; #; @; //;
+##| #p; nelim p; ##[##1,2: #y; ncases y; //; ##|##3,4: #x y; ncases y; //; #; napply (?^-1); nassumption;
+    ##|##5,6: #r1 r2 H1 H2 p2; ncases p2; //; #s1 s2; nnormalize; *; #; @; /2/;
+    ##| #r H y; ncases y; //; nnormalize; /2/;##]
+##| #x; nelim x; 
+    ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+    ##| ##3,4: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+    ##| ##5,6: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+        ##[##1,2,5,6,7,8,4,10: #; ncases (?:False); //;##]
+        #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+    ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3,4: #; ncases (?:False); //]
+        #r2 r3; /3/; ##]##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ SS:Alpha;
+    S ≟ acarr SS,
+    A ≟ carr S,
+    P1 ≟ refl ? (eq0 (PITEM SS)),
+    P2 ≟ sym ? (eq0 (PITEM SS)),
+    P3 ≟ trans ? (eq0 (PITEM SS)),
+    R ≟ mk_setoid (pitem S) (mk_equivalence_relation (pitem A) (eq_pitem SS) P1 P2 P3)
+(*---------------------------*)⊢
+    carr R ≡ pitem A.
+    
+unification hint 0 ≔ S:Alpha,a,b:pitem S;
+   R ≟ PITEM S,
+   L ≟ (pitem S)
+(* -------------------------------------------- *) ⊢
+   eq_pitem S a b ≡ eq_rel L (eq0 R) a b.    
+    
+(* XXX move to pair.ma *)   
+nlet rec eq_pair (A, B : setoid) (a : A × B) (b : A × B) on a : CProp[0] ≝ 
+  match a with [ mk_pair a1 a2 ⇒ 
+  match b with [ mk_pair b1 b2 ⇒ a1 = b1 ∧ a2 = b2 ]].
+
+interpretation "eq_pair" 'eq_low a b = (eq_pair ?? a b). 
+
+nlemma PAIR : ∀A,B:setoid. setoid.
+#A B; @(A × B); @(eq_pair …);
+##[ #ab; ncases ab; #a b; @; napply #;
+##| #ab cd; ncases ab; ncases cd; #a1 a2 b1 b2; *; #E1 E2;
+    @; napply (?^-1); //;
+##| #a b c; ncases a; ncases b; ncases c; #c1 c2 b1 b2 a1 a2;
+    *; #E1 E2; *; #E3 E4; @; ##[ napply (.= E1); //] napply (.= E2); //.##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ AA, BB;
+    A ≟ carr AA, B ≟ carr BB,
+    P1 ≟ refl ? (eq0 (PAIR AA BB)),
+    P2 ≟ sym ? (eq0 (PAIR AA BB)),
+    P3 ≟ trans ? (eq0 (PAIR AA BB)),
+    R ≟ mk_setoid (A × B) (mk_equivalence_relation ? (eq_pair …) P1 P2 P3)
+(*---------------------------------------------------------------------------*)⊢
+    carr R ≡ A × B.
+ 
+unification hint 0 ≔ S1,S2,a,b;
+   R ≟ PAIR S1 S2,
+   L ≟ (pair S1 S2)
+(* -------------------------------------------- *) ⊢
+   eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.    
+
+(* end move to pair *) 
+ 
 ndefinition pre ≝ λS.pitem S × bool.
 
 notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
@@ -293,7 +409,7 @@ unification hint 0 ≔ SS : setoid;
 (*-----------------------------------------------------------------*) ⊢ 
   list S ≡ carr1 TT.
 
-(* Ex setoid support *)
+(* 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.
@@ -334,8 +450,7 @@ nqed.
 
 ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
 #S r; @(𝐋\p r); #w1 w2 E; nelim r; 
-##[ /2/;
-##| /2/;
+##[ ##1,2: /2/;
 ##| #x; @; *;
 ##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
     napply ((.=_0 H) E^-1);
@@ -482,37 +597,44 @@ napply (.=_1 (cupA…));
 //;
 nqed.
 
-FINQUI
 
-manca setoide per pair (e pre)
+(* XXX problem: auto does not find # (refl) when it has a concrete == *)
+nlemma odotEt : ∀S:Alpha.∀e1,e2:pitem S.∀b2:bool.
+  〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
+#S e1 e2 b2; ncases b2; nnormalize; @; //; @; napply refl; nqed.
 
-nlemma odotEt : 
-  ∀S:Alpha.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = ?.〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
-#S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
+nlemma LcatE : ∀S:Alpha.∀e1,e2:pitem S.
+  𝐋\p (e1 · e2) =  𝐋\p e1 · 𝐋  |e2| ∪ 𝐋\p e2. //; nqed.
 
-nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) =  𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed.
-
-nlemma cup_dotD : ∀S.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r). 
-#S p q r; napply extP; #w; nnormalize; @; 
+nlemma cup_dotD : ∀S:Alpha.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r). 
+#S p q r; napply ext_set; #w; nnormalize; @; 
 ##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
 ##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
 nqed.
 
 
-nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| =  𝐋 .|e1| · 𝐋 .|e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
+nlemma erase_dot : ∀S:Alpha.∀e1,e2:pitem S.𝐋 |e1 · e2| =  𝐋 |e1| · 𝐋 |e2|.
+#S e1 e2; napply ext_set; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
 nqed.
 
-nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 .|e1 + e2| =  𝐋 .|e1| ∪ 𝐋 .|e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
+nlemma erase_plus : ∀S:Alpha.∀e1,e2:pitem S.𝐋 |e1 + e2| =  𝐋 |e1| ∪ 𝐋 |e2|.
+#S e1 e2; napply ext_set; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
 
-nlemma erase_star : ∀S.∀e1:pitem S.𝐋 .|e1|^* = 𝐋 .|e1^*|. //; nqed.
+nlemma erase_star : ∀S:Alpha.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
 
-ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
+ndefinition substract := λS:Alpha.λp,q:lang S.{ w | w ∈ p ∧ ¬ w ∈ q }.
 interpretation "substract" 'minus a b = (substract ? a b).
 
-nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
-#S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed.
+FINQUI: manca ext per substract
+
+nlemma memnil : ∀S:Alpha.∀a:list S. a ∈ {[]} → a = [ ].
+#S a; ncases a; //; nqed.
+
+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 sub0 : ∀S.∀a:word S → Prop. a - {} = a.
 #S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
-- 
2.39.2