A failing unification of a coercion vs a term is now tried again after

a delta-beta weak head reduction of the coercion. This is necessary to handle
the case (f (g ?)) vs (fg t) where f and g are coercions and fg is the
composite coercion.

As a result the notation in algebra is now nicer and more notation can be
parsed.

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index c93c9d94c9757e0d1f3cfdaaa2aac452e8c0272a..bec57fb4c2ca845a9d49bcd511c74b15a44e81bb 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -104,13 +104,15 @@ record finite_enumerable (T:Type) : Type ≝
    repr_index_of: ∀x. repr (index_of x) = x
  }.
  
-notation < "hvbox(C \sub i)" with precedence 89
+notation "hvbox(C \sub i)" with precedence 89
 for @{ 'repr $C $i }.
 
+(* CSC: multiple interpretations in the same file are not considered in the
+ right order
 interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/groups/repr.con C _ i).
+ (cic:/matita/algebra/groups/repr.con C _ i).*)
  
-notation < "hvbox(|C|)" with precedence 89
+notation "hvbox(|C|)" with precedence 89
 for @{ 'card $C }.
 
 interpretation "Finite_enumerable order" 'card C =
@@ -159,11 +161,7 @@ theorem foo:
   right_cancellable ? (op G) →
    ∃e:G. isMonoid G e.
 intros;
-letin f ≝
- (λn.index_of G (is_finite_enumerable G)
-  (op G
-   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) O)
-   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) n)));
+letin f ≝ (λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
 [ letin EX ≝ (Hcut O ?);
   [ apply le_O_n
@@ -175,7 +173,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
     clearbody HH;
     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
-    apply (ex_intro ? ? (repr ? (is_finite_enumerable G) a));
+    apply (ex_intro ? ? (G \sub a));
     letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
     clearbody GOGO;
     rewrite < HH in GOGO;
@@ -186,13 +184,13 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clear GOGO;
     constructor 1;
     [ unfold is_left_unit; intro;
-      letin GaxGax ≝ (refl_eq ? ((repr ? (is_finite_enumerable G) a)·x));
+      letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite > (semigroup_properties G) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (x·(repr ? (is_finite_enumerable G) a)));
+      letin GaxGax ≝ (refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite < (semigroup_properties G) in GaxGax;

diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma
index 7c40db1fd89bffad6aefb0b284c01f10e4f1b169..cf1e531f47c01b90e2633caa00952fc71f76fb42 100644 (file)
--- a/helm/matita/library/algebra/monoids.ma
+++ b/helm/matita/library/algebra/monoids.ma
@@ -51,12 +51,12 @@ interpretation "Semigroup coercion" 'semigroup M =
 definition is_left_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. op M (opp x) x = 1.
+   ∀x:M. (opp x)·x = 1.
    
 definition is_right_inverse ≝
  λM:Monoid.
   λopp: M → M.
-   ∀x:M. op M x (opp x) = 1.
+   ∀x:M. x·(opp x) = 1.
 
 theorem is_left_inverse_to_is_right_inverse_to_eq:
  ∀M:Monoid. ∀l,r.
@@ -64,7 +64,7 @@ theorem is_left_inverse_to_is_right_inverse_to_eq:
    ∀x:M. l x = r x.
  intros;
  generalize in match (H x); intro;
- generalize in match (eq_f ? ? (λy. op M y (r x)) ? ? H2);
+ generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
  simplify; fold simplify (op M);
  intro; clear H2;
  generalize in match (semigroup_properties M);

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index b1ef27f4ec9399e83cb9e2d366e97810f7f4e8ec..8deb6af4aed58807d89cc79d82e052ae7cdb08f1 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -571,8 +571,57 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                         fo_unif_l 
                           test_equality_only subst' metasenv' (l1,l2) ugraph1
               in
+              (try 
                 fo_unif_l 
-                  test_equality_only subst metasenv (lr1, lr2)  ugraph)
+                  test_equality_only subst metasenv (lr1, lr2)  ugraph
+              with 
+              | UnificationFailure _ as exn -> 
+                  (match l1, l2 with
+                  | (((Cic.Const (uri1, ens1)) as c1) :: tl1), 
+                     (((Cic.Const (uri2, ens2)) as c2) :: tl2) when
+                    CoercGraph.is_a_coercion c1 && 
+                    CoercGraph.is_a_coercion c2 ->
+                      let body1, attrs1, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri1 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u  -> bo, attrs,u
+                        | _ -> assert false
+                      in
+                      let body2, attrs2, ugraph = 
+                        match CicEnvironment.get_obj ugraph uri2 with
+                        | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+                        | _ -> assert false
+                      in
+                      let is_composite1 = 
+                        List.exists ((=) (`Class `Coercion)) attrs1 in
+                      let is_composite2 = 
+                        List.exists ((=) (`Class `Coercion)) attrs2 in
+                      (match is_composite1, is_composite2 with
+                      | false, false -> raise exn
+                      | true, false ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl = Cic.Appl (body1::tl1) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                              redappl t2 ugraph
+                      | false, true -> 
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl = Cic.Appl (body2::tl2) in
+                          let redappl = CicReduction.head_beta_reduce appl in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             t1 redappl ugraph
+                      | true, true ->
+                          let body1 = CicSubstitution.subst_vars ens1 body1 in
+                          let appl1 = Cic.Appl (body1::tl1) in
+                          let redappl1 = CicReduction.head_beta_reduce appl1 in
+                          let body2 = CicSubstitution.subst_vars ens2 body2 in
+                          let appl2 = Cic.Appl (body2::tl2) in
+                          let redappl2 = CicReduction.head_beta_reduce appl2 in
+                          fo_unif_subst 
+                            test_equality_only subst context metasenv 
+                             redappl1 redappl2 ugraph)
+                  | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2