Library Coq.Setoids.Setoid
Require Export Relation_Definitions.
Set Implicit Arguments.
Inductive X_Relation_Class (X: Type) : Type :=
SymmetricReflexive :
forall A Aeq, symmetric A Aeq -> reflexive _ Aeq -> X_Relation_Class X
| AsymmetricReflexive : X -> forall A Aeq, reflexive A Aeq -> X_Relation_Class X
| SymmetricAreflexive : forall A Aeq, symmetric A Aeq -> X_Relation_Class X
| AsymmetricAreflexive : X -> forall A (Aeq : relation 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, symmetric A Aeq -> reflexive _ Aeq -> Reflexive_Relation_Class
| RAsymmetric :
forall A Aeq, reflexive A Aeq -> Reflexive_Relation_Class
| RLeibniz : Type -> Reflexive_Relation_Class.
Inductive Areflexive_Relation_Class : Type :=
| ASymmetric : forall A Aeq, symmetric A Aeq -> Areflexive_Relation_Class
| AAsymmetric : forall A (Aeq : relation 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 -> Prop.
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
| necons : 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), Prop.
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 }.
The
iff relation class
Definition Iff_Relation_Class : Relation_Class.
eapply (@SymmetricReflexive unit _ iff).
exact iff_sym.
exact iff_refl.
Defined.
The
impl relation class
Definition impl (A B: Prop) := A -> B.
Theorem impl_refl: reflexive _ impl.
Proof.
hnf; unfold impl; tauto.
Qed.
Definition Impl_Relation_Class : Relation_Class.
eapply (@AsymmetricReflexive unit tt _ impl).
exact impl_refl.
Defined.
Every function is a morphism from Leibniz+ to Leibniz
Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
induction 1.
exact (singl (Leibniz _ a)).
exact (necons (Leibniz _ a) IHX).
Defined.
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.
Every predicate is a 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.
Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
let ASetoidClass := SymmetricAreflexive _ sym in
(Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_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: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
(trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
(Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_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: relation A)(trans: transitive _ Aeq),
let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
(Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; unfold impl; eauto.
Defined.
Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq),
let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
let ASetoidClass2 := AsymmetricReflexive Covariant refl in
(Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
intros.
exists Aeq.
unfold make_compatibility_goal; simpl; unfold impl; eauto.
Defined.
iff as a relation
Add Relation Prop iff
reflexivity proved by iff_refl
symmetry proved by iff_sym
transitivity proved by iff_trans
as iff_relation.
impl as a relation
Theorem impl_trans: transitive _ impl.
Proof.
hnf; unfold impl; tauto.
Qed.
Add Relation Prop impl
reflexivity proved by impl_refl
transitivity proved by impl_trans
as impl_relation.
impl is a morphism
Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
Proof.
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.
Proof.
tauto.
Qed.
not is a morphism
Add Morphism not with signature iff ==> iff as Not_Morphism.
Proof.
tauto.
Qed.
The same examples on
impl
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
Proof.
unfold impl; tauto.
Qed.
Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
Proof.
unfold impl; tauto.
Qed.
Add Morphism not with signature impl --> impl as Not_Morphism2.
Proof.
unfold impl; tauto.
Qed.
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.
Proof.
destruct dir; reflexivity.
Qed.
Inductive check_if_variance_is_respected :
option variance -> rewrite_direction -> rewrite_direction -> Prop :=
| 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'' (necons 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 (prod (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.
exact (opposite_direction dir).
exact dir.
Defined.
Definition directed_relation_of_relation_class:
forall dir (R: Relation_Class),
carrier_of_relation_class R -> carrier_of_relation_class R -> Prop.
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 -> Prop.
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 -> Prop.
induction In.
simpl.
exact (directed_relation_of_argument_class (get_rewrite_direction dir a) a).
simpl; intros.
destruct X; destruct X0.
apply and.
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.
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.
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).
Proof.
induction In; intros.
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.
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.
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)).
Proof.
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 H0.
apply apply_morphism_compatibility_Right2Left.
exact (Compat m).
exact H0.
exact H.
unfold interp, Morphism_Context_rect2.
destruct S; destruct dir'0; simpl; (apply r || reflexivity).
destruct dir'0; exact r.
destruct S; unfold directed_relation_of_argument_class; simpl in H0 |- *;
unfold get_rewrite_direction; simpl.
destruct dir'0; destruct dir'';
(exact H0 ||
unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
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 ||
unfold directed_relation_of_argument_class; simpl; apply s; exact H0).
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.
For backwark compatibility
Record Setoid_Theory (A: Type) (Aeq: relation A) : Prop :=
{ 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 }.
Implicit Arguments Setoid_Theory [].
Implicit Arguments Seq_refl [].
Implicit Arguments Seq_sym [].
Implicit Arguments Seq_trans [].
Some tactics for manipulating Setoid Theory not officially
declared as Setoid.
Ltac trans_st x := match goal with
| H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
apply (Seq_trans _ _ H) with x; auto
end.
Ltac sym_st := match goal with
| H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
apply (Seq_sym _ _ H); auto
end.
Ltac refl_st := match goal with
| H : Setoid_Theory _ ?eqA |- ?eqA _ _ =>
apply (Seq_refl _ _ H); auto
end.
Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A).
Proof.
constructor; congruence.
Qed.