aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-ext.tex2
-rw-r--r--tactics/class_setoid.ml423
-rw-r--r--tactics/eauto.ml437
-rw-r--r--tactics/eauto.mli3
-rw-r--r--theories/Classes/Morphisms.v59
-rw-r--r--theories/Classes/Relations.v43
-rw-r--r--theories/Classes/SetoidClass.v14
-rw-r--r--toplevel/classes.ml3
8 files changed, 84 insertions, 100 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 3a834ff8a..5dc06f33c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1192,8 +1192,6 @@ Check (fun l:list (list nat) => map length l).
\Rem To know which are the implicit arguments of an object, use the command
{\tt Print Implicit} (see \ref{PrintImplicit}).
-\Rem
-
\Rem If the list of arguments is empty, the command removes the
implicit arguments of {\qualid}.
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 84c1937ea..9aa445187 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -74,7 +74,8 @@ let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation")
+(* let coq_relation = lazy (gen_constant ["Classes";"Relations"] "relation") *)
+let coq_relation a = mkProd (Anonymous, a, mkProd (Anonymous, a, mkProp))
let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
@@ -112,7 +113,7 @@ let build_signature isevars env m cstrs finalcstr =
(* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
in
let mk_relty ty obj =
- let relty = mkApp (Lazy.force coq_relation, [| ty |]) in
+ let relty = coq_relation ty in
match obj with
| None -> new_evar isevars env relty
| Some (p, (a, r, oldt, newt)) -> r
@@ -256,17 +257,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
let relargs, args = array_chop (Array.length args - 2) args in
let rel = mkApp (r, relargs) in
let typ = pf_type_of gl rel in
- (match kind_of_term typ with
- | App (relation, [| carrier |]) when eq_constr relation (Lazy.force coq_relation)
- || eq_constr relation (Lazy.force coq_relationT) ->
- (c, (carrier, rel, args.(0), args.(1)))
- | _ when isArity typ ->
- let (ctx, ar) = destArity typ in
- (match ctx with
- [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy ->
- (c, (sx, rel, args.(0), args.(1)))
- | _ -> error "Only binary relations are supported")
- | _ -> error "Not a relation")
+ (if isArity typ then
+ let (ctx, ar) = destArity typ in
+ (match ctx with
+ [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy ->
+ (c, (sx, rel, args.(0), args.(1)))
+ | _ -> error "Only binary relations are supported")
+ else error "Not a relation")
| _ -> error "Not a relation"
in
if left2right then res
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 70ec9d046..da477f2a3 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -241,15 +241,19 @@ module SearchProblem = struct
let success s = (sig_it (fst s.tacres)) = []
- let rec filter_tactics (glls,v) = function
- | [] -> []
- | (tac,pptac) :: tacl ->
- try
- let (lgls,ptl) = apply_tac_list tac glls in
- let v' p = v (ptl p) in
- ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
- with e when Logic.catchable_exception e ->
- filter_tactics (glls,v) tacl
+ let filter_tactics (glls,v) l =
+(* let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+ let rec aux = function
+ | [] -> []
+ | (tac,pptac) :: tacl ->
+ try
+ let (lgls,ptl) = apply_tac_list tac glls in
+ let v' p = v (ptl p) in
+(* msg (hov 0 (pptac ++ str"\n")); *)
+ ((lgls,v'),pptac) :: aux tacl
+ with e when Logic.catchable_exception e ->
+ aux tacl
+ in aux l
(* Ordering of states is lexicographic on depth (greatest first) then
number of remaining goals. *)
@@ -498,7 +502,7 @@ let valid evm p res_sigma l =
!res_sigma (l, Evd.create_evar_defs !res_sigma)
in raise (Found (snd evd'))
-let resolve_all_evars debug (mode, depth) env p evd =
+let resolve_all_evars_once debug (mode, depth) env p evd =
let evm = Evd.evars_of evd in
let goals =
Evd.fold
@@ -513,3 +517,16 @@ let resolve_all_evars debug (mode, depth) env p evd =
let gls', valid' = full_eauto_gls debug (mode, depth) [] (gls, valid evm p res_sigma) in
res_sigma := Evarutil.nf_evars (sig_sig gls');
try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd'
+
+let has_undefined p evd =
+ Evd.fold (fun ev evi has -> has ||
+ (evi.evar_body = Evar_empty && p ev evi))
+ (Evd.evars_of evd) false
+
+let rec resolve_all_evars debug m env p evd =
+ let rec aux n evd =
+ if has_undefined p evd && n > 0 then
+ let evd' = resolve_all_evars_once debug m env p evd in
+ aux (pred n) evd'
+ else evd
+ in aux 3 evd
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 940648c2e..a1ff89905 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -61,6 +61,9 @@ end
val full_eauto_gls : bool -> bool * int -> constr list -> goal list sigma * validation ->
goal list sigma * validation
+val resolve_all_evars_once : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
+ evar_defs
+
val resolve_all_evars : bool -> bool * int -> env -> (evar -> evar_info -> bool) -> evar_defs ->
evar_defs
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 09a58fa01..72db276e4 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -29,23 +29,16 @@ Unset Strict Implicit.
(** Respectful morphisms. *)
-Definition respectful_depT (A : Type) (R : relationT A)
- (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) :=
+Definition respectful_dep (A : Type) (R : relation A)
+ (B : A -> Type) (R' : forall x y, B x -> B y -> Prop) : relation (forall x : A, B x) :=
fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
-Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
- Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
-
Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
fun f g => forall x y : A, R x y -> R' (f x) (g y).
-(** Notations reminiscent of the old syntax for declaring morphisms.
- We use three + or - for type morphisms, and two for [Prop] ones.
- *)
-
-Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
-Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20).
Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
@@ -53,7 +46,7 @@ Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity,
The relation [R] will be instantiated by [respectful] and [A] by an arrow type
for usual morphisms. *)
-Class Morphism A (R : relationT A) (m : A) :=
+Class Morphism A (R : relation A) (m : A) :=
respect : R m m.
(** Here we build an equivalence instance for functions which relates respectful ones only. *)
@@ -63,7 +56,7 @@ Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : rela
Ltac obligations_tactic ::= program_simpl.
-Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] =>
+Program Instance [ Equivalence A R, Equivalence B R' ] =>
respecting_equiv : Equivalence respecting
(fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
@@ -93,12 +86,6 @@ Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation
Ltac obligations_tactic ::= program_simpl ; simpl_relation.
-Program Instance notT_arrow_morphism :
- Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
-
-Program Instance not_iso_morphism :
- Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
-
Program Instance not_impl_morphism :
Morphism (Prop -> Prop) (impl --> impl) not.
@@ -134,7 +121,7 @@ Program Instance `A` (R : relation A) `B` (R' : relation B)
destruct respect with x y x0 y0 ; auto.
Qed.
-Program Instance `A` (R : relation A) `B` (R' : relation B)
+Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
[ ? Morphism (R ++> R' ++> iff) m ] =>
iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
@@ -171,7 +158,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
(* fun x y => R x y -> R' (f x) (f y). *)
-(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *)
+(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *)
(* [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
(* intros. *)
(* destruct H. *)
@@ -182,7 +169,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
(* Existing Instance morphism_respectful'. *)
-(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A) *)
+(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A) *)
(* [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
(* intros. *)
(* cut (relation A) ; intros R'. *)
@@ -210,7 +197,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
(** A proof of [R x x] is available. *)
-(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *)
+(* Program Instance (A : Type) R B (R' : relation B) *)
(* [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
(* morphism_partial_app_morphism : ? Morphism R' (m x). *)
@@ -223,7 +210,7 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
(** Morpshism declarations for partial applications. *)
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
Next Obligation.
@@ -231,7 +218,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
trans y...
Qed.
-Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
Next Obligation.
@@ -239,7 +226,7 @@ Program Instance [ Transitive A (R : relation A) ] (x : A) =>
trans x0...
Qed.
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
Next Obligation.
@@ -248,7 +235,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
sym...
Qed.
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
Next Obligation.
@@ -257,7 +244,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
sym...
Qed.
-Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
+Program Instance [ Equivalence A R ] (x : A) =>
equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
Next Obligation.
@@ -270,7 +257,7 @@ Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
(** With symmetric relations, variance is no issue ! *)
-Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B)
+Program Instance [ Symmetric A R ] B (R' : relation B)
[ Morphism _ (R ++> R') m ] =>
sym_contra_morphism : ? Morphism (R --> R') m.
@@ -282,7 +269,7 @@ Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B)
(** [R] is reflexive, hence we can build the needed proof. *)
-Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
+Program Instance [ Reflexive A R ] B (R' : relation B)
[ ? Morphism (R ++> R') m ] (x : A) =>
reflexive_partial_app_morphism : ? Morphism R' (m x).
@@ -295,7 +282,7 @@ Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
+Program Instance [ Transitive A R, Symmetric A R ] =>
trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
Next Obligation.
@@ -306,7 +293,7 @@ Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
trans y... trans y0... sym...
Qed.
-Program Instance [ Equivalence A (R : relation A) ] =>
+Program Instance [ Equivalence A R ] =>
equiv_morphism : ? Morphism (R ++> R ++> iff) R.
Next Obligation.
@@ -335,16 +322,16 @@ Program Instance inverse_iff_impl_id :
(** Logical conjunction. *)
-(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *)
+Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
-(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *)
+Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
(** Logical disjunction. *)
-(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *)
+Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
-(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *)
+Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index aaeb18654..9cc78a970 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -22,41 +22,35 @@ Require Import Coq.Classes.Init.
Set Implicit Arguments.
Unset Strict Implicit.
-Definition relationT A := A -> A -> Type.
-Definition relation A := A -> A -> Prop.
+Notation "'relation' A " := (A -> A -> Prop) (at level 0).
Definition inverse A (R : relation A) : relation A := fun x y => R y x.
Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
-Definition complementT A (R : relationT A) := fun x y => notT (R x y).
-
Definition complement A (R : relation A) := fun x y => R x y -> False.
(** These are convertible. *)
-Lemma complementT_flip : forall A (R : relationT A), complementT (flip R) = flip (complementT R).
-Proof. reflexivity. Qed.
-
Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
Proof. reflexivity. Qed.
(** We rebind relations in separate classes to be able to overload each proof. *)
-Class Reflexive A (R : relationT A) :=
+Class Reflexive A (R : relation A) :=
reflexive : forall x, R x x.
-Class Irreflexive A (R : relationT A) :=
+Class Irreflexive A (R : relation A) :=
irreflexive : forall x, R x x -> False.
-Class Symmetric A (R : relationT A) :=
+Class Symmetric A (R : relation A) :=
symmetric : forall x y, R x y -> R y x.
-Class Asymmetric A (R : relationT A) :=
+Class Asymmetric A (R : relation A) :=
asymmetric : forall x y, R x y -> R y x -> False.
-Class Transitive A (R : relationT A) :=
+Class Transitive A (R : relation A) :=
transitive : forall x y z, R x y -> R y z -> R x z.
Implicit Arguments Reflexive [A].
@@ -141,23 +135,6 @@ Ltac simpl_relation :=
Ltac obligations_tactic ::= simpl_relation.
-(** The arrow is a reflexive and transitive relation on types. *)
-
-Program Instance arrow_refl : ? Reflexive arrow :=
- reflexive X := id.
-
-Program Instance arrow_trans : ? Transitive arrow :=
- transitive X Y Z f g := g o f.
-
-(** Isomorphism. *)
-
-Definition iso (A B : Type) :=
- A -> B * B -> A.
-
-Program Instance iso_refl : ? Reflexive iso.
-Program Instance iso_sym : ? Symmetric iso.
-Program Instance iso_trans : ? Transitive iso.
-
(** Logical implication. *)
Program Instance impl_refl : ? Reflexive impl.
@@ -180,7 +157,7 @@ Program Instance eq_trans : ? Transitive (@eq A).
- a tactic to immediately solve a goal without user intervention
- a tactic taking input from the user to make progress on a goal *)
-Definition relate A (R : relationT A) : relationT A := R.
+Definition relate A (R : relation A) : relation A := R.
Ltac relationify_relation R R' :=
match goal with
@@ -287,7 +264,7 @@ Ltac relation_tac := relation_refl || relation_sym || relation_trans.
(** The [PER] typeclass. *)
-Class PER (carrier : Type) (pequiv : relationT carrier) :=
+Class PER (carrier : Type) (pequiv : relation carrier) :=
per_sym :> Symmetric pequiv ;
per_trans :> Transitive pequiv.
@@ -307,14 +284,14 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
(** The [Equivalence] typeclass. *)
-Class Equivalence (carrier : Type) (equiv : relationT carrier) :=
+Class Equivalence (carrier : Type) (equiv : relation carrier) :=
equiv_refl :> Reflexive equiv ;
equiv_sym :> Symmetric equiv ;
equiv_trans :> Transitive equiv.
(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
-Class [ Equivalence A eqA ] => Antisymmetric (R : relationT A) :=
+Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) :=
antisymmetric : forall x y, R x y -> R y x -> eqA x y.
Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] =>
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5e18ef2af..8c8c8c67c 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -31,9 +31,10 @@ Class Setoid A :=
equiv : relation A ;
setoid_equiv :> Equivalence A equiv.
-Program Instance [ eqa : Equivalence A (eqA : relation A) ] =>
- equivalence_setoid : Setoid A :=
- equiv := eqA ; setoid_equiv := eqa.
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] => *)
+(* equivalence_setoid : Setoid A := *)
+(* equiv := eqA ; setoid_equiv := eqa. *)
(** Shortcuts to make proof search easier. *)
@@ -46,6 +47,10 @@ Proof. eauto with typeclass_instances. Qed.
Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
Proof. eauto with typeclass_instances. Qed.
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
(** Standard setoids. *)
(* Program Instance eq_setoid : Setoid A := *)
@@ -142,11 +147,10 @@ Ltac obligations_tactic ::= morphism_tac.
Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
-Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
(* (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
-
(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
(* [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] => *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 959dc1040..1d5280a49 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,7 +34,8 @@ open Entries
let hint_db = "typeclass_instances"
let add_instance_hint inst =
- Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))])
+ Auto.add_hints false [hint_db]
+ (Vernacexpr.HintsResolve [CAppExpl (dummy_loc, (None, Ident (dummy_loc, inst)), [])])
let declare_instance (_,id) =
add_instance_hint id
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-25 01:35:56 +0000