From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 12 Sep 2010 16:55:11 +0000 (+0000)
Subject: Change (or better define) the order of hints premises.
X-Git-Tag: make_still_working~2832
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d7f1e8403bebcfc759d0955bd2f5a4837c414b2;p=helm.git

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).
---

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.