aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--Makefile.common4
-rw-r--r--tactics/class_tactics.ml415
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1634.v20
-rw-r--r--test-suite/bugs/closed/shouldsucceed/846.v6
-rw-r--r--test-suite/output/ZSyntax.out10
-rw-r--r--test-suite/success/extraction.v4
-rw-r--r--test-suite/success/setoid_test.v4
-rw-r--r--test-suite/success/setoid_test2.v4
-rw-r--r--test-suite/success/setoid_test_function_space.v12
-rw-r--r--theories/Classes/Equivalence.v75
-rw-r--r--theories/Classes/Relations.v11
-rw-r--r--theories/Classes/SetoidAxioms.v35
-rw-r--r--theories/Classes/SetoidDec.v16
-rw-r--r--theories/Classes/SetoidTactics.v77
-rw-r--r--theories/Program/Utils.v10
-rw-r--r--theories/ZArith/Zdiv.v1
-rw-r--r--toplevel/classes.ml3
-rw-r--r--toplevel/record.ml5
-rw-r--r--toplevel/record.mli8
20 files changed, 188 insertions, 135 deletions
diff --git a/CHANGES b/CHANGES
index 3bba84fc7..d1e60f33b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -159,6 +159,9 @@ Program
they can be automatically solved by the default tactic.
- New command "Preterm [ of id ]" to see the actual term fed to Coq for
debugging purposes.
+- Changed the notations "left" and "right" to "in_left" and "in_right" to hide the
+ proofs in standard disjunctions, to avoid breaking existing scripts when importing
+ Program. Also, put them in program_scope.
Miscellaneous
diff --git a/Makefile.common b/Makefile.common
index d4dc8256f..5e35108db 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -748,8 +748,8 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories
UNICODEVO:= theories/Unicode/Utf8.vo
CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
- theories/Classes/Functions.vo theories/Classes/Equivalence.vo \
- theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
+ theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
+ theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo
THEORIESVO:=\
$(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bb73d4094..aa509ba77 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -368,6 +368,7 @@ let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep
let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence")
+let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation")
let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
@@ -858,8 +859,14 @@ let require_library dirpath =
let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
Library.require_library [qualid] (Some false)
+let check_required_library d =
+ let d' = List.map id_of_string d in
+ let dir = make_dirpath (List.rev d') in
+ if not (Library.library_is_opened dir) then
+ error ("Library "^(list_last d)^" has to be required first")
+
let init_setoid () =
- require_library "Coq.Setoids.Setoid"
+ check_required_library ["Coq";"Setoids";"Setoid"]
let declare_instance_refl a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive"
@@ -1029,9 +1036,9 @@ let build_morphism_signature m =
in
let sig_, evars = build_signature isevars env t cstrs snd in
let _ = List.iter
- (fun (ty, relty) ->
- let equiv = mkApp (Lazy.force equivalence, [| ty; relty |]) in
- ignore(Evarutil.e_new_evar isevars env equiv))
+ (fun (ty, rel) ->
+ let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
+ ignore(Evarutil.e_new_evar isevars env default))
evars
in
let morph =
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 9e50f6f25..205e82798 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -3,22 +3,22 @@ Require Export Setoid.
Variable A : Type.
Variable S : A -> Type.
-Variable Seq : forall (a:A), relation (S a).
+Variable Seq : forall {a:A}, relation (S a).
-Hypothesis Seq_refl : forall (a:A) (x : S a), Seq a x x.
-Hypothesis Seq_sym : forall (a:A) (x y : S a), Seq a x y -> Seq a y x.
-Hypothesis Seq_trans : forall (a:A) (x y z : S a), Seq a x y -> Seq a y z ->
-Seq
-a x z.
+Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
+Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
+Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
+Seq x z.
-Add Relation S Seq
+Add Relation (S a) Seq
reflexivity proved by Seq_refl
symmetry proved by Seq_sym
transitivity proved by Seq_trans
as S_Setoid.
-Goal forall (a : A) (x y : S a), Seq a x y -> Seq a x y.
+Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
intros a x y H.
- setoid_replace x with y using relation Seq.
- apply Seq_refl. trivial.
+ setoid_replace x with y.
+ reflexivity.
+ trivial.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225f..95bbab92a 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -138,15 +138,15 @@ Proof.
right; assumption.
intros l _ r.
apply (step (A:=L' A l)).
- exact (inl _ (inl _ r)).
+ exact (inl (inl r)).
intros l _ r1 _ r2.
apply (step (A:=L' A l)).
(* unfold L' in * |- *.
Check 0. *)
- exact (inl _ (inr _ (pair r1 r2))).
+ exact (inl (inr (pair r1 r2))).
intros l _ r.
apply (step (A:=L' A l)).
- exact (inr _ r).
+ exact (inr r).
Defined.
Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index cbfb9f207..a24ad124e 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
: Z
fun f : nat -> Z => (f 0%nat + 0)%Z
: (nat -> Z) -> Z
-fun x : positive => Zpos (xO x)
+fun x : positive => Zpos x~0)
: positive -> Z
fun x : positive => (Zpos x + 1)%Z
: positive -> Z
fun x : positive => Zpos x
: positive -> Z
-fun x : positive => Zneg (xO x)
+fun x : positive => Zneg x~0
: positive -> Z
-fun x : positive => (Zpos (xO x) + 0)%Z
+fun x : positive => (Zpos x~0 + 0)%Z
: positive -> Z
-fun x : positive => (- Zpos (xO x))%Z
+fun x : positive => (- Zpos x~0)%Z
: positive -> Z
-fun x : positive => (- Zpos (xO x) + 0)%Z
+fun x : positive => (- Zpos x~0 + 0)%Z
: positive -> Z
(Z_of_nat 0 + 1)%Z
: Z
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0b3060d51..6a5bf58b6 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -84,7 +84,7 @@ Extraction test12.
(* type test12 = (__ -> __ -> __) -> __ *)
-Definition test13 := match left True I with
+Definition test13 := match @left True True I with
| left x => 1
| right x => 0
end.
@@ -322,7 +322,7 @@ Extraction test24.
Require Import Gt.
Definition loop (Ax:Acc gt 0) :=
(fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
- F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
+ F (S a) (Acc_inv b (gt_Sn_n a))) 0 Ax.
Extraction loop.
(* let loop _ =
let rec f a =
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index e99b3c19b..2be1500f4 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -110,9 +110,9 @@ Definition id: Set -> Set := fun A => A.
Definition rel : forall A : Set, relation (id A) := @eq.
Definition f: forall A : Set, A -> A := fun A x => x.
-Add Relation id rel as eq_rel.
+Instance DefaultRelation (id A) (rel A).
-Add Morphism f with signature rel ++> rel as f_morph.
+Add Morphism (@f A) : f_morph.
Proof.
unfold rel, f. trivial.
Qed.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index bac1cf149..8e5729dce 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,6 +120,8 @@ Axiom eqS1: S1 -> S1 -> Prop.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1 as S1setoid.
+Instance DefaultRelation S1 eqS1.
+
Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'.
@@ -218,6 +220,8 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
+Instance DefaultRelation S1_test8 eqS1_test8.
+
Axiom f_test8 : S2 -> S1_test8.
Add Morphism f_test8 : f_compat_test8. Admitted.
diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index 1602991df..2e9bd60ea 100644
--- a/test-suite/success/setoid_test_function_space.v
+++ b/test-suite/success/setoid_test_function_space.v
@@ -26,14 +26,14 @@ Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
Variable K:(nat -> nat)->Prop.
Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
-Add Relation (fun A B:Type => A -> B) feq
- reflexivity proved by feq_refl
- symmetry proved by feq_sym
- transitivity proved by feq_trans as funsetoid.
+Add Relation (A -> B) (@feq A B)
+ reflexivity proved by (@feq_refl A B)
+ symmetry proved by (@feq_sym A B)
+ transitivity proved by (@feq_trans A B) as funsetoid.
-Add Morphism K with signature feq ==> iff as K_ext1.
+Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1.
intuition. apply (K_ext H0 H).
-intuition. assert (x2 =f x1);auto. apply (K_ext H0 H1).
+intuition. assert (y =f x);auto. apply (K_ext H0 H1).
Qed.
Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index da302ea9d..a19f8da82 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -22,6 +22,7 @@ Require Import Coq.Program.Program.
Require Import Coq.Classes.Init.
Require Export Coq.Classes.Relations.
Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.SetoidTactics.
Set Implicit Arguments.
Unset Strict Implicit.
@@ -47,7 +48,7 @@ Proof. eauto with typeclass_instances. Qed.
Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-
+
Open Local Scope equiv_scope.
(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
@@ -67,66 +68,6 @@ Ltac clsubst_nofail :=
Tactic Notation "clsubst" "*" := clsubst_nofail.
-Ltac setoidreplace H t :=
- let Heq := fresh "Heq" in
- cut(H) ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | unfold equiv ; t ].
-
-Ltac setoidreplacein H H' t :=
- let Heq := fresh "Heq" in
- cut(H) ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | unfold equiv ; t ].
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
- setoidreplace (x === y) idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
- setoidreplacein (x === y) id idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
- setoidreplace (x === y) ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
- setoidreplacein (x === y) id ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
- setoidreplace (rel x y) idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y)
- "using" "relation" constr(rel) "by" tactic(t) :=
- setoidreplace (rel x y) ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
- "using" "relation" constr(rel) :=
- setoidreplacein (rel x y) id idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
- "using" "relation" constr(rel) "by" tactic(t) :=
- setoidreplacein (rel x y) id ltac:t.
-
-
-Ltac red_subst_eq_morphism concl :=
- match concl with
- | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
- | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
- | _ => idtac
- end.
-
-Ltac destruct_morphism :=
- match goal with
- | [ |- @Morphism ?A ?R ?m ] => constructor
- end.
-
-Ltac reverse_arrows x :=
- match x with
- | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
- | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
- | _ => idtac
- end.
-
-Ltac add_morphism_tactic := (try destruct_morphism) ;
- match goal with
- | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
- end.
-
Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
Proof with auto.
intros; intro.
@@ -196,21 +137,17 @@ Program Instance iff_impl_id_morphism :
Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
pequiv_prf :> PER carrier pequiv.
+Definition pequiv [ PartialEquivalence A R ] : relation A := R.
+
(** Overloaded notation for partial equiv equivalence. *)
-(* Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. *)
+Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
(** Reset the default Program tactic. *)
Ltac obligations_tactic ::= program_simpl.
-(** Default relation on a given support. *)
-
-Class DefaultRelation A := default_relation : relation A.
-
(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
Instance [ ! Equivalence A R ] =>
- equivalence_default : DefaultRelation A | 4 :=
- default_relation := R.
-
+ equivalence_default : DefaultRelation A R | 4.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index b14647d06..530f21264 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -24,6 +24,17 @@ Unset Strict Implicit.
Notation "'relation' A " := (A -> A -> Prop) (at level 0).
+(** Default relation on a given support. *)
+
+Class DefaultRelation A (R : relation A).
+
+(** To search for the default relation, just call [default_relation]. *)
+
+Definition default_relation [ DefaultRelation A R ] : relation A := R.
+
+(** A notation for applying the default relation to [x] and [y]. *)
+Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
+
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.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
new file mode 100644
index 000000000..6b7881c9f
--- /dev/null
+++ b/theories/Classes/SetoidAxioms.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Extensionality axioms that can be used when reasoning with setoids.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ * 91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.SetoidClass.
+
+(* Application of the extensionality axiom to turn a goal on leibinz equality to
+ a setoid equivalence. *)
+
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+
+(** Application of the extensionality principle for setoids. *)
+
+Ltac setoid_extensionality :=
+ match goal with
+ [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
+ end. \ No newline at end of file
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8a435b449..86a2bef80 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,6 +50,8 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
Require Import Coq.Program.Program.
+Open Local Scope program_scope.
+
(** Invert the branches. *)
Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
@@ -87,7 +89,7 @@ Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
equiv_dec := bool_dec.
Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
- equiv_dec x y := left.
+ equiv_dec x y := in_left.
Next Obligation.
Proof.
@@ -101,9 +103,9 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
dest x as (x1, x2) in
dest y as (y1, y2) in
if x1 == y1 then
- if x2 == y2 then left
- else right
- else right.
+ if x2 == y2 then in_left
+ else in_right
+ else in_right.
Solve Obligations using unfold complement ; program_simpl.
@@ -114,9 +116,9 @@ Require Import Coq.Program.FunctionalExtensionality.
Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
equiv_dec f g :=
if f true == g true then
- if f false == g false then left
- else right
- else right.
+ if f false == g false then in_left
+ else in_right
+ else in_right.
Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 1277dcda9..c71db6995 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,21 +15,80 @@
(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
-Require Import Coq.Program.Program.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
-Require Export Coq.Classes.SetoidClass.
+(** The setoid_replace tactics in Ltac, defined in terms of default relations [===def] and
+ the setoid_rewrite tactic. *)
-(* Application of the extensionality axiom to turn a goal on leibinz equality to
- a setoid equivalence. *)
+Ltac setoidreplace H t :=
+ let Heq := fresh "Heq" in
+ cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | t ].
-Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+Ltac setoidreplacein H H' t :=
+ let Heq := fresh "Heq" in
+ cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
-(** Application of the extensionality principle for setoids. *)
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+ setoidreplace (x ===def y) idtac.
-Ltac setoid_extensionality :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
+ setoidreplacein (x ===def y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
+ setoidreplace (x ===def y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
+ setoidreplacein (x ===def y) id ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
+ setoidreplace (rel x y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+ "using" "relation" constr(rel) "by" tactic(t) :=
+ setoidreplace (rel x y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
+ "using" "relation" constr(rel) :=
+ setoidreplacein (rel x y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
+ "using" "relation" constr(rel) "by" tactic(t) :=
+ setoidreplacein (rel x y) id ltac:t.
+
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
+ to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
+ and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+
+Require Import Coq.Program.Tactics.
+
+Ltac red_subst_eq_morphism concl :=
+ match concl with
+ | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+ | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+ | _ => idtac
+ end.
+
+Ltac destruct_morphism :=
match goal with
- [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
- end. \ No newline at end of file
+ | [ |- @Morphism ?A ?R ?m ] => constructor
+ end.
+
+Ltac reverse_arrows x :=
+ match x with
+ | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+ | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+ | _ => idtac
+ end.
+
+Ltac default_add_morphism_tactic :=
+ (try destruct_morphism) ;
+ match goal with
+ | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
+ end.
+
+Ltac add_morphism_tactic := default_add_morphism_tactic.
+
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c514d3234..184e3c367 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -61,16 +61,10 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0).
(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
-
-(** These type arguments should be infered from the context. *)
-
-Implicit Arguments left [[A]].
-Implicit Arguments right [[B]].
-
(** Hide proofs and generates obligations when put in a term. *)
-Notation left := (left _ _).
-Notation right := (right _ _).
+Notation "'in_left'" := (@left _ _ _) : program_scope.
+Notation "'in_right'" := (@right _ _ _) : program_scope.
(** Extraction directives *)
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index ff8033eeb..6bcbbf6b7 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,6 +21,7 @@ Require Import Zbool.
Require Import Omega.
Require Import ZArithRing.
Require Import Zcomplements.
+Require Export Setoid.
Open Local Scope Z_scope.
(** * Definitions of Euclidian operations *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 32803742a..4af59ff62 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -185,7 +185,8 @@ let declare_structure env id idbuild params arity fields =
mind_entry_inds = [mie_ind] } in
let kn = Command.declare_mutual_with_eliminations true mie in
let rsp = (kn,0) in (* This is ind path of idstruc *)
- let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in
+ let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
+ let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
let _build = ConstructRef (rsp,1) in
Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
rsp
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b94dffe1a..b04557304 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,15 +131,14 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
-let declare_projections indsp coers fields =
+let declare_projections indsp ?name coers fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
let r = mkInd indsp in
let rp = applist (r, extended_rel_list 0 paramdecls) in
let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
- let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in
- (* Termops.named_hd (Global.env()) r Anonymous *)
+ let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in
let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
let lifted_fields = lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
diff --git a/toplevel/record.mli b/toplevel/record.mli
index e322dcfd0..5ba8b04e1 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -16,12 +16,12 @@ open Vernacexpr
open Topconstr
(*i*)
-(* [declare_projections ref coers params fields] declare projections of
- record [ref] (if allowed), and put them as coercions accordingly to
- [coers]; it returns the absolute names of projections *)
+(* [declare_projections ref name coers params fields] declare projections of
+ record [ref] (if allowed) using the given [name] as argument, and put them
+ as coercions accordingly to [coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> bool list -> rel_context -> bool list * constant option list
+ inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
val definition_structure :
lident with_coercion * local_binder list *
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 19:25:50 +0000