coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>
- To: anoun AT labri.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] problem setoid
- Date: Wed, 16 Feb 2005 15:16:58 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear Houda,
yesterday I wrote:
> I am investigating whether these issues can be solved, but this will
> require a bit of time.
I have patched the implementation of the tactic so that it works now on
your example (not finished yet: I still have to port a few proofs in
Setoid.v to the new names generated by Coq due to the sort change :-(.
In attachment you can find your example and two files that
you have to substitute for the original ones before recompiling Coq.
However, these modifications have a few drawbacks:
1. several Props replaced by Type here and there ==> it is quite easy
to fall into an "universe inconsistency" using the tactic since Coq
lacks universe polymnorphism
2. less reusal of standard notions. For instance, a relation has no
longer type Relation_Definitions.relation (= forall A, A -> A ->
Prop); it has the ad-hoc type "forall A, A -> A -> Type"
I do not know how to avoid these drawbacks, but I consider them very
annoying.
Moreover, before committing (if I decide to do so) I have to finish porting
the proof and I prefer to clean up the code a bit and perform some regression
tests. Since I am a bit busy right now, I will probably commit not before
next week.
In the meantime, can you test my patch and see if it works for you?
Regards,
C.S.C.
--
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail:
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: Setoid.v,v 1.18 2004/11/16 16:11:10 sacerdot Exp $: i*)
Definition relationT (A: Type) := A -> A -> Type.
Definition reflexiveT (A: Type) (R: relationT A) := forall x, R x x.
Definition symmetricT (A: Type) (R: relationT A) := forall x y, R x y -> R y
x.
Definition transitiveT (A: Type) (R: relationT A) :=
forall x y z, R x y -> R y z -> R x z.
Set Implicit Arguments.
(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
(* X will be used to distinguish covariant arguments whose type is an *)
(* Asymmetric* relation from contravariant arguments of the same type *)
Inductive X_Relation_Class (X: Type) : Type :=
SymmetricReflexive :
forall A Aeq, symmetricT A Aeq -> reflexiveT _ Aeq -> X_Relation_Class X
| AsymmetricReflexive : X -> forall A Aeq, reflexiveT A Aeq ->
X_Relation_Class X
| SymmetricAreflexive : forall A Aeq, symmetricT A Aeq -> X_Relation_Class X
| AsymmetricAreflexive : X -> forall A (Aeq : relationT A), X_Relation_Class
X
| Leibniz : Type -> X_Relation_Class X.
Inductive variance : Set :=
Covariant
| Contravariant.
Definition Argument_Class := X_Relation_Class variance.
Definition Relation_Class := X_Relation_Class unit.
Inductive Reflexive_Relation_Class : Type :=
RSymmetric :
forall A Aeq, symmetricT A Aeq -> reflexiveT _ Aeq ->
Reflexive_Relation_Class
| RAsymmetric :
forall A Aeq, reflexiveT A Aeq -> Reflexive_Relation_Class
| RLeibniz : Type -> Reflexive_Relation_Class.
Inductive Areflexive_Relation_Class : Type :=
| ASymmetric : forall A Aeq, symmetricT A Aeq -> Areflexive_Relation_Class
| AAsymmetric : forall A (Aeq : relationT A), Areflexive_Relation_Class.
Implicit Type Hole Out: Relation_Class.
Definition relation_class_of_argument_class : Argument_Class ->
Relation_Class.
destruct 1.
exact (SymmetricReflexive _ s r).
exact (AsymmetricReflexive tt r).
exact (SymmetricAreflexive _ s).
exact (AsymmetricAreflexive tt Aeq).
exact (Leibniz _ T).
Defined.
Definition carrier_of_relation_class : forall X, X_Relation_Class X -> Type.
destruct 1.
exact A.
exact A.
exact A.
exact A.
exact T.
Defined.
Definition relation_of_relation_class :
forall X R, @carrier_of_relation_class X R -> carrier_of_relation_class R ->
Type.
destruct R.
exact Aeq.
exact Aeq.
exact Aeq.
exact Aeq.
exact (@eq T).
Defined.
Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
forall R,
carrier_of_relation_class (relation_class_of_argument_class R) =
carrier_of_relation_class R.
destruct R; reflexivity.
Defined.
Inductive nelistT (A : Type) : Type :=
singl : A -> nelistT A
| cons : A -> nelistT A -> nelistT A.
Definition Arguments := nelistT Argument_Class.
Implicit Type In: Arguments.
Definition function_type_of_morphism_signature :
Arguments -> Relation_Class -> Type.
intros In Out.
induction In.
exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
exact (carrier_of_relation_class a -> IHIn).
Defined.
Definition make_compatibility_goal_aux:
forall In Out
(f g: function_type_of_morphism_signature In Out), Type.
intros; induction In; simpl in f, g.
induction a; simpl in f, g.
exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1)
(g x2)).
destruct x.
exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f
x1) (g x2)).
exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f
x1) (g x2)).
exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f x1)
(g x2)).
destruct x.
exact (forall x1 x2, Aeq x1 x2 -> relation_of_relation_class Out (f
x1) (g x2)).
exact (forall x1 x2, Aeq x2 x1 -> relation_of_relation_class Out (f
x1) (g x2)).
exact (forall x, relation_of_relation_class Out (f x) (g x)).
induction a; simpl in f, g.
exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
destruct x.
exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
destruct x.
exact (forall x1 x2, Aeq x1 x2 -> IHIn (f x1) (g x2)).
exact (forall x1 x2, Aeq x2 x1 -> IHIn (f x1) (g x2)).
exact (forall x, IHIn (f x) (g x)).
Defined.
Definition make_compatibility_goal :=
(fun In Out f => make_compatibility_goal_aux In Out f f).
Record Morphism_Theory In Out : Type :=
{Function : function_type_of_morphism_signature In Out;
Compat : make_compatibility_goal In Out Function}.
Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
induction 1.
exact (singl (Leibniz _ a)).
exact (cons (Leibniz _ a) IHX).
Defined.
(* every function is a morphism from Leibniz+ to Leibniz *)
Definition morphism_theory_of_function :
forall (In: nelistT Type) (Out: Type),
let In' := list_of_Leibniz_of_list_of_types In in
let Out' := Leibniz _ Out in
function_type_of_morphism_signature In' Out' ->
Morphism_Theory In' Out'.
intros.
exists X.
induction In; unfold make_compatibility_goal; simpl.
reflexivity.
intro; apply (IHIn (X x)).
Defined.
(* THE iffT RELATION CLASS *)
Inductive prodT' (A : Type) (B : Type) : Type := pairT' : A -> B -> prodT' A
B.
Definition proj1T' (A B: Type) (c: prodT' A B) :=
let (p1,_) := c in p1.
Definition proj2T' (A B: Type) (c: prodT' A B) :=
let (_,p2) := c in p2.
Definition iffT (A B: Type):= prodT' (A -> B) (B -> A).
Lemma iffT_refl: forall A, iffT A A.
split; auto.
Qed.
Lemma iffT_sym: forall A B, iffT A B -> iffT B A.
intros; destruct X; split; auto.
Qed.
Lemma iffT_trans: forall A B C, iffT A B -> iffT B C -> iffT A C.
intros; destruct X; destruct X0; split; auto.
Qed.
Definition IffT_Relation_Class : Relation_Class.
eapply (@SymmetricReflexive unit _ iffT).
exact iffT_sym.
exact iffT_refl.
Defined.
(* THE implT RELATION CLASS *)
Definition implT (A B: Type) := A -> B.
Theorem implT_refl: reflexiveT _ implT.
hnf; unfold implT; tauto.
Qed.
Definition Impl_Relation_Class : Relation_Class.
eapply (@AsymmetricReflexive unit tt _ implT).
exact implT_refl.
Defined.
(* UTILITY FUNCTIONS TO PROVE THAT EVERY TRANSITIVE RELATION IS A MORPHISM *)
Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
forall (A: Type)(Aeq: relationT A)(sym: symmetricT _ Aeq)(trans: transitiveT
_ Aeq),
let ASetoidClass := SymmetricAreflexive _ sym in
(Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
IffT_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; split; eauto.
Defined.
Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
forall (A: Type)(Aeq: relationT A)(refl: reflexiveT _ Aeq)(sym: symmetricT _
Aeq)
(trans: transitiveT _ Aeq), let ASetoidClass := SymmetricReflexive _ sym
refl in
(Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
IffT_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; split; eauto.
Defined.
Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
forall (A: Type)(Aeq: relationT A)(trans: transitiveT _ Aeq),
let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
(Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2))
Impl_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; unfold implT; eauto.
Defined.
Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
forall (A: Type)(Aeq: relationT A)(refl: reflexiveT _ Aeq)(trans:
transitiveT _ Aeq),
let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
let ASetoidClass2 := AsymmetricReflexive Covariant refl in
(Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2))
Impl_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; unfold implT; eauto.
Defined.
(* iff AS A RELATION *)
Add Relation Type iffT
reflexivity proved by iffT_refl
symmetry proved by iffT_sym
transitivity proved by iffT_trans
as iffT_relation.
Add Relation Prop iff
reflexivity proved by iff_refl
symmetry proved by iff_sym
transitivity proved by iff_trans
as iff_relation.
Definition Iff_Relation_Class : Relation_Class.
eapply (@SymmetricReflexive unit _ iff).
exact iff_sym.
exact iff_refl.
Defined.
(* every predicate is morphism from Leibniz+ to Iff_Relation_Class *)
Definition morphism_theory_of_predicate :
forall (In: nelistT Type),
let In' := list_of_Leibniz_of_list_of_types In in
function_type_of_morphism_signature In' Iff_Relation_Class ->
Morphism_Theory In' Iff_Relation_Class.
intros.
exists X.
induction In; unfold make_compatibility_goal; simpl.
intro; apply iff_refl.
intro; apply (IHIn (X x)).
Defined.
(* every predicate is morphism from Leibniz+ to IffT_Relation_Class *)
Definition morphism_theory_of_predicateT :
forall (In: nelistT Type),
let In' := list_of_Leibniz_of_list_of_types In in
function_type_of_morphism_signature In' IffT_Relation_Class ->
Morphism_Theory In' IffT_Relation_Class.
intros.
exists X.
induction In; unfold make_compatibility_goal; simpl.
intro; apply iffT_refl.
intro; apply (IHIn (X x)).
Defined.
(* impl and implT AS RELATIONS *)
Definition impl (A B: Prop) := A -> B.
Theorem impl_refl: reflexiveT _ impl.
hnf; unfold impl; tauto.
Qed.
Theorem impl_trans: transitiveT _ impl.
hnf; unfold impl; tauto.
Qed.
Theorem implT_trans: transitiveT _ implT.
hnf; unfold implT; tauto.
Qed.
Add Relation Type implT
reflexivity proved by implT_refl
transitivity proved by implT_trans
as implT_relation.
Add Relation Prop impl
reflexivity proved by impl_refl
transitivity proved by impl_trans
as impl_relation.
(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
Inductive rewrite_direction : Type :=
Left2Right
| Right2Left.
Implicit Type dir: rewrite_direction.
Definition variance_of_argument_class : Argument_Class -> option variance.
destruct 1.
exact None.
exact (Some v).
exact None.
exact (Some v).
exact None.
Defined.
Definition opposite_direction :=
fun dir =>
match dir with
Left2Right => Right2Left
| Right2Left => Left2Right
end.
Lemma opposite_direction_idempotent:
forall dir, (opposite_direction (opposite_direction dir)) = dir.
destruct dir; reflexivity.
Qed.
Inductive check_if_variance_is_respected :
option variance -> rewrite_direction -> rewrite_direction -> Type
:=
MSNone : forall dir dir', check_if_variance_is_respected None dir dir'
| MSCovariant : forall dir, check_if_variance_is_respected (Some Covariant)
dir dir
| MSContravariant :
forall dir,
check_if_variance_is_respected (Some Contravariant) dir
(opposite_direction dir).
Definition relation_class_of_reflexive_relation_class:
Reflexive_Relation_Class -> Relation_Class.
induction 1.
exact (SymmetricReflexive _ s r).
exact (AsymmetricReflexive tt r).
exact (Leibniz _ T).
Defined.
Definition relation_class_of_areflexive_relation_class:
Areflexive_Relation_Class -> Relation_Class.
induction 1.
exact (SymmetricAreflexive _ s).
exact (AsymmetricAreflexive tt Aeq).
Defined.
Definition carrier_of_reflexive_relation_class :=
fun R => carrier_of_relation_class
(relation_class_of_reflexive_relation_class R).
Definition carrier_of_areflexive_relation_class :=
fun R => carrier_of_relation_class
(relation_class_of_areflexive_relation_class R).
Definition relation_of_areflexive_relation_class :=
fun R => relation_of_relation_class
(relation_class_of_areflexive_relation_class R).
Inductive Morphism_Context Hole dir : Relation_Class -> rewrite_direction ->
Type :=
App :
forall In Out dir',
Morphism_Theory In Out -> Morphism_Context_List Hole dir dir' In ->
Morphism_Context Hole dir Out dir'
| ToReplace : Morphism_Context Hole dir Hole dir
| ToKeep :
forall S dir',
carrier_of_reflexive_relation_class S ->
Morphism_Context Hole dir (relation_class_of_reflexive_relation_class
S) dir'
| ProperElementToKeep :
forall S dir' (x: carrier_of_areflexive_relation_class S),
relation_of_areflexive_relation_class S x x ->
Morphism_Context Hole dir
(relation_class_of_areflexive_relation_class S) dir'
with Morphism_Context_List Hole dir :
rewrite_direction -> Arguments -> Type
:=
fcl_singl :
forall S dir' dir'',
check_if_variance_is_respected (variance_of_argument_class S) dir'
dir'' ->
Morphism_Context Hole dir (relation_class_of_argument_class S) dir' ->
Morphism_Context_List Hole dir dir'' (singl S)
| fcl_cons :
forall S L dir' dir'',
check_if_variance_is_respected (variance_of_argument_class S) dir'
dir'' ->
Morphism_Context Hole dir (relation_class_of_argument_class S) dir' ->
Morphism_Context_List Hole dir dir'' L ->
Morphism_Context_List Hole dir dir'' (cons S L).
Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type
with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort
Type.
Definition product_of_arguments : Arguments -> Type.
induction 1.
exact (carrier_of_relation_class a).
exact (prodT (carrier_of_relation_class a) IHX).
Defined.
Definition get_rewrite_direction: rewrite_direction -> Argument_Class ->
rewrite_direction.
intros dir R.
destruct (variance_of_argument_class R).
destruct v.
exact dir. (* covariant *)
exact (opposite_direction dir). (* contravariant *)
exact dir. (* symmetric relation *)
Defined.
Definition directed_relation_of_relation_class:
forall dir (R: Relation_Class),
carrier_of_relation_class R -> carrier_of_relation_class R -> Type.
destruct 1.
exact (@relation_of_relation_class unit).
intros; exact (relation_of_relation_class _ X0 X).
Defined.
Definition directed_relation_of_argument_class:
forall dir (R: Argument_Class),
carrier_of_relation_class R -> carrier_of_relation_class R -> Type.
intros dir R.
rewrite <-
(about_carrier_of_relation_class_and_relation_class_of_argument_class R).
exact (directed_relation_of_relation_class dir
(relation_class_of_argument_class R)).
Defined.
Definition relation_of_product_of_arguments:
forall dir In,
product_of_arguments In -> product_of_arguments In -> Type.
induction In.
simpl.
exact (directed_relation_of_argument_class (get_rewrite_direction dir a)
a).
simpl; intros.
destruct X; destruct X0.
apply prodT.
exact
(directed_relation_of_argument_class (get_rewrite_direction dir a) a c
c0).
exact (IHIn p p0).
Defined.
Definition apply_morphism:
forall In Out (m: function_type_of_morphism_signature In Out)
(args: product_of_arguments In), carrier_of_relation_class Out.
intros.
induction In.
exact (m args).
simpl in m, args.
destruct args.
exact (IHIn (m c) p).
Defined.
Theorem apply_morphism_compatibility_Right2Left:
forall In Out (m1 m2: function_type_of_morphism_signature In Out)
(args1 args2: product_of_arguments In),
make_compatibility_goal_aux _ _ m1 m2 ->
relation_of_product_of_arguments Right2Left _ args1 args2 ->
directed_relation_of_relation_class Right2Left _
(apply_morphism _ _ m2 args1)
(apply_morphism _ _ m1 args2).
induction In; intros Out m1 m2 args1 args2 H H0.
simpl in m1, m2, args1, args2, H0 |- *.
destruct a; simpl in H; hnf in H0.
apply H; exact H0.
destruct v; simpl in H0; apply H; exact H0.
apply H; exact H0.
destruct v; simpl in H0; apply H; exact H0.
rewrite H0; apply H; exact H0.
simpl in m1, m2, args1, args2, H0 |- *.
destruct args1; destruct args2; simpl.
destruct H0 as [ H0 H1 ].
simpl in H.
destruct a; simpl in H.
apply IHIn.
apply H; exact H0.
exact H1.
destruct v.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
apply H; exact H0.
exact H1.
destruct v.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
apply H; exact H0.
exact H1.
rewrite H0; apply IHIn.
apply H.
exact H1.
Qed.
Theorem apply_morphism_compatibility_Left2Right:
forall In Out (m1 m2: function_type_of_morphism_signature In Out)
(args1 args2: product_of_arguments In),
make_compatibility_goal_aux _ _ m1 m2 ->
relation_of_product_of_arguments Left2Right _ args1 args2 ->
directed_relation_of_relation_class Left2Right _
(apply_morphism _ _ m1 args1)
(apply_morphism _ _ m2 args2).
induction In; intros Out m1 m2 args1 args2 H H0.
simpl in m1, m2, args1, args2, H0 |- *.
destruct a; simpl in H; hnf in H0.
apply H; exact H0.
destruct v; simpl in H0; apply H; exact H0.
apply H; exact H0.
destruct v; simpl in H0; apply H; exact H0.
rewrite H0; apply H; exact H0.
simpl in m1, m2, args1, args2, H0 |- *.
destruct args1; destruct args2; simpl.
destruct H0 as [ H0 H1 ].
simpl in H.
destruct a; simpl in H.
apply IHIn.
apply H; exact H0.
exact H1.
destruct v.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
apply H; exact H0.
exact H1.
apply IHIn.
destruct v; simpl in H, H0; apply H; exact H0.
exact H1.
rewrite H0; apply IHIn.
apply H.
exact H1.
Qed.
Definition interp :
forall Hole dir Out dir', carrier_of_relation_class Hole ->
Morphism_Context Hole dir Out dir' -> carrier_of_relation_class Out.
intros Hole dir Out dir' H t.
elim t using
(@Morphism_Context_rect2 Hole dir (fun S _ _ => carrier_of_relation_class S)
(fun _ L fcl => product_of_arguments L));
intros.
exact (apply_morphism _ _ (Function m) X).
exact H.
exact c.
exact x.
simpl;
rewrite <-
(about_carrier_of_relation_class_and_relation_class_of_argument_class
S);
exact X.
split.
rewrite <-
(about_carrier_of_relation_class_and_relation_class_of_argument_class
S);
exact X.
exact X0.
Defined.
(*CSC: interp and interp_relation_class_list should be mutually defined, since
the proof term of each one contains the proof term of the other one.
However
I cannot do that interactively (I should write the Fix by hand) *)
Definition interp_relation_class_list :
forall Hole dir dir' (L: Arguments), carrier_of_relation_class Hole ->
Morphism_Context_List Hole dir dir' L -> product_of_arguments L.
intros Hole dir dir' L H t.
elim t using
(@Morphism_Context_List_rect2 Hole dir (fun S _ _ =>
carrier_of_relation_class S)
(fun _ L fcl => product_of_arguments L));
intros.
exact (apply_morphism _ _ (Function m) X).
exact H.
exact c.
exact x.
simpl;
rewrite <-
(about_carrier_of_relation_class_and_relation_class_of_argument_class
S);
exact X.
split.
rewrite <-
(about_carrier_of_relation_class_and_relation_class_of_argument_class
S);
exact X.
exact X0.
Defined.
Theorem setoid_rewrite:
forall Hole dir Out dir' (E1 E2: carrier_of_relation_class Hole)
(E: Morphism_Context Hole dir Out dir'),
(directed_relation_of_relation_class dir Hole E1 E2) ->
(directed_relation_of_relation_class dir' Out (interp E1 E) (interp E2
E)).
(*
intros.
elim E using
(@Morphism_Context_rect2 Hole dir
(fun S dir'' E => directed_relation_of_relation_class dir'' S (interp E1
E) (interp E2 E))
(fun dir'' L fcl =>
relation_of_product_of_arguments dir'' _
(interp_relation_class_list E1 fcl)
(interp_relation_class_list E2 fcl))); intros.
change (directed_relation_of_relation_class dir'0 Out0
(apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
(apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
destruct dir'0.
apply apply_morphism_compatibility_Left2Right.
exact (Compat m).
exact X0.
apply apply_morphism_compatibility_Right2Left.
exact (Compat m).
exact X0.
exact X.
unfold interp, Morphism_Context_rect2.
(*CSC: reflexivity used here*)
destruct S; destruct dir'0; simpl; (apply r || reflexivity).
destruct dir'0; exact r.
destruct S; unfold directed_relation_of_argument_class; simpl in X0 |- *;
unfold get_rewrite_direction; simpl.
destruct dir'0; destruct dir'';
(exact X0 ||
unfold directed_relation_of_argument_class; simpl; apply s; exact X0).
(* the following mess with generalize/clear/intros is to help Coq
resolving *)
(* second order unification problems.
*)
generalize m c X0; clear X0 m c; inversion c;
generalize m c; clear m c; rewrite <- H0; rewrite <- H1; intros;
(exact H2 || rewrite (opposite_direction_idempotent dir'0); apply
H2).
destruct dir'0; destruct dir'';
(exact H0 ||
unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
(* the following mess with generalize/clear/intros is to help Coq resolving *)
(* second order unification problems.
*)
generalize m c H0; clear H0 m c; inversion c;
generalize m c; clear m c; rewrite <- H1; rewrite <- H2; intros;
(exact H3 || rewrite (opposite_direction_idempotent dir'0); apply
H3).
destruct dir'0; destruct dir''; (exact H0 || hnf; symmetry; exact H0).
change
(directed_relation_of_argument_class (get_rewrite_direction dir'' S) S
(eq_rect _ (fun T : Type => T) (interp E1 m) _
(about_carrier_of_relation_class_and_relation_class_of_argument_class S))
(eq_rect _ (fun T : Type => T) (interp E2 m) _
(about_carrier_of_relation_class_and_relation_class_of_argument_class S)) /\
relation_of_product_of_arguments dir'' _
(interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
split.
clear m0 H1; destruct S; simpl in H0 |- *; unfold get_rewrite_direction;
simpl.
destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
inversion c.
rewrite <- H3; exact H0.
rewrite (opposite_direction_idempotent dir'0); exact H0.
destruct dir''; destruct dir'0; (exact H0 || hnf; apply s; exact H0).
inversion c.
rewrite <- H3; exact H0.
rewrite (opposite_direction_idempotent dir'0); exact H0.
destruct dir''; destruct dir'0; (exact H0 || hnf; symmetry; exact H0).
exact H1.
Qed.
*) Admitted.
(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
Record Setoid_Theory (A: Type) (Aeq: relationT A) : Type :=
{Seq_refl : forall x:A, Aeq x x;
Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}.
(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
(* A FEW EXAMPLES ON iff *)
(* impl IS A MORPHISM *)
Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
unfold impl; tauto.
Qed.
(* and IS A MORPHISM *)
Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
tauto.
Qed.
(* or IS A MORPHISM *)
Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
tauto.
Qed.
(* not IS A MORPHISM *)
Add Morphism not with signature iff ==> iff as Not_Morphism.
tauto.
Qed.
(* THE SAME EXAMPLES ON impl *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
unfold impl; tauto.
Qed.
Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
unfold impl; tauto.
Qed.
Add Morphism not with signature impl --> impl as Not_Morphism2.
unfold impl; tauto.
Qed.
(* FOR BACKWARD COMPATIBILITY *)
Implicit Arguments Setoid_Theory [].
Implicit Arguments Seq_refl [].
Implicit Arguments Seq_sym [].
Implicit Arguments Seq_trans [].
Require Import Setoid.
Require Import Arith.
Require Import Relations.
Require Import Compare_dec.
Require Import ArithRing.
Require Import Omega.
Set Implicit Arguments.
(* We represent integers as pairs of Peano numbers *)
Delimit Scope Z'_scope with Z'.
Open Scope Z'_scope.
Inductive Z' : Type :=
mkZ' : nat -> nat -> Z'.
(* The equivalence relation on Z' *)
Definition Z'eq (z z':Z') : Prop :=
let (a, b) := z in
let (c, d) := z' in a + d = b + c.
Notation "a =Z= b" := (Z'eq a b) (at level 70): Z'_scope.
(* Z'eq is an equivalence relation *)
Lemma Z'eq_refl : reflexive Z' Z'eq.
Admitted.
Lemma Z'eq_sym : symmetric _ Z'eq.
Admitted.
Lemma Z'eq_trans : transitive _ Z'eq.
Admitted.
(* We can now build a setoid *)
Theorem Z'oid : Setoid_Theory _ Z'eq.
split.
exact Z'eq_refl.
exact Z'eq_sym.
exact Z'eq_trans.
Qed.
Add Setoid Z' Z'eq Z'oid as Z'_register.
Inductive Z'pos : Z' -> Prop :=
mkpos : forall (a b:nat), b < a -> Z'pos (mkZ' a b).
Add Morphism Z'pos : pos_morph.
destruct x1.
destruct x2.
simpl.
split;
inversion 1;split;omega.
Qed.
Inductive eqSet(A B:Set):Set:=
|mk_eq_set:(A->B)->(B->A)->eqSet A B.
Lemma eqSet_reflexive: forall A, eqSet A A.
constructor; trivial.
Qed.
Lemma eqSet_symmetric: forall A B, eqSet A B -> eqSet B A.
intros; destruct H; constructor; trivial.
Qed.
Lemma eqSet_transitive: forall A B C, eqSet A B -> eqSet B C -> eqSet A C.
intros; destruct H; destruct H0; constructor; auto.
Qed.
Inductive Z'pos2 : Z' -> Type :=
mkpos2 : forall (a b:nat), b < a -> Z'pos2 (mkZ' a b).
Add Morphism Z'pos2
with signature Z'eq ==> Setoid.iffT
as pos_morph2.
destruct x1.
destruct x2.
simpl.
split; intro HH; inversion HH; exists; omega.
Qed.
Theorem test: forall (x y: Z'), Z'eq x y -> Z'pos2 x -> Z'pos2 y.
intros.
rewrite <- H.
assumption.
Qed.
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id: setoid_replace.ml,v 1.106 2005/01/18 10:32:48 sacerdot Exp $ *)
open Tacmach
open Proof_type
open Libobject
open Reductionops
open Term
open Termops
open Names
open Entries
open Libnames
open Nameops
open Util
open Pp
open Printer
open Environ
open Clenv
open Unification
open Tactics
open Tacticals
open Vernacexpr
open Safe_typing
open Nametab
open Decl_kinds
open Constrintern
open Mod_subst
let replace = ref (fun _ _ -> assert false)
let register_replace f = replace := f
let general_rewrite = ref (fun _ _ -> assert false)
let register_general_rewrite f = general_rewrite := f
(* util function; it should be in util.mli *)
let prlist_with_sepi sep elem =
let rec aux n =
function
| [] -> mt ()
| [h] -> elem n h
| h::t ->
let e = elem n h and s = sep() and r = aux (n+1) t in
e ++ s ++ r
in
aux 1
type relation =
{ rel_a: constr ;
rel_aeq: constr;
rel_refl: constr option;
rel_sym: constr option;
rel_trans : constr option;
rel_quantifiers_no: int (* it helps unification *);
rel_X_relation_class: constr;
rel_Xreflexive_relation_class: constr
}
type 'a relation_class =
Relation of 'a (* the rel_aeq of the relation or the relation
*)
| Leibniz of constr option (* the carrier (if eq is partially instantiated)
*)
type 'a morphism =
{ args : (bool option * 'a relation_class) list;
output : 'a relation_class;
lem : constr;
morphism_theory : constr
}
type funct =
{ f_args : constr list;
f_output : constr
}
type morphism_class =
ACMorphism of relation morphism
| ACFunction of funct
let subst_mps_in_relation_class subst =
function
Relation t -> Relation (subst_mps subst t)
| Leibniz t -> Leibniz (option_app (subst_mps subst) t)
let subst_mps_in_argument_class subst (variance,rel) =
variance, subst_mps_in_relation_class subst rel
let constr_relation_class_of_relation_relation_class =
function
Relation relation -> Relation relation.rel_aeq
| Leibniz t -> Leibniz t
let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s
let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s
let eval_reference dir s = EvalConstRef (destConst (constant dir s))
let eval_init_reference dir s = EvalConstRef (destConst (gen_constant
("Init"::dir) s))
let current_constant id =
try
global_reference id
with Not_found ->
anomaly ("Setoid: cannot find " ^ (string_of_id id))
(* From Setoid.v *)
let coq_reflexiveT = lazy(constant ["Setoid"] "reflexiveT")
let coq_symmetricT = lazy(constant ["Setoid"] "symmetricT")
let coq_transitiveT = lazy(constant ["Setoid"] "transitiveT")
let coq_relationT = lazy(constant ["Setoid"] "relationT")
let coq_Relation_Class = lazy(constant ["Setoid"] "Relation_Class")
let coq_Argument_Class = lazy(constant ["Setoid"] "Argument_Class")
let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory")
let coq_Morphism_Theory = lazy(constant ["Setoid"] "Morphism_Theory")
let coq_Build_Morphism_Theory= lazy(constant ["Setoid"]
"Build_Morphism_Theory")
let coq_Compat = lazy(constant ["Setoid"] "Compat")
let coq_AsymmetricReflexive = lazy(constant ["Setoid"] "AsymmetricReflexive")
let coq_SymmetricReflexive = lazy(constant ["Setoid"] "SymmetricReflexive")
let coq_SymmetricAreflexive = lazy(constant ["Setoid"] "SymmetricAreflexive")
let coq_AsymmetricAreflexive = lazy(constant ["Setoid"]
"AsymmetricAreflexive")
let coq_Leibniz = lazy(constant ["Setoid"] "Leibniz")
let coq_RAsymmetric = lazy(constant ["Setoid"] "RAsymmetric")
let coq_RSymmetric = lazy(constant ["Setoid"] "RSymmetric")
let coq_RLeibniz = lazy(constant ["Setoid"] "RLeibniz")
let coq_ASymmetric = lazy(constant ["Setoid"] "ASymmetric")
let coq_AAsymmetric = lazy(constant ["Setoid"] "AAsymmetric")
let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl")
let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym")
let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans")
let coq_variance = lazy(constant ["Setoid"] "variance")
let coq_Covariant = lazy(constant ["Setoid"] "Covariant")
let coq_Contravariant = lazy(constant ["Setoid"] "Contravariant")
let coq_Left2Right = lazy(constant ["Setoid"] "Left2Right")
let coq_Right2Left = lazy(constant ["Setoid"] "Right2Left")
let coq_MSNone = lazy(constant ["Setoid"] "MSNone")
let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant")
let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant")
let coq_singl = lazy(constant ["Setoid"] "singl")
let coq_cons = lazy(constant ["Setoid"] "cons")
let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation =
lazy(constant ["Setoid"]
"equality_morphism_of_asymmetric_areflexive_transitive_relation")
let coq_equality_morphism_of_symmetric_areflexive_transitive_relation =
lazy(constant ["Setoid"]
"equality_morphism_of_symmetric_areflexive_transitive_relation")
let coq_equality_morphism_of_asymmetric_reflexive_transitive_relation =
lazy(constant ["Setoid"]
"equality_morphism_of_asymmetric_reflexive_transitive_relation")
let coq_equality_morphism_of_symmetric_reflexive_transitive_relation =
lazy(constant ["Setoid"]
"equality_morphism_of_symmetric_reflexive_transitive_relation")
let coq_make_compatibility_goal =
lazy(constant ["Setoid"] "make_compatibility_goal")
let coq_make_compatibility_goal_eval_ref =
lazy(eval_reference ["Setoid"] "make_compatibility_goal")
let coq_make_compatibility_goal_aux_eval_ref =
lazy(eval_reference ["Setoid"] "make_compatibility_goal_aux")
let coq_App = lazy(constant ["Setoid"] "App")
let coq_ToReplace = lazy(constant ["Setoid"] "ToReplace")
let coq_ToKeep = lazy(constant ["Setoid"] "ToKeep")
let coq_ProperElementToKeep = lazy(constant ["Setoid"] "ProperElementToKeep")
let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl")
let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons")
let coq_setoid_rewrite = lazy(constant ["Setoid"] "setoid_rewrite")
let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
let coq_proj1T = lazy(constant ["Setoid"] "proj1T'")
let coq_proj2T = lazy(constant ["Setoid"] "proj2T'")
let coq_unit = lazy(gen_constant ["Init"; "Datatypes"] "unit")
let coq_tt = lazy(gen_constant ["Init"; "Datatypes"] "tt")
let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq")
let coq_morphism_theory_of_function =
lazy(constant ["Setoid"] "morphism_theory_of_function")
let coq_morphism_theory_of_predicate =
lazy(constant ["Setoid"] "morphism_theory_of_predicate")
let coq_morphism_theory_of_predicateT =
lazy(constant ["Setoid"] "morphism_theory_of_predicateT")
let coq_relation_of_relation_class =
lazy(eval_reference ["Setoid"] "relation_of_relation_class")
let coq_directed_relation_of_relation_class =
lazy(eval_reference ["Setoid"] "directed_relation_of_relation_class")
let coq_interp = lazy(eval_reference ["Setoid"] "interp")
let coq_Morphism_Context_rect2 =
lazy(eval_reference ["Setoid"] "Morphism_Context_rect2")
let coq_iff = lazy(gen_constant ["Init"; "Logic"] "iff")
let coq_iffT = lazy(constant ["Setoid"] "iffT")
let coq_impl = lazy(constant ["Setoid"] "impl")
let coq_implT = lazy(constant ["Setoid"] "implT")
(************************* Table of declared relations **********************)
(* Relations are stored in a table which is synchronised with the Reset
mechanism. *)
let relation_table = ref Gmap.empty
let relation_table_add (s,th) = relation_table := Gmap.add s th
!relation_table
let relation_table_find s = Gmap.find s !relation_table
let relation_table_mem s = Gmap.mem s !relation_table
let prrelation s =
str "(" ++ prterm s.rel_a ++ str "," ++ prterm s.rel_aeq ++ str ")"
let prrelation_class =
function
Relation eq ->
(try prrelation (relation_table_find eq)
with Not_found ->
str "[[ Error: " ++ prterm eq ++
str " is not registered as a relation ]]")
| Leibniz (Some ty) -> prterm ty
| Leibniz None -> str "_"
let prmorphism_argument_gen prrelation (variance,rel) =
prrelation rel ++
match variance with
None -> str " ==> "
| Some true -> str " ++> "
| Some false -> str " --> "
let prargument_class = prmorphism_argument_gen prrelation_class
let pr_morphism_signature (l,c) =
prlist (prmorphism_argument_gen Ppconstrnew.pr_constr) l ++
Ppconstrnew.pr_constr c
let prmorphism k m =
prterm k ++ str ": " ++
prlist prargument_class m.args ++
prrelation_class m.output
(* A function that gives back the only relation_class on a given carrier *)
(*CSC: this implementation is really inefficient. I should define a new
map to make it efficient. However, is this really worth of? *)
let default_relation_for_carrier ?(filter=fun _ -> true) a =
let rng = Gmap.rng !relation_table in
match List.filter (fun ({rel_a=rel_a} as r) -> rel_a = a && filter r) rng
with
[] -> Leibniz (Some a)
| relation::tl ->
if tl <> [] then
ppnl
(str "Warning: There are several relations on the carrier \"" ++
prterm a ++ str "\". The relation " ++ prrelation relation ++
str " is chosen.") ;
Relation relation
let find_relation_class rel =
try Relation (relation_table_find rel)
with
Not_found ->
let rel = Reduction.whd_betadeltaiota (Global.env ()) rel in
match kind_of_term rel with
| App (eq,[|ty|]) when eq_constr eq (Lazy.force coq_eq) -> Leibniz (Some
ty)
| _ when eq_constr rel (Lazy.force coq_eq) -> Leibniz None
| _ -> raise Not_found
let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff))
let coq_iffT_relation = lazy (find_relation_class (Lazy.force coq_iffT))
let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl))
let coq_implT_relation = lazy (find_relation_class (Lazy.force coq_implT))
let relation_morphism_of_constr_morphism =
let relation_relation_class_of_constr_relation_class =
function
Leibniz t -> Leibniz t
| Relation aeq ->
Relation (try relation_table_find aeq with Not_found -> assert false)
in
function mor ->
let args' =
List.map
(fun (variance,rel) ->
variance, relation_relation_class_of_constr_relation_class rel
) mor.args in
let output' = relation_relation_class_of_constr_relation_class mor.output
in
{mor with args=args' ; output=output'}
let subst_relation subst relation =
let rel_a' = subst_mps subst relation.rel_a in
let rel_aeq' = subst_mps subst relation.rel_aeq in
let rel_refl' = option_app (subst_mps subst) relation.rel_refl in
let rel_sym' = option_app (subst_mps subst) relation.rel_sym in
let rel_trans' = option_app (subst_mps subst) relation.rel_trans in
let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in
let rel_Xreflexive_relation_class' =
subst_mps subst relation.rel_Xreflexive_relation_class
in
if rel_a' == relation.rel_a
&& rel_aeq' == relation.rel_aeq
&& rel_refl' == relation.rel_refl
&& rel_sym' == relation.rel_sym
&& rel_trans' == relation.rel_trans
&& rel_X_relation_class' == relation.rel_X_relation_class
&&
rel_Xreflexive_relation_class'==relation.rel_Xreflexive_relation_class
then
relation
else
{ rel_a = rel_a' ;
rel_aeq = rel_aeq' ;
rel_refl = rel_refl' ;
rel_sym = rel_sym';
rel_trans = rel_trans';
rel_quantifiers_no = relation.rel_quantifiers_no;
rel_X_relation_class = rel_X_relation_class';
rel_Xreflexive_relation_class = rel_Xreflexive_relation_class'
}
let equiv_list () = List.map (fun x -> x.rel_aeq) (Gmap.rng !relation_table)
let _ =
Summary.declare_summary "relation-table"
{ Summary.freeze_function = (fun () -> !relation_table);
Summary.unfreeze_function = (fun t -> relation_table := t);
Summary.init_function = (fun () -> relation_table := Gmap .empty);
Summary.survive_module = false;
Summary.survive_section = false }
(* Declare a new type of object in the environment : "relation-theory". *)
let (relation_to_obj, obj_to_relation)=
let cache_set (_,(s, th)) =
let th' =
if relation_table_mem s then
begin
let old_relation = relation_table_find s in
let th' =
{th with rel_sym =
match th.rel_sym with
None -> old_relation.rel_sym
| Some t -> Some t} in
ppnl
(str "Warning: The relation " ++ prrelation th' ++
str " is redeclared. The new declaration" ++
(match th'.rel_refl with
None -> str ""
| Some t -> str " (reflevity proved by " ++ prterm t) ++
(match th'.rel_sym with
None -> str ""
| Some t ->
(if th'.rel_refl = None then str " (" else str " and ") ++
str "symmetry proved by " ++ prterm t) ++
(if th'.rel_refl <> None && th'.rel_sym <> None then
str ")" else str "") ++
str " replaces the old declaration" ++
(match old_relation.rel_refl with
None -> str ""
| Some t -> str " (reflevity proved by " ++ prterm t) ++
(match old_relation.rel_sym with
None -> str ""
| Some t ->
(if old_relation.rel_refl = None then
str " (" else str " and ") ++
str "symmetry proved by " ++ prterm t) ++
(if old_relation.rel_refl <> None && old_relation.rel_sym <> None
then str ")" else str "") ++
str ".");
th'
end
else
th
in
relation_table_add (s,th')
and subst_set (_,subst,(s,th as obj)) =
let s' = subst_mps subst s in
let th' = subst_relation subst th in
if s' == s && th' == th then obj else
(s',th')
and export_set x = Some x
in
declare_object {(default_object "relation-theory") with
cache_function = cache_set;
load_function = (fun i o -> cache_set o);
subst_function = subst_set;
classify_function = (fun (_,x) -> Substitute x);
export_function = export_set}
(******************************* Table of declared morphisms
********************)
(* Setoids are stored in a table which is synchronised with the Reset
mechanism. *)
let morphism_table = ref Gmap.empty
let morphism_table_find m = Gmap.find m !morphism_table
let morphism_table_add (m,c) =
let old =
try
morphism_table_find m
with
Not_found -> []
in
try
let old_morph =
List.find
(function mor -> mor.args = c.args && mor.output = c.output) old
in
ppnl
(str "Warning: The morphism " ++ prmorphism m old_morph ++
str " is redeclared. " ++
str "The new declaration whose compatibility is proved by " ++
prterm c.lem ++ str " replaces the old declaration whose" ++
str " compatibility was proved by " ++
prterm old_morph.lem ++ str ".")
with
Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table
let default_morphism ?(filter=fun _ -> true) m =
match List.filter filter (morphism_table_find m) with
[] -> raise Not_found
| m1::ml ->
if ml <> [] then
ppnl
(str "Warning: There are several morphisms associated to \"" ++
prterm m ++ str"\". Morphism " ++ prmorphism m m1 ++
str " is randomly chosen.");
relation_morphism_of_constr_morphism m1
let subst_morph subst morph =
let lem' = subst_mps subst morph.lem in
let args' = list_smartmap (subst_mps_in_argument_class subst) morph.args in
let output' = subst_mps_in_relation_class subst morph.output in
let morphism_theory' = subst_mps subst morph.morphism_theory in
if lem' == morph.lem
&& args' == morph.args
&& output' == morph.output
&& morphism_theory' == morph.morphism_theory
then
morph
else
{ args = args' ;
output = output' ;
lem = lem' ;
morphism_theory = morphism_theory'
}
let _ =
Summary.declare_summary "morphism-table"
{ Summary.freeze_function = (fun () -> !morphism_table);
Summary.unfreeze_function = (fun t -> morphism_table := t);
Summary.init_function = (fun () -> morphism_table := Gmap .empty);
Summary.survive_module = false;
Summary.survive_section = false }
(* Declare a new type of object in the environment : "morphism-definition". *)
let (morphism_to_obj, obj_to_morphism)=
let cache_set (_,(m, c)) = morphism_table_add (m, c)
and subst_set (_,subst,(m,c as obj)) =
let m' = subst_mps subst m in
let c' = subst_morph subst c in
if m' == m && c' == c then obj else
(m',c')
and export_set x = Some x
in
declare_object {(default_object "morphism-definition") with
cache_function = cache_set;
load_function = (fun i o -> cache_set o);
subst_function = subst_set;
classify_function = (fun (_,x) -> Substitute x);
export_function = export_set}
(************************** Printing relations and morphisms
**********************)
let print_setoids () =
Gmap.iter
(fun k relation ->
assert (k=relation.rel_aeq) ;
ppnl (str"Relation " ++ prrelation relation ++ str";" ++
(match relation.rel_refl with
None -> str ""
| Some t -> str" reflexivity proved by " ++ prterm t) ++
(match relation.rel_sym with
None -> str ""
| Some t -> str " symmetry proved by " ++ prterm t) ++
(match relation.rel_trans with
None -> str ""
| Some t -> str " transitivity proved by " ++ prterm t)))
!relation_table ;
Gmap.iter
(fun k l ->
List.iter
(fun ({lem=lem} as mor) ->
ppnl (str "Morphism " ++ prmorphism k mor ++
str ". Compatibility proved by " ++
prterm lem ++ str "."))
l) !morphism_table
;;
(***************** Adding a morphism to the database
****************************)
(* We maintain a table of the currently edited proofs of morphism lemma
in order to add them in the morphism_table when the user does Save *)
let edited = ref Gmap.empty
let new_edited id m =
edited := Gmap.add id m !edited
let is_edited id =
Gmap.mem id !edited
let no_more_edited id =
edited := Gmap.remove id !edited
let what_edited id =
Gmap.find id !edited
(* also returns the triple (args_ty_quantifiers_rev,real_args_ty,real_output)
where the args_ty and the output are delifted *)
let check_is_dependent n args_ty output =
let args_ty_quantifiers, args_ty = Util.list_chop n args_ty in
let delift n = substl (Array.to_list (Array.make n (mkRel 1) (* dummy *))) in
let rec aux t =
match kind_of_term t with
Prod (n,s,t) ->
if not (dependent (mkRel 1) t) then
let args,out = aux (subst1 (mkRel 1) (* dummy *) t) in
s::args,out
else
errorlabstrm "New Morphism"
(str "The morphism is not a quantified non dependent product.")
| _ -> [],t
in
let ty = compose_prod (List.rev args_ty) output in
let args_ty, output = aux ty in
List.rev args_ty_quantifiers, args_ty, output
let cic_relation_class_of_X_relation typ value =
function
{rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
mkApp ((Lazy.force coq_AsymmetricReflexive),
[| typ ; value ; rel_a ; rel_aeq; refl |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
mkApp ((Lazy.force coq_SymmetricReflexive),
[| typ ; rel_a ; rel_aeq; sym ; refl |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
mkApp ((Lazy.force coq_AsymmetricAreflexive),
[| typ ; value ; rel_a ; rel_aeq |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
mkApp ((Lazy.force coq_SymmetricAreflexive),
[| typ ; rel_a ; rel_aeq; sym |])
let cic_relation_class_of_X_relation_class typ value =
function
Relation {rel_X_relation_class=x_relation_class} ->
mkApp (x_relation_class, [| typ ; value |])
| Leibniz (Some t) ->
mkApp ((Lazy.force coq_Leibniz), [| typ ; t |])
| Leibniz None -> assert false
let cic_precise_relation_class_of_relation =
function
{rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
mkApp ((Lazy.force coq_RAsymmetric), [| rel_a ; rel_aeq; refl |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
mkApp ((Lazy.force coq_RSymmetric), [| rel_a ; rel_aeq; sym ; refl |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
mkApp ((Lazy.force coq_AAsymmetric), [| rel_a ; rel_aeq |])
| {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
mkApp ((Lazy.force coq_ASymmetric), [| rel_a ; rel_aeq; sym |])
let cic_precise_relation_class_of_relation_class =
function
Relation
{rel_aeq=rel_aeq; rel_Xreflexive_relation_class=lem; rel_refl=rel_refl }
->
rel_aeq,lem,not(rel_refl=None)
| Leibniz (Some t) ->
mkApp ((Lazy.force coq_eq), [| t |]),
mkApp ((Lazy.force coq_RLeibniz), [| t |]), true
| Leibniz None -> assert false
let cic_relation_class_of_relation_class rel =
cic_relation_class_of_X_relation_class
(Lazy.force coq_unit) (Lazy.force coq_tt) rel
let cic_argument_class_of_argument_class (variance,arg) =
let coq_variant_value =
match variance with
None -> (Lazy.force coq_Covariant) (* dummy value, it won't be used *)
| Some true -> (Lazy.force coq_Covariant)
| Some false -> (Lazy.force coq_Contravariant)
in
cic_relation_class_of_X_relation_class (Lazy.force coq_variance)
coq_variant_value arg
let cic_arguments_of_argument_class_list args =
let rec aux =
function
[] -> assert false
| [last] ->
mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class; last
|])
| he::tl ->
mkApp ((Lazy.force coq_cons),
[| Lazy.force coq_Argument_Class; he ; aux tl |])
in
aux (List.map cic_argument_class_of_argument_class args)
let gen_compat_lemma_statement quantifiers_rev output args m =
let output = cic_relation_class_of_relation_class output in
let args = cic_arguments_of_argument_class_list args in
args, output,
compose_prod quantifiers_rev
(mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m
|]))
let morphism_theory_id_of_morphism_proof_id id =
id_of_string (string_of_id id ^ "_morphism_theory")
(* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *)
let apply_to_rels c l =
if l = [] then c
else
let len = List.length l in
applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l)
let apply_to_relation subst rel =
if subst = [||] then rel
else
let new_quantifiers_no = rel.rel_quantifiers_no - Array.length subst in
assert (new_quantifiers_no >= 0) ;
{ rel_a = mkApp (rel.rel_a, subst) ;
rel_aeq = mkApp (rel.rel_aeq, subst) ;
rel_refl = option_app (fun c -> mkApp (c,subst)) rel.rel_refl ;
rel_sym = option_app (fun c -> mkApp (c,subst)) rel.rel_sym;
rel_trans = option_app (fun c -> mkApp (c,subst)) rel.rel_trans;
rel_quantifiers_no = new_quantifiers_no;
rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst);
rel_Xreflexive_relation_class =
mkApp (rel.rel_Xreflexive_relation_class, subst) }
let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
let env = Global.env() in
let lem =
match lemma_infos with
None ->
(* the Morphism_Theory object has already been created *)
let applied_args =
let len = List.length quantifiers_rev in
let subst =
Array.of_list
(Util.list_map_i (fun i _ -> mkRel (len - i)) 0 quantifiers_rev)
in
List.map
(fun (v,rel) ->
match rel with
Leibniz (Some t) ->
assert (subst=[||]);
v, Leibniz (Some t)
| Leibniz None ->
assert (Array.length subst = 1);
v, Leibniz (Some (subst.(0)))
| Relation rel -> v, Relation (apply_to_relation subst rel)) args
in
compose_lam quantifiers_rev
(mkApp (Lazy.force coq_Compat,
[| cic_arguments_of_argument_class_list applied_args;
cic_relation_class_of_relation_class output;
apply_to_rels (current_constant mor_name) quantifiers_rev |]))
| Some (lem_name,argsconstr,outputconstr) ->
(* only the compatibility has been proved; we need to declare the
Morphism_Theory object *)
let mext = current_constant lem_name in
ignore (
Declare.declare_internal_constant mor_name
(DefinitionEntry
{const_entry_body =
compose_lam quantifiers_rev
(mkApp ((Lazy.force coq_Build_Morphism_Theory),
[| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ;
apply_to_rels mext quantifiers_rev |]));
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
IsDefinition)) ;
mext
in
let mmor = current_constant mor_name in
let args_constr =
List.map
(fun (variance,arg) ->
variance, constr_relation_class_of_relation_relation_class arg) args in
let output_constr = constr_relation_class_of_relation_relation_class output
in
Lib.add_anonymous_leaf
(morphism_to_obj (m,
{ args = args_constr;
output = output_constr;
lem = lem;
morphism_theory = mmor }));
Options.if_verbose ppnl (prterm m ++ str " is registered as a morphism")
(* first order matching with a bit of conversion *)
let unify_relation_carrier_with_type env rel t =
let raise_error quantifiers_no =
errorlabstrm "New Morphism"
(str "One morphism argument or its output has type " ++ prterm t ++
str " but the signature requires an argument of type \"" ++
prterm rel.rel_a ++ str " " ++ prvect_with_sep pr_spc (fun _ -> str "?")
(Array.make quantifiers_no 0) ++ str "\"") in
let args =
match kind_of_term t with
App (he',args') ->
let argsno = Array.length args' - rel.rel_quantifiers_no in
let args1 = Array.sub args' 0 argsno in
let args2 = Array.sub args' argsno rel.rel_quantifiers_no in
if is_conv_leq env Evd.empty (mkApp (he',args1)) rel.rel_a then
args2
else
raise_error rel.rel_quantifiers_no
| _ ->
if rel.rel_quantifiers_no = 0 && is_conv_leq env Evd.empty t rel.rel_a
then
[||]
else
raise_error rel.rel_quantifiers_no
in
apply_to_relation args rel
let unify_relation_class_carrier_with_type env rel t =
match rel with
Leibniz (Some t') ->
if is_conv env Evd.empty t t' then
rel
else
errorlabstrm "New Morphism"
(str "One morphism argument or its output has type " ++ prterm t ++
str " but the signature requires an argument of type " ++
prterm t')
| Leibniz None -> Leibniz (Some t)
| Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
(* first order matching with a bit of conversion *)
(* Note: the type checking operations performed by the function could *)
(* be done once and for all abstracting the morphism structure using *)
(* the quantifiers. Would the new structure be more suited than the *)
(* existent one for other tasks to? (e.g. pretty printing would expose *)
(* much more information: is it ok or is it too much information?) *)
let unify_morphism_with_arguments gl (c,av)
{args=args; output=output; lem=lem; morphism_theory=morphism_theory} t
=
let al = Array.to_list av in
let argsno = List.length args in
let quantifiers,al' = Util.list_chop (List.length al - argsno) al in
let quantifiersv = Array.of_list quantifiers in
let c' = mkApp (c,quantifiersv) in
if dependent t c' then None else (
(* these are pf_type_of we could avoid *)
let al'_type = List.map (Tacmach.pf_type_of gl) al' in
let args' =
List.map2
(fun (var,rel) ty ->
var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
args al'_type in
(* this is another pf_type_of we could avoid *)
let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in
let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty
in
let lem' = mkApp (lem,quantifiersv) in
let morphism_theory' = mkApp (morphism_theory,quantifiersv) in
Some
({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
c',Array.of_list al'))
let new_morphism m signature id hook =
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
errorlabstrm "New Morphism" (pr_id id ++ str " already exists")
else
let env = Global.env() in
let typeofm = Typing.type_of env Evd.empty m in
let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm
in
let argsrev, output = decompose_prod typ in
let args_ty = List.rev argsrev in
let args_ty_len = List.length (args_ty) in
let args_ty_quantifiers_rev,args,args_instance,output,output_instance =
match signature with
None ->
if args_ty = [] then
errorlabstrm "New Morphism"
(str "The term " ++ prterm m ++ str " has type " ++
prterm typeofm ++ str " that is not a product.") ;
ignore (check_is_dependent 0 args_ty output) ;
let args =
List.map
(fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
let output = default_relation_for_carrier output in
[],args,args,output,output
| Some (args,output') ->
assert (args <> []);
let number_of_arguments = List.length args in
let number_of_quantifiers = args_ty_len - number_of_arguments in
if number_of_quantifiers < 0 then
errorlabstrm "New Morphism"
(str "The morphism " ++ prterm m ++ str " has type " ++
prterm typeofm ++ str " that attends at most " ++ int args_ty_len ++
str " arguments. The signature that you specified requires " ++
int number_of_arguments ++ str " arguments.")
else
begin
(* the real_args_ty returned are already delifted *)
let args_ty_quantifiers_rev, real_args_ty, real_output =
check_is_dependent number_of_quantifiers args_ty output in
let find_relation_class t real_t =
try
let rel = find_relation_class t in
rel, unify_relation_class_carrier_with_type env rel real_t
with Not_found ->
errorlabstrm "Add Morphism"
(str "Not a valid signature: " ++ prterm t ++
str " is neither a registered relation nor the Leibniz " ++
str " equality.")
in
let find_relation_class_v (variance,t) real_t =
let relation,relation_instance = find_relation_class t real_t in
match relation, variance with
Leibniz _, None
| Relation {rel_sym = Some _}, None
| Relation {rel_sym = None}, Some _ ->
(variance, relation), (variance, relation_instance)
| Relation {rel_sym = None},None ->
errorlabstrm "Add Morphism"
(str "You must specify the variance in each argument " ++
str "whose relation is asymmetric.")
| Leibniz _, Some _
| Relation {rel_sym = Some _}, Some _ ->
errorlabstrm "Add Morphism"
(str "You cannot specify the variance of an argument " ++
str "whose relation is symmetric.")
in
let args, args_instance =
List.split
(List.map2 find_relation_class_v args real_args_ty) in
let output,output_instance= find_relation_class output' real_output
in
args_ty_quantifiers_rev, args, args_instance, output,
output_instance
end
in
let argsconstr,outputconstr,lem =
gen_compat_lemma_statement args_ty_quantifiers_rev output_instance
args_instance (apply_to_rels m args_ty_quantifiers_rev) in
(* "unfold make_compatibility_goal" *)
let lem =
Reductionops.clos_norm_flags
(Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref))
env Evd.empty lem in
(* "unfold make_compatibility_goal_aux" *)
let lem =
Reductionops.clos_norm_flags
(Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
env Evd.empty lem in
(* "simpl" *)
let lem = Tacred.nf env Evd.empty lem in
if Lib.is_modtype () then
begin
ignore
(Declare.declare_internal_constant id
(ParameterEntry lem, IsAssumption Logical)) ;
let mor_name = morphism_theory_id_of_morphism_proof_id id in
let lemma_infos = Some (id,argsconstr,outputconstr) in
add_morphism lemma_infos mor_name
(m,args_ty_quantifiers_rev,args,output)
end
else
begin
new_edited id
(m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
Pfedit.start_proof id (IsGlobal (Proof Lemma))
(Declare.clear_proofs (Global.named_context ()))
lem hook;
Options.if_verbose msg (Printer.pr_open_subgoals ());
end
let morphism_hook _ ref =
let pf_id = id_of_global ref in
let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in
let (m,quantifiers_rev,args,argsconstr,output,outputconstr) =
what_edited pf_id in
if (is_edited pf_id)
then
begin
add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
(m,quantifiers_rev,args,output) ;
no_more_edited pf_id
end
type morphism_signature =
(bool option * Topconstr.constr_expr) list * Topconstr.constr_expr
let new_named_morphism id m sign =
let sign =
match sign with
None -> None
| Some (args,out) ->
Some
(List.map (fun (variance,ty) -> variance, constr_of ty) args,
constr_of out)
in
new_morphism (constr_of m) sign id morphism_hook
(************************** Adding a relation to the database
*********************)
let check_a env a =
let typ = Typing.type_of env Evd.empty a in
let a_quantifiers_rev,_ = Reduction.dest_arity env typ in
a_quantifiers_rev
let check_eq env a_quantifiers_rev a aeq =
let typ =
Sign.it_mkProd_or_LetIn
(mkApp ((Lazy.force coq_relationT),[| apply_to_rels a a_quantifiers_rev
|]))
a_quantifiers_rev in
let aeqtyp = Typing.type_of env Evd.empty aeq in
if
not
(is_conv_leq env Evd.empty aeqtyp typ)
then
errorlabstrm "Add Relation Class"
(prterm aeq ++ str " should have type (" ++ prterm typ ++ str ")") ;
match Typing.sort_of env Evd.empty aeqtyp with
Term.Prop _ -> true
| Term.Type _ -> false
let check_property env a_quantifiers_rev a aeq strprop coq_prop t =
if
not
(is_conv env Evd.empty (Typing.type_of env Evd.empty t)
(Sign.it_mkProd_or_LetIn
(mkApp ((Lazy.force coq_prop),
[| apply_to_rels a a_quantifiers_rev ;
apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
then
errorlabstrm "Add Relation Class"
(str "Not a valid proof of " ++ str strprop ++ str ".")
let check_refl env a_quantifiers_rev a aeq refl =
check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexiveT refl
let check_sym env a_quantifiers_rev a aeq sym =
check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetricT sym
let check_trans env a_quantifiers_rev a aeq trans =
check_property env a_quantifiers_rev a aeq "transitivity" coq_transitiveT
trans
let check_setoid_theory env a_quantifiers_rev a aeq th =
if
not
(is_conv env Evd.empty (Typing.type_of env Evd.empty th)
(Sign.it_mkProd_or_LetIn
(mkApp ((Lazy.force coq_Setoid_Theory),
[| apply_to_rels a a_quantifiers_rev ;
apply_to_rels aeq a_quantifiers_rev |])) a_quantifiers_rev))
then
errorlabstrm "Add Relation Class"
(str "Not a valid proof of symmetry")
let int_add_relation id a aeq refl sym trans =
let env = Global.env () in
let a_quantifiers_rev = check_a env a in
let is_a_relation_in_Prop = check_eq env a_quantifiers_rev a aeq in
option_iter (check_refl env a_quantifiers_rev a aeq) refl ;
option_iter (check_sym env a_quantifiers_rev a aeq) sym ;
option_iter (check_trans env a_quantifiers_rev a aeq) trans ;
let quantifiers_no = List.length a_quantifiers_rev in
let aeq_rel =
{ rel_a = a;
rel_aeq = aeq;
rel_refl = refl;
rel_sym = sym;
rel_trans = trans;
rel_quantifiers_no = quantifiers_no;
rel_X_relation_class = mkProp; (* dummy value, overwritten below *)
rel_Xreflexive_relation_class = mkProp (* dummy value, overwritten below
*)
} in
let x_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
Array.of_list
(Util.list_map_i (fun i _ -> mkRel (len - i + 2)) 0 a_quantifiers_rev) in
cic_relation_class_of_X_relation
(mkRel 2) (mkRel 1) (apply_to_relation subst aeq_rel) in
let _ =
Declare.declare_internal_constant id
(DefinitionEntry
{const_entry_body =
Sign.it_mkLambda_or_LetIn x_relation_class
([ Name (id_of_string "v"),None,mkRel 1;
Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @
a_quantifiers_rev);
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
IsDefinition) in
let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class")
in
let xreflexive_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
Array.of_list
(Util.list_map_i (fun i _ -> mkRel (len - i)) 0 a_quantifiers_rev)
in
cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel)
in
let _ =
Declare.declare_internal_constant id_precise
(DefinitionEntry
{const_entry_body =
Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() },
IsDefinition) in
let aeq_rel =
{ aeq_rel with
rel_X_relation_class = current_constant id;
rel_Xreflexive_relation_class = current_constant id_precise } in
Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ;
Options.if_verbose ppnl (prterm aeq ++ str " is registered as a relation");
match trans with
None -> ()
| Some trans ->
let mor_name = id_of_string (string_of_id id ^ "_morphism") in
let a_instance = apply_to_rels a a_quantifiers_rev in
let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
let sym_instance =
option_app (fun x -> apply_to_rels x a_quantifiers_rev) sym in
let refl_instance =
option_app (fun x -> apply_to_rels x a_quantifiers_rev) refl in
let trans_instance = apply_to_rels trans a_quantifiers_rev in
let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
match sym_instance, refl_instance with
None, None ->
(Some false, Relation aeq_rel),
(Some true, Relation aeq_rel),
mkApp
((Lazy.force
coq_equality_morphism_of_asymmetric_areflexive_transitive_relation),
[| a_instance ; aeq_instance ; trans_instance |]),
(if is_a_relation_in_Prop then Lazy.force coq_impl_relation
else Lazy.force coq_implT_relation)
| None, Some refl_instance ->
(Some false, Relation aeq_rel),
(Some true, Relation aeq_rel),
mkApp
((Lazy.force
coq_equality_morphism_of_asymmetric_reflexive_transitive_relation),
[| a_instance ; aeq_instance ; refl_instance ; trans_instance
|]),
(if is_a_relation_in_Prop then Lazy.force coq_impl_relation
else Lazy.force coq_implT_relation)
| Some sym_instance, None ->
(None, Relation aeq_rel),
(None, Relation aeq_rel),
mkApp
((Lazy.force
coq_equality_morphism_of_symmetric_areflexive_transitive_relation),
[| a_instance ; aeq_instance ; sym_instance ; trans_instance
|]),
(if is_a_relation_in_Prop then Lazy.force coq_iff_relation
else Lazy.force coq_iffT_relation)
| Some sym_instance, Some refl_instance ->
(None, Relation aeq_rel),
(None, Relation aeq_rel),
mkApp
((Lazy.force
coq_equality_morphism_of_symmetric_reflexive_transitive_relation),
[| a_instance ; aeq_instance ; refl_instance ; sym_instance ;
trans_instance |]),
(if is_a_relation_in_Prop then Lazy.force coq_iff_relation
else Lazy.force coq_iffT_relation) in
let _ =
Declare.declare_internal_constant mor_name
(DefinitionEntry
{const_entry_body = Sign.it_mkLambda_or_LetIn lemma
a_quantifiers_rev;
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
IsDefinition)
in
let a_quantifiers_rev =
List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
add_morphism None mor_name
(aeq,a_quantifiers_rev,[aeq_rel_class_and_var1;
aeq_rel_class_and_var2],
output)
(* The vernac command "Add Relation ..." *)
let add_relation id a aeq refl sym trans =
int_add_relation id (constr_of a) (constr_of aeq) (option_app constr_of refl)
(option_app constr_of sym) (option_app constr_of trans)
(************************ Add Setoid
******************************************)
(* The vernac command "Add Setoid" *)
let add_setoid id a aeq th =
let a = constr_of a in
let aeq = constr_of aeq in
let th = constr_of th in
let env = Global.env () in
let a_quantifiers_rev = check_a env a in
let _ = check_eq env a_quantifiers_rev a aeq in
check_setoid_theory env a_quantifiers_rev a aeq th ;
let a_instance = apply_to_rels a a_quantifiers_rev in
let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
let th_instance = apply_to_rels th a_quantifiers_rev in
let refl =
Sign.it_mkLambda_or_LetIn
(mkApp ((Lazy.force coq_seq_refl),
[| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
let sym =
Sign.it_mkLambda_or_LetIn
(mkApp ((Lazy.force coq_seq_sym),
[| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
let trans =
Sign.it_mkLambda_or_LetIn
(mkApp ((Lazy.force coq_seq_trans),
[| a_instance; aeq_instance; th_instance |])) a_quantifiers_rev in
int_add_relation id a aeq (Some refl) (Some sym) (Some trans)
(****************************** The tactic itself
*******************************)
type direction =
Left2Right
| Right2Left
let prdirection =
function
Left2Right -> str "->"
| Right2Left -> str "<-"
type constr_with_marks =
| MApp of constr * morphism_class * constr_with_marks array * direction
| ToReplace
| ToKeep of constr * relation relation_class * direction
let is_to_replace = function
| ToKeep _ -> false
| ToReplace -> true
| MApp _ -> true
let get_mark a =
Array.fold_left (||) false (Array.map is_to_replace a)
let cic_direction_of_direction =
function
Left2Right -> Lazy.force coq_Left2Right
| Right2Left -> Lazy.force coq_Right2Left
let opposite_direction =
function
Left2Right -> Right2Left
| Right2Left -> Left2Right
let direction_of_constr_with_marks hole_direction =
function
MApp (_,_,_,dir) -> cic_direction_of_direction dir
| ToReplace -> hole_direction
| ToKeep (_,_,dir) -> cic_direction_of_direction dir
type argument =
Toapply of constr (* apply the function to the argument *)
| Toexpand of name * types (* beta-expand the function w.r.t. an argument
of this type *)
let beta_expand c args_rev =
let rec to_expand =
function
[] -> []
| (Toapply _)::tl -> to_expand tl
| (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in
let rec aux n =
function
[] -> []
| (Toapply arg)::tl -> arg::(aux n tl)
| (Toexpand _)::tl -> (mkRel n)::(aux (n + 1) tl)
in
compose_lam (to_expand args_rev)
(mkApp (c, Array.of_list (List.rev (aux 1 args_rev))))
exception Optimize (* used to fall-back on the tactic for Leibniz equality *)
let relation_class_that_matches_a_constr caller_name new_goals hypt =
let (heq, hargs) = decompose_app hypt in
let rec get_all_but_last_two =
function
[]
| [_] ->
errorlabstrm caller_name (prterm hypt ++
str " is not a registered relation.")
| [_;_] -> []
| he::tl -> he::(get_all_but_last_two tl) in
let all_aeq_args = get_all_but_last_two hargs in
let rec find_relation l subst =
let aeq = mkApp (heq,(Array.of_list l)) in
try
let rel = find_relation_class aeq in
match rel,new_goals with
Leibniz _,[] ->
assert (subst = []);
raise Optimize (* let's optimize the proof term size *)
| Leibniz (Some _), _ ->
assert (subst = []);
rel
| Leibniz None, _ ->
(* for well-typedness reasons it should have been catched by the
previous guard in the previous iteration. *)
assert false
| Relation rel,_ -> Relation (apply_to_relation (Array.of_list subst) rel)
with Not_found ->
if l = [] then
errorlabstrm caller_name
(prterm (mkApp (aeq, Array.of_list all_aeq_args)) ++
str " is not a registered relation.")
else
let last,others = Util.list_sep_last l in
find_relation others (last::subst)
in
find_relation all_aeq_args []
(* rel1 is a subrelation of rel2 whenever
forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
The Coq part of the tactic, however, needs rel1 == rel2.
Hence the third case commented out.
Note: accepting user-defined subtrelations seems to be the last
useful generalization that does not go against the original spirit of
the tactic.
*)
let subrelation gl rel1 rel2 =
match rel1,rel2 with
Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} ->
Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2
| Leibniz (Some t1), Leibniz (Some t2) ->
Tacmach.pf_conv_x gl t1 t2
| Leibniz None, _
| _, Leibniz None -> assert false
(* This is the commented out case (see comment above)
| Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} ->
Tacmach.pf_conv_x gl t1 t2
*)
| _,_ -> false
(* this function returns the list of new goals opened by a constr_with_marks
*)
let rec collect_new_goals =
function
MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list
a))
| ToReplace
| ToKeep (_,Leibniz _,_)
| ToKeep (_,Relation {rel_refl=Some _},_) -> []
| ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [mkApp(aeq,[|c ;
c|])]
(* two marked_constr are equivalent if they produce the same set of new goals
*)
let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 =
let glc1 = collect_new_goals (to_marked_constr c1) in
let glc2 = collect_new_goals (to_marked_constr c2) in
List.for_all (fun c -> List.exists (fun c' -> pf_conv_x gl c c') glc1) glc2
let pr_new_goals i c =
let glc = collect_new_goals c in
str " " ++ int i ++ str ") side conditions:" ++
(if glc = [] then str " no side conditions"
else
(pr_fnl () ++ str " " ++
prlist_with_sep (fun () -> str "\n ")
(fun c -> str " ... |- " ++ prterm c) glc))
(* given a list of constr_with_marks, it returns the list where
constr_with_marks than open more goals than simpler ones in the list
are got rid of *)
let elim_duplicates gl to_marked_constr =
let rec aux =
function
[] -> []
| he:: tl ->
if List.exists
(marked_constr_equiv_or_more_complex to_marked_constr gl he) tl
then aux tl
else he::aux tl
in
aux
let filter_superset_of_new_goals gl new_goals l =
List.filter
(fun (_,_,c) ->
List.for_all
(fun g -> List.exists (pf_conv_x gl g) (collect_new_goals c)) new_goals)
l
(* given the array of lists [| l1 ; ... ; ln |] it returns the list of arrays
[ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *)
let cartesian_product gl a =
let rec aux =
function
[] -> assert false
| [he] -> List.map (fun e -> [e]) he
| he::tl ->
let tl' = aux tl in
List.flatten
(List.map (function e -> List.map (function l -> e :: l) tl') he)
in
List.map Array.of_list
(aux (List.map (elim_duplicates gl identity) (Array.to_list a)))
let mark_occur gl ~new_goals t in_c input_relation input_direction =
let rec aux output_relation output_direction in_c =
if eq_constr t in_c then
if input_direction = output_direction
&& subrelation gl input_relation output_relation then
[ToReplace]
else []
else
match kind_of_term in_c with
| App (c,al) ->
let mors_and_cs_and_als =
let mors_and_cs_and_als =
let morphism_table_find c =
try morphism_table_find c with Not_found -> [] in
let rec aux acc =
function
[] ->
let c' = mkApp (c, Array.of_list acc) in
let al' = [||] in
List.map (fun m -> m,c',al') (morphism_table_find c')
| (he::tl) as l ->
let c' = mkApp (c, Array.of_list acc) in
let al' = Array.of_list l in
let acc' = acc @ [he] in
(List.map (fun m -> m,c',al') (morphism_table_find c')) @
(aux acc' tl)
in
aux [] (Array.to_list al) in
let mors_and_cs_and_als =
List.map
(function (m,c,al) ->
relation_morphism_of_constr_morphism m, c, al)
mors_and_cs_and_als in
let mors_and_cs_and_als =
List.fold_left
(fun l (m,c,al) ->
match unify_morphism_with_arguments gl (c,al) m t with
Some res -> res::l
| None -> l
) [] mors_and_cs_and_als
in
List.filter
(fun (mor,_,_) -> subrelation gl mor.output output_relation)
mors_and_cs_and_als
in
(* First we look for well typed morphisms *)
let res_mors =
List.fold_left
(fun res (mor,c,al) ->
let a =
let arguments = Array.of_list mor.args in
let apply_variance_to_direction default_dir =
function
None -> default_dir
| Some true -> output_direction
| Some false -> opposite_direction output_direction
in
Util.array_map2
(fun a (variance,relation) ->
(aux relation
(apply_variance_to_direction Left2Right variance) a) @
(aux relation
(apply_variance_to_direction Right2Left variance) a)
) al arguments
in
let a' = cartesian_product gl a in
(List.map
(function a ->
if not (get_mark a) then
ToKeep (in_c,output_relation,output_direction)
else
MApp (c,ACMorphism mor,a,output_direction)) a') @ res
) [] mors_and_cs_and_als in
(* Then we look for well typed functions *)
let res_functions =
(* the tactic works only if the function type is
made of non-dependent products only. However, here we
can cheat a bit by partially istantiating c to match
the requirement when the arguments to be replaced are
bound by non-dependent products only. *)
let typeofc = Tacmach.pf_type_of gl c in
let typ = nf_betaiota typeofc in
let rec find_non_dependent_function env c c_args_rev typ
f_args_rev
a_rev
=
function
[] ->
if a_rev = [] then
[ToKeep (in_c,output_relation,output_direction)]
else
let a' =
cartesian_product gl (Array.of_list (List.rev a_rev))
in
List.fold_left
(fun res a ->
if not (get_mark a) then
(ToKeep (in_c,output_relation,output_direction))::res
else
let err =
match output_relation with
Leibniz (Some typ') when pf_conv_x gl typ typ' ->
false
| Leibniz None -> assert false
| _ when output_relation = Lazy.force
coq_iffT_relation
|| output_relation = Lazy.force
coq_iff_relation
-> false
| _ -> true
in
if err then res
else
let mor =
ACFunction{f_args=List.rev f_args_rev;f_output=typ}
in
let func = beta_expand c c_args_rev in
(MApp (func,mor,a,output_direction))::res
) [] a'
| (he::tl) as a->
let typnf = Reduction.whd_betadeltaiota env typ in
match kind_of_term typnf with
Cast (typ,_) ->
find_non_dependent_function env c c_args_rev typ
f_args_rev a_rev a
| Prod (name,s,t) ->
let env' = push_rel (name,None,s) env in
let he =
(aux (Leibniz (Some s)) Left2Right he) @
(aux (Leibniz (Some s)) Right2Left he) in
if he = [] then []
else
let he0 = List.hd he in
begin
match noccurn 1 t, he0 with
_, ToKeep (arg,_,_) ->
(* invariant: if he0 = ToKeep (t,_,_) then every
element in he is = ToKeep (t,_,_) *)
assert
(List.for_all
(function
ToKeep(arg',_,_) when pf_conv_x gl arg arg'
->
true
| _ -> false) he) ;
(* generic product, to keep *)
find_non_dependent_function
env' c ((Toapply arg)::c_args_rev)
(subst1 arg t) f_args_rev a_rev tl
| true, _ ->
(* non-dependent product, to replace *)
find_non_dependent_function
env' c ((Toexpand (name,s))::c_args_rev)
(lift 1 t) (s::f_args_rev) (he::a_rev) tl
| false, _ ->
(* dependent product, to replace *)
(* This limitation is due to the reflexive
implementation and it is hard to lift *)
errorlabstrm "Setoid_replace"
(str "Cannot rewrite in the argument of a " ++
str "dependent product. If you need this " ++
str "feature, please report to the author.")
end
| _ -> assert false
in
find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] []
(Array.to_list al)
in
elim_duplicates gl identity (res_functions @ res_mors)
| Prod (_, c1, c2) ->
if (dependent (mkRel 1) c2)
then
errorlabstrm "Setoid_replace"
(str "Cannot rewrite in the type of a variable bound " ++
str "in a dependent product.")
else
(*CSC: ???
let typeofc1 = Tacmach.pf_type_of gl c1 in
if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then
(* to avoid this error we should introduce an impl relation
whose first argument is Type instead of Prop. However,
the type of the new impl would be Type -> Prop -> Prop
that is no longer a Relation_Definitions.relation. Thus
the Coq part of the tactic should be heavily modified. *)
errorlabstrm "Setoid_replace"
(str "Rewriting in a product A -> B is possible only when A " ++
str "is a proposition (i.e. A is of type Prop). The type " ++
prterm c1 ++ str " has type " ++ prterm typeofc1 ++
str " that is not convertible to Prop.")
else
*)
aux output_relation output_direction
(mkApp ((Lazy.force coq_implT),
[| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |]))
| _ -> [ToKeep (in_c,output_relation,output_direction)]
in
let aux2 output_relation output_direction =
List.map
(fun res -> output_relation,output_direction,res)
(aux output_relation output_direction in_c) in
let res =
(aux2 (Lazy.force coq_iffT_relation) Right2Left) @
(aux2 (Lazy.force coq_iff_relation) Right2Left) @
(* This is the case of a proposition of signature A ++> iff or B --> iff *)
(aux2 (Lazy.force coq_iffT_relation) Left2Right) @
(aux2 (Lazy.force coq_iff_relation) Left2Right) @
(aux2 (Lazy.force coq_implT_relation) Right2Left) @
(aux2 (Lazy.force coq_impl_relation) Right2Left) in
let res = elim_duplicates gl (function (_,_,t) -> t) res in
let res' = filter_superset_of_new_goals gl new_goals res in
match res' with
[] when res = [] ->
errorlabstrm "Setoid_rewrite"
(str "Either the term " ++ prterm t ++ str " that must be " ++
str "rewritten occurs in a covariant position or the goal is not " ++
str "made of morphism applications only. You can replace only " ++
str "occurrences that are in a contravariant position and such that "
++
str "the context obtained by abstracting them is made of morphism " ++
str "applications only.")
| [] ->
errorlabstrm "Setoid_rewrite"
(str "No generated set of side conditions is a superset of those " ++
str "requested by the user. The generated sets of side conditions " ++
str "are: " ++
pr_fnl () ++
prlist_with_sepi pr_fnl
(fun i (_,_,mc) -> pr_new_goals i mc) res)
| [he] -> he
| he::_ ->
ppnl
(str "Warning: The application of the tactic is subject to one of " ++
str "the \nfollowing set of side conditions that the user needs " ++
str "to prove:" ++
pr_fnl () ++
prlist_with_sepi pr_fnl
(fun i (_,_,mc) -> pr_new_goals i mc) res' ++ pr_fnl () ++
str "The first set is randomly chosen. Use the syntax " ++
str "\"setoid_rewrite ... generate side conditions ...\" to choose "
++
str "a different set.") ;
he
let cic_morphism_context_list_of_list hole_relation hole_direction
out_direction
=
let check =
function
(None,dir,dir') ->
mkApp ((Lazy.force coq_MSNone), [| dir ; dir' |])
| (Some true,dir,dir') ->
assert (dir = dir');
mkApp ((Lazy.force coq_MSCovariant), [| dir |])
| (Some false,dir,dir') ->
assert (dir <> dir');
mkApp ((Lazy.force coq_MSContravariant), [| dir |]) in
let rec aux =
function
[] -> assert false
| [(variance,out),(value,direction)] ->
mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class ; out
|]),
mkApp ((Lazy.force coq_fcl_singl),
[| hole_relation; hole_direction ; out ;
direction ; out_direction ;
check (variance,direction,out_direction) ; value |])
| ((variance,out),(value,direction))::tl ->
let outtl, valuetl = aux tl in
mkApp ((Lazy.force coq_cons),
[| Lazy.force coq_Argument_Class ; out ; outtl |]),
mkApp ((Lazy.force coq_fcl_cons),
[| hole_relation ; hole_direction ; out ; outtl ;
direction ; out_direction ;
check (variance,direction,out_direction) ;
value ; valuetl |])
in aux
let rec cic_type_nelist_of_list =
function
[] -> assert false
| [value] ->
mkApp ((Lazy.force coq_singl), [| mkType (Termops.new_univ ()) ; value
|])
| value::tl ->
mkApp ((Lazy.force coq_cons),
[| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])
let syntactic_but_representation_of_marked_but hole_relation hole_direction =
let rec aux out (rel_out,precise_out,is_reflexive) =
function
MApp (f, m, args, direction) ->
let direction = cic_direction_of_direction direction in
let morphism_theory, relations =
match m with
ACMorphism { args = args ; morphism_theory = morphism_theory } ->
morphism_theory,args
| ACFunction { f_args = f_args ; f_output = f_output } ->
let mt =
if eq_constr out (cic_relation_class_of_relation_class
(Lazy.force coq_iff_relation))
then
mkApp ((Lazy.force coq_morphism_theory_of_predicate),
[| cic_type_nelist_of_list f_args; f|])
else if eq_constr out (cic_relation_class_of_relation_class
(Lazy.force coq_iffT_relation))
then
mkApp ((Lazy.force coq_morphism_theory_of_predicateT),
[| cic_type_nelist_of_list f_args; f|])
else
mkApp ((Lazy.force coq_morphism_theory_of_function),
[| cic_type_nelist_of_list f_args; f_output; f|])
in
mt,List.map (fun x -> None,Leibniz (Some x)) f_args in
let cic_relations =
List.map
(fun (variance,r) ->
variance,
r,
cic_relation_class_of_relation_class r,
cic_precise_relation_class_of_relation_class r
) relations in
let cic_args_relations,argst =
cic_morphism_context_list_of_list hole_relation hole_direction
direction
(List.map2
(fun (variance,trel,t,precise_t) v ->
(variance,cic_argument_class_of_argument_class (variance,trel)),
(aux t precise_t v,
direction_of_constr_with_marks hole_direction v)
) cic_relations (Array.to_list args))
in
mkApp ((Lazy.force coq_App),
[|hole_relation ; hole_direction ;
cic_args_relations ; out ; direction ;
morphism_theory ; argst|])
| ToReplace ->
mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |])
| ToKeep (c,_,direction) ->
let direction = cic_direction_of_direction direction in
if is_reflexive then
mkApp ((Lazy.force coq_ToKeep),
[| hole_relation ; hole_direction ; precise_out ; direction ; c |])
else
let c_is_proper =
let typ = mkApp (rel_out, [| c ; c |]) in
mkCast (Evarutil.mk_new_meta (),typ)
in
mkApp ((Lazy.force coq_ProperElementToKeep),
[| hole_relation ; hole_direction; precise_out ;
direction; c ; c_is_proper |])
in aux
let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
prop_direction m
=
let hole_relation = cic_relation_class_of_relation_class hole_relation in
let hyp,hole_direction = h,cic_direction_of_direction direction in
let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in
let precise_prop_relation =
cic_precise_relation_class_of_relation_class prop_relation
in
mkApp ((Lazy.force coq_setoid_rewrite),
[| hole_relation ; hole_direction ; cic_prop_relation ;
prop_direction ; c1 ; c2 ;
syntactic_but_representation_of_marked_but hole_relation hole_direction
cic_prop_relation precise_prop_relation m ; hyp |])
let check_evar_map_of_evars_defs evd =
let metas = Evd.meta_list evd in
let check_freemetas_is_empty rebus =
Evd.Metaset.iter
(fun m ->
if Evd.meta_defined evd m then () else
raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
in
List.iter
(fun (_,binding) ->
match binding with
Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
check_freemetas_is_empty rebus freemetas
| Evd.Clval (_,{Evd.rebus=rebus1; Evd.freemetas=freemetas1},
{Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
check_freemetas_is_empty rebus1 freemetas1 ;
check_freemetas_is_empty rebus2 freemetas2
) metas
let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
let but = pf_concl gl in
let (sigma,hyp,c1,c2) =
let (env',c1) =
try
(* ~mod_delta:false to allow to mark occurences that must not be
rewritten simply by replacing them with let-defined definitions
in the context *)
w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
with
Pretype_errors.PretypeError _ ->
(* ~mod_delta:true to make Ring work (since it really
exploits conversion) *)
w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
in
let cl' = {cl with env = env' } in
let c2 = Clenv.clenv_nf_meta cl' c2 in
check_evar_map_of_evars_defs env' ;
env',(input_direction,Clenv.clenv_value cl'), c1, c2
in
try
let input_relation =
relation_class_that_matches_a_constr "Setoid_rewrite"
new_goals (Typing.mtype_of (pf_env gl) sigma (snd hyp)) in
let output_relation,output_direction,marked_but =
mark_occur gl ~new_goals c1 but input_relation input_direction in
let cic_output_direction = cic_direction_of_direction output_direction in
let if_output_relation_is_iff relation_in_Prop gl =
let th =
apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
cic_output_direction marked_but
in
let new_but = Termops.replace_term c1 c2 but in
let hyp1,hyp2,proj =
match output_direction with
Right2Left ->
new_but, but,
if relation_in_Prop then Lazy.force coq_proj1
else Lazy.force coq_proj1T
| Left2Right ->
but, new_but,
if relation_in_Prop then Lazy.force coq_proj2
else Lazy.force coq_proj2T
in
let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in
let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
let th' = mkApp (proj, [|impl2; impl1; th|]) in
Tactics.refine
(mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in
let if_output_relation_is_if gl =
let th =
apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
cic_output_direction marked_but
in
let new_but = Termops.replace_term c1 c2 but in
Tactics.refine
(mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
in
if output_relation = (Lazy.force coq_iffT_relation) then
if_output_relation_is_iff false gl
else if output_relation = (Lazy.force coq_iff_relation) then
if_output_relation_is_iff true gl
else
if_output_relation_is_if gl
with
Optimize ->
!general_rewrite (input_direction = Left2Right) (snd hyp) gl
let analyse_hypothesis gl c =
let ctype = pf_type_of gl c in
let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
let l,res = split_last_two (y::z) in x::l, res
| _ -> error "The term provided is not an equivalence" in
let others,(c1,c2) = split_last_two args in
eqclause,mkApp (equiv, Array.of_list others),c1,c2
let general_s_rewrite lft2rgt c ~new_goals gl =
let direction = if lft2rgt then Left2Right else Right2Left in
let eqclause,_,c1,c2 = analyse_hypothesis gl c in
match direction with
Left2Right -> relation_rewrite c1 c2 (direction,eqclause) ~new_goals gl
| Right2Left -> relation_rewrite c2 c1 (direction,eqclause) ~new_goals gl
let general_s_rewrite_in id lft2rgt c ~new_goals gl =
let _,_,c1,c2 = analyse_hypothesis gl c in
let hyp = pf_type_of gl (mkVar id) in
(* since we will actually rewrite in the opposite direction, we also need
to replace every occurrence of c2 (resp. c1) in hyp with something that
is convertible but not syntactically equal. To this aim we introduce a
let-in and then we will use the intro tactic to get rid of it *)
let let_in_abstract t in_t =
let t' = lift 1 t in
let in_t' = lift 1 in_t in
mkLetIn (Anonymous,t,pf_type_of gl t,subst_term t' in_t') in
let mangled_new_hyp,new_hyp =
if lft2rgt then
Termops.replace_term c1 c2 (let_in_abstract c2 hyp),
Termops.replace_term c1 c2 hyp
else
Termops.replace_term c2 c1 (let_in_abstract c1 hyp),
Termops.replace_term c2 c1 hyp
in
cut_replacing id new_hyp
(tclTHENLAST
(tclTHEN (change_in_concl None mangled_new_hyp)
(tclTHEN intro
(general_s_rewrite (not lft2rgt) c ~new_goals))))
gl
let setoid_replace relation c1 c2 ~new_goals gl =
try
let relation =
match relation with
Some rel ->
(try
match find_relation_class rel with
Relation sa -> sa
| Leibniz _ -> raise Optimize
with
Not_found ->
errorlabstrm "Setoid_rewrite"
(prterm rel ++ str " is not a registered relation."))
| None ->
match default_relation_for_carrier (pf_type_of gl c1) with
Relation sa -> sa
| Leibniz _ -> raise Optimize
in
let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in
let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in
let replace dir eq =
tclTHENS (assert_tac false Anonymous eq)
[onLastHyp (fun id ->
tclTHEN
(general_s_rewrite dir (mkVar id) ~new_goals)
(clear [id]));
Tacticals.tclIDTAC]
in
tclORELSE
(replace true eq_left_to_right) (replace false eq_right_to_left) gl
with
Optimize -> (!replace c1 c2) gl
let setoid_replace_in id relation c1 c2 ~new_goals gl =
let hyp = pf_type_of gl (mkVar id) in
let new_hyp = Termops.replace_term c1 c2 hyp in
cut_replacing id new_hyp
(fun exact -> tclTHENLASTn
(setoid_replace relation c2 c1 ~new_goals)
[| exact; tclIDTAC |]) gl
(* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
let setoid_reflexivity gl =
try
let relation_class =
relation_class_that_matches_a_constr "Setoid_reflexivity"
[] (pf_concl gl) in
match relation_class with
Leibniz _ -> assert false (* since [] is empty *)
| Relation rel ->
match rel.rel_refl with
None ->
errorlabstrm "Setoid_reflexivity"
(str "The relation " ++ prrelation rel ++ str " is not reflexive.")
| Some refl -> apply refl gl
with
Optimize -> reflexivity gl
let setoid_symmetry gl =
try
let relation_class =
relation_class_that_matches_a_constr "Setoid_symmetry"
[] (pf_concl gl) in
match relation_class with
Leibniz _ -> assert false (* since [] is empty *)
| Relation rel ->
match rel.rel_sym with
None ->
errorlabstrm "Setoid_symmetry"
(str "The relation " ++ prrelation rel ++ str " is not symmetric.")
| Some sym -> apply sym gl
with
Optimize -> symmetry gl
let setoid_symmetry_in id gl =
let new_hyp =
let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
mkApp (he, [| c2 ; c1 |])
in
cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
let setoid_transitivity c gl =
try
let relation_class =
relation_class_that_matches_a_constr "Setoid_transitivity"
[] (pf_concl gl) in
match relation_class with
Leibniz _ -> assert false (* since [] is empty *)
| Relation rel ->
let ctyp = pf_type_of gl c in
let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in
match rel'.rel_trans with
None ->
errorlabstrm "Setoid_transitivity"
(str "The relation " ++ prrelation rel ++ str " is not
transitive.")
| Some trans ->
let transty = nf_betaiota (pf_type_of gl trans) in
let argsrev, _ =
Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in
let binder =
match List.rev argsrev with
_::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2
| _ -> assert false
in
apply_with_bindings
(trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
with
Optimize -> transitivity c gl
;;
Tactics.register_setoid_reflexivity setoid_reflexivity;;
Tactics.register_setoid_symmetry setoid_symmetry;;
Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
Tactics.register_setoid_transitivity setoid_transitivity;;
- [Coq-Club] problem setoid, anoun
- Re: [Coq-Club] problem setoid,
Claudio Sacerdoti Coen
- Re: [Coq-Club] problem setoid, Claudio Sacerdoti Coen
- Re: [Coq-Club] problem setoid,
Claudio Sacerdoti Coen
Archive powered by MhonArc 2.6.16.