From 1db3c6d81f853f98f145cd9924dd18b79ca846e9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Jan 2006 17:50:09 +0000 Subject: [PATCH] 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. --- helm/matita/library/algebra/groups.ma | 20 ++++---- helm/matita/library/algebra/monoids.ma | 6 +-- helm/ocaml/cic_unification/cicUnification.ml | 51 +++++++++++++++++++- 3 files changed, 62 insertions(+), 15 deletions(-) diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma index c93c9d94c..bec57fb4c 100644 --- 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 7c40db1fd..cf1e531f4 100644 --- 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 b1ef27f4e..8deb6af4a 100644 --- 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 -- 2.39.2