include "algebra/monoids.ma".
include "nat/le_arith.ma".
-record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
- { opp_is_left_inverse: is_left_inverse M opp;
- opp_is_right_inverse: is_right_inverse M opp
+record PreGroup : Type ≝
+ { premonoid:> PreMonoid;
+ opp: premonoid -> premonoid
+ }.
+
+record isGroup (G:PreGroup) : Prop ≝
+ { is_monoid: isMonoid G;
+ opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
+ opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
}.
record Group : Type ≝
- { monoid: Monoid;
- opp: monoid -> monoid;
- group_properties: isGroup ? opp
+ { pregroup:> PreGroup;
+ group_properties:> isGroup pregroup
}.
-coercion cic:/matita/algebra/groups/monoid.con.
-
-notation < "G"
+(*notation < "G"
for @{ 'monoid $G }.
interpretation "Monoid coercion" 'monoid G =
- (cic:/matita/algebra/groups/monoid.con G).
+ (cic:/matita/algebra/groups/monoid.con G).*)
notation < "G"
for @{ 'type_of_group $G }.
(cic:/matita/algebra/groups/Type_of_Group.con G).
notation < "G"
-for @{ 'semigroup_of_group $G }.
+for @{ 'magma_of_group $G }.
-interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
- (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
+interpretation "magma_of_group coercion" 'magma_of_group G =
+ (cic:/matita/algebra/groups/Magma_of_Group.con G).
notation "hvbox(x \sup (-1))" with precedence 89
for @{ 'gopp $x }.
unfold left_cancellable;
unfold injective;
intros (x y z);
-rewrite < (e_is_left_unit ? ? (monoid_properties G));
-rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-rewrite > (semigroup_properties G);
-rewrite > (semigroup_properties G);
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_left_inverse ? (group_properties G) x);
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
apply eq_f;
assumption.
qed.
unfold injective;
simplify;fold simplify (op G);
intros (x y z);
-rewrite < (e_is_right_unit ? ? (monoid_properties G));
-rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
-rewrite < (semigroup_properties G);
-rewrite < (semigroup_properties G);
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_right_inverse ? (group_properties G) x);
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
rewrite > H;
reflexivity.
qed.
(cic:/matita/algebra/groups/order.con C _).
record finite_enumerable_SemiGroup : Type ≝
- { semigroup: SemiGroup;
- is_finite_enumerable: finite_enumerable semigroup
+ { semigroup:> SemiGroup;
+ is_finite_enumerable:> finite_enumerable semigroup
}.
-coercion cic:/matita/algebra/groups/semigroup.con.
-coercion cic:/matita/algebra/groups/is_finite_enumerable.con.
-
notation < "S"
for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
=
(cic:/matita/algebra/groups/semigroup.con S).
+notation < "S"
+for @{ 'magma_of_finite_enumerable_semigroup $S }.
+
+interpretation "Magma_of_finite_enumerable_semigroup"
+ 'magma_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S).
+
notation < "S"
for @{ 'type_of_finite_enumerable_semigroup $S }.
∀G:finite_enumerable_SemiGroup.
left_cancellable ? (op G) →
right_cancellable ? (op G) →
- ∃e:G. isMonoid G e.
+ ∃e:G. isMonoid (mk_PreMonoid G e).
intros;
letin f ≝ (λn.ι(G \sub O · G \sub n));
cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
- rewrite > (semigroup_properties G) in GOGO;
+ rewrite > (associative ? G) in GOGO;
letin GaGa ≝ (H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
constructor 1;
- [ unfold is_left_unit; intro;
+ [ simplify;
+ apply (semigroup_properties G)
+ | unfold is_left_unit; intro;
letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (semigroup_properties G) in GaxGax;
+ rewrite > (associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (semigroup_properties G) in GaxGax;
+ rewrite < (associative ? (semigroup_properties G)) in GaxGax;
apply (H1 ? ? ? GaxGax)
+ ]
]
|
-].
\ No newline at end of file
+].
include "algebra/semigroups.ma".
-record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝
- { e_is_left_unit: is_left_unit SS e;
- e_is_right_unit: is_right_unit SS e
+record PreMonoid : Type ≝
+ { magma:> Magma;
+ e: magma
+ }.
+
+notation < "M" for @{ 'pmmagma $M }.
+interpretation "premonoid magma coercion" 'pmmagma M =
+ (cic:/matita/algebra/monoids/magma.con M).
+
+record isMonoid (M:PreMonoid) : Prop ≝
+ { is_semi_group: isSemiGroup M;
+ e_is_left_unit:
+ is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
+ e_is_right_unit:
+ is_right_unit (mk_SemiGroup ? is_semi_group) (e M)
}.
record Monoid : Type ≝
- { semigroup: SemiGroup;
- e: semigroup;
- monoid_properties: isMonoid ? e
+ { premonoid:> PreMonoid;
+ monoid_properties:> isMonoid premonoid
}.
-
-coercion cic:/matita/algebra/monoids/semigroup.con.
-
-(* too ugly
-notation "hvbox(1 \sub S)" with precedence 89
-for @{ 'munit $S }.
-
-interpretation "Monoid unit" 'munit S =
- (cic:/matita/algebra/monoids/e.con S). *)
+notation < "M" for @{ 'semigroup $M }.
+interpretation "premonoid coercion" 'premonoid M =
+ (cic:/matita/algebra/monoids/premonoid.con M).
+
+notation < "M" for @{ 'typeofmonoid $M }.
+interpretation "premonoid coercion" 'typeofmonoid M =
+ (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
+
+notation < "M" for @{ 'magmaofmonoid $M }.
+interpretation "premonoid coercion" 'magmaofmonoid M =
+ (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
+
notation "1" with precedence 89
for @{ 'munit }.
interpretation "Monoid unit" 'munit =
(cic:/matita/algebra/monoids/e.con _).
-notation < "M"
-for @{ 'semigroup $M }.
-
-interpretation "Semigroup coercion" 'semigroup M =
- (cic:/matita/algebra/monoids/semigroup.con M).
-
definition is_left_inverse ≝
λM:Monoid.
λopp: M → M.
generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
simplify; fold simplify (op M);
intro; clear H2;
- generalize in match (semigroup_properties M);
- fold simplify (Type_of_Monoid M);
+ generalize in match (associative ? (is_semi_group ? (monoid_properties M)));
intro;
- unfold isSemiGroup in H2; unfold associative in H2;
rewrite > H2 in H3; clear H2;
rewrite > H1 in H3;
- rewrite > (e_is_left_unit ? ? (monoid_properties M)) in H3;
- rewrite > (e_is_right_unit ? ? (monoid_properties M)) in H3;
+ rewrite > (e_is_left_unit ? (monoid_properties M)) in H3;
+ rewrite > (e_is_right_unit ? (monoid_properties M)) in H3;
assumption.
qed.
include "higher_order_defs/functions.ma".
-definition isSemiGroup ≝
- λC:Type. λop: C → C → C.associative C op.
+(* Magmas *)
-record SemiGroup : Type ≝
- { carrier: Type;
- op: carrier → carrier → carrier;
- semigroup_properties: isSemiGroup carrier op
+record Magma : Type ≝
+ { carrier:> Type;
+ op: carrier → carrier → carrier
}.
-
-coercion cic:/matita/algebra/semigroups/carrier.con.
-notation "hvbox(a break \middot \sub S b)"
- left associative with precedence 55
-for @{ 'ptimes $S $a $b }.
+notation < "M" for @{ 'carrier $M }.
+interpretation "carrier coercion" 'carrier S =
+ (cic:/matita/algebra/semigroups/carrier.con S).
notation "hvbox(a break \middot b)"
left associative with precedence 55
-for @{ 'ptimesi $a $b }.
+for @{ 'magma_op $a $b }.
-interpretation "Semigroup operation" 'ptimesi a b =
+interpretation "magma operation" 'magma_op a b =
(cic:/matita/algebra/semigroups/op.con _ a b).
-(* too ugly
-interpretation "Semigroup operation" 'ptimes S a b =
- (cic:/matita/algebra/semigroups/op.con S a b). *)
-
-notation < "S"
-for @{ 'carrier $S }.
+(* Semigroups *)
-interpretation "Carrier coercion" 'carrier S =
- (cic:/matita/algebra/semigroups/carrier.con S).
+record isSemiGroup (M:Magma) : Prop ≝
+ { associative: associative ? (op M) }.
+record SemiGroup : Type ≝
+ { magma:> Magma;
+ semigroup_properties:> isSemiGroup magma
+ }.
+
+notation < "S" for @{ 'magma $S }.
+interpretation "magma coercion" 'magma S =
+ (cic:/matita/algebra/semigroups/magma.con S).
+
definition is_left_unit ≝
λS:SemiGroup. λe:S. ∀x:S. e·x = x.
in
C.CoFix (i, fl')
in
- um_aux term
+ LibrarySync.merge_coercions (um_aux term)
;;
let apply_subst =
let newt, _, subst, metasenv, ugraph =
avoid_double_coercion
subst metasenv ugraph
- (Cic.Appl[c;hete]) tgt_carr
- in
- newt, subst, metasenv, ugraph)
+ (Cic.Appl[c;hete]) tgt_carr in
+ try
+ let newty,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety s ugraph
+ in
+ newt, subst, metasenv, ugraph
+ with exn ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*)))) exn)
| exn ->
enrich localization_tbl hete
~f:(fun _ ->
fo_unif_l
test_equality_only subst metasenv (lr1, lr2) ugraph
with
- | UnificationFailure _ as exn ->
+ | UnificationFailure _
+ | Uncertain _ 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 c2 ->
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
- | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u
+ | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
| _ -> assert false
in
let body2, attrs2, ugraph =
with Invalid_argument _ ->
match t with
| Cic.Sort s -> Sort s
+ | Cic.Appl ((Cic.Const (uri, _))::_)
+ | Cic.Appl ((Cic.MutInd (uri, _, _))::_)
+ | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri
| t -> Term t
;;
+let name_of_carr = function
+ | Uri u -> UriManager.name_of_uri u
+ | Sort s -> CicPp.ppsort s
+ | Term (Cic.Appl ((Cic.Const (uri, _))::_))
+ | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_))
+ | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) ->
+ UriManager.name_of_uri uri
+ | Term t -> (* CicPp.ppterm t *) assert false
+
let eq_carr src tgt =
match src, tgt with
| Uri src, Uri tgt -> UriManager.eq src tgt
else raise EqCarrOnNonMetaClosed
| _, _ -> false
-let name_of_carr = function
- | Uri u -> UriManager.name_of_uri u
- | Sort s -> CicPp.ppsort s
- | Term t -> CicPp.ppterm t
-
-
let to_list () =
!db
* *)
let coercion_hashtbl = UriManager.UriHashtbl.create 3
-let merge_coercions obj =
+let rec merge_coercions =
+ let module C = Cic in
+ let aux = (fun (u,t) -> u,merge_coercions t) in
+ function
+ C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
+ | C.Meta (n,subst) ->
+ let subst' =
+ List.map
+ (function None -> None | Some t -> Some (merge_coercions t)) subst
+ in
+ C.Meta (n,subst')
+ | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty)
+ | C.Prod (name,so,dest) ->
+ C.Prod (name, merge_coercions so, merge_coercions dest)
+ | C.Lambda (name,so,dest) ->
+ C.Lambda (name, merge_coercions so, merge_coercions dest)
+ | C.LetIn (name,so,dest) ->
+ C.LetIn (name, merge_coercions so, merge_coercions dest)
+ | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
+ CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CoercGraph.target_of c1 in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
+ | _ -> assert false) (* the composite coercion must exist *)
+ | C.Appl l -> C.Appl (List.map merge_coercions l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Var (uri, exp_named_subst)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Const (uri, exp_named_subst)
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutInd (uri,tyno,exp_named_subst)
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst)
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ let pl = List.map merge_coercions pl in
+ C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl)
+ | C.Fix (fno, fl) ->
+ let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in
+ C.Fix (fno, fl)
+ | C.CoFix (fno, fl) ->
+ let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in
+ C.CoFix (fno, fl)
+
+let merge_coercions_in_obj obj =
let module C = Cic in
- let rec aux2 = (fun (u,t) -> u,aux t)
- and aux = function
- | C.Rel _ | C.Sort _ as t -> t
- | C.Meta _ | C.Implicit _ -> assert false
- | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
- | C.Prod (name,so,dest) ->
- C.Prod (name, aux so, aux dest)
- | C.Lambda (name,so,dest) ->
- C.Lambda (name, aux so, aux dest)
- | C.LetIn (name,so,dest) ->
- C.LetIn (name, aux so, aux dest)
- | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CoercGraph.target_of c1 in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
- | _ -> assert false) (* the composite coercion must exist *)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux2 exp_named_subst in
- C.Var (uri, exp_named_subst)
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux2 exp_named_subst in
- C.Const (uri, exp_named_subst)
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst = List.map aux2 exp_named_subst in
- C.MutInd (uri,tyno,exp_named_subst)
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst = List.map aux2 exp_named_subst in
- C.MutConstruct (uri,tyno,consno,exp_named_subst)
- | C.MutCase (uri,tyno,out,te,pl) ->
- let pl = List.map aux pl in
- C.MutCase (uri,tyno,aux out,aux te,pl)
- | C.Fix (fno, fl) ->
- let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in
- C.Fix (fno, fl)
- | C.CoFix (fno, fl) ->
- let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in
- C.CoFix (fno, fl)
- in
match obj with
| C.Constant (id, body, ty, params, attrs) ->
let body =
match body with
| None -> None
- | Some body -> Some (aux body)
+ | Some body -> Some (merge_coercions body)
in
- let ty = aux ty in
+ let ty = merge_coercions ty in
C.Constant (id, body, ty, params, attrs)
| C.Variable (name, body, ty, params, attrs) ->
let body =
match body with
| None -> None
- | Some body -> Some (aux body)
+ | Some body -> Some (merge_coercions body)
in
- let ty = aux ty in
+ let ty = merge_coercions ty in
C.Variable (name, body, ty, params, attrs)
| C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
assert false
let indtys =
List.map
(fun (name, ind, arity, cl) ->
- let arity = aux arity in
- let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in
+ let arity = merge_coercions arity in
+ let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in
(name, ind, arity, cl))
indtys
in
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
then
- merge_coercions obj
+ merge_coercions_in_obj obj
else
obj
in
exception AlreadyDefined of UriManager.uri
+val merge_coercions: Cic.term -> Cic.term
+
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
projects / helm.git / commitdiff