Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 122 insertions, 71 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index e1de9ee9..9b848551 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,14 +7,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based relations, tactics and standard instances.
+(** *  Typeclass-based relations, tactics and standard instances
+
    This is the basic theory needed to formalize morphisms and setoids.
- 
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
@@ -42,16 +44,18 @@ Unset Strict Implicit.
 Class Reflexive {A} (R : relation A) :=
   reflexivity : forall x, R x x.
 
-Class Irreflexive {A} (R : relation A) := 
-  irreflexivity :> Reflexive (complement R).
+Class Irreflexive {A} (R : relation A) :=
+  irreflexivity : Reflexive (complement R).
 
-Class Symmetric {A} (R : relation A) := 
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+
+Class Symmetric {A} (R : relation A) :=
   symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric {A} (R : relation A) := 
+Class Asymmetric {A} (R : relation A) :=
   asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive {A} (R : relation A) := 
+Class Transitive {A} (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
 Hint Resolve @irreflexivity : ord.
@@ -61,7 +65,7 @@ Unset Implicit Arguments.
 (** A HintDb for relations. *)
 
 Ltac solve_relation :=
-  match goal with 
+  match goal with
   | [ |- ?R ?x ?x ] => reflexivity
   | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
   end.
@@ -70,34 +74,39 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
-Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
-  reflexivity (R:=R).
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
-  irreflexivity (R:=R).
+Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
+Proof. tauto. Qed.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
 
-Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
+Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
+  irreflexivity (R:=R).
 
-  Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
+Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
+  fun x y H => symmetry (R:=R) H.
 
-Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
-  
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
+Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
+  fun x y H H' => asymmetry (R:=R) H H'.
 
-Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
+Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
+  fun x y z H H' => transitivity (R:=R) H' H.
 
-  Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
 
-Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
+Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
    : Irreflexive (complement R).
+Proof. firstorder. Qed.
 
-  Next Obligation. 
-  Proof. firstorder. Qed.
-
-Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Proof. firstorder. Qed.
 
-  Next Obligation.
-  Proof. firstorder. Qed.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances.
 
 (** * Standard instances. *)
 
@@ -117,7 +126,7 @@ Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
 
 Ltac reduce := reduce_goal.
 
-Tactic Notation "apply" "*" constr(t) := 
+Tactic Notation "apply" "*" constr(t) :=
   first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
     refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
 
@@ -125,7 +134,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligation_tactic ::= simpl_relation.
+Local Obligation Tactic := simpl_relation.
 
 (** Logical implication. *)
 
@@ -174,13 +183,14 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
 Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
-  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
+  antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
 
-Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
-  ! Antisymmetric A eqA (flip R).
+Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
+  Antisymmetric A eqA (flip R).
+Proof. firstorder. Qed.
 
 (** Leibinz equality [eq] is an equivalence relation.
-   The instance has low priority as it is always applicable 
+   The instance has low priority as it is always applicable
    if only the type is constrained. *)
 
 Program Instance eq_equivalence : Equivalence (@eq A) | 10.
@@ -193,26 +203,24 @@ Program Instance iff_equivalence : Equivalence iff.
    The resulting theory can be applied to homogeneous binary relations but also to
    arbitrary n-ary predicates. *)
 
-Require Import Coq.Lists.List.
+Local Open Scope list_scope.
 
 (* Notation " [ ] " := nil : list_scope. *)
 (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
 
-(* Open Local Scope list_scope. *)
-
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
-Fixpoint arrows (l : list Type) (r : Type) : Type := 
-  match l with 
+Fixpoint arrows (l : list Type) (r : Type) : Type :=
+  match l with
     | nil => r
     | A :: l' => A -> arrows l' r
   end.
 
 (** We can define abbreviations for operation and relation types based on [arrows]. *)
 
-Definition unary_operation A := arrows (cons A nil) A.
-Definition binary_operation A := arrows (cons A (cons A nil)) A.
-Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
+Definition unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
 
 (** We define n-ary [predicate]s as functions into [Prop]. *)
 
@@ -220,13 +228,13 @@ Notation predicate l := (arrows l Prop).
 
 (** Unary predicates, or sets. *)
 
-Definition unary_predicate A := predicate (cons A nil).
+Definition unary_predicate A := predicate (A::nil).
 
 (** Homogeneous binary relations, equivalent to [relation A]. *)
 
-Definition binary_relation A := predicate (cons A (cons A nil)).
+Definition binary_relation A := predicate (A::A::nil).
 
-(** We can close a predicate by universal or existential quantification. *) 
+(** We can close a predicate by universal or existential quantification. *)
 
 Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
   match l with
@@ -240,7 +248,7 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
     | A :: tl => fun f => exists x : A, predicate_exists tl (f x)
   end.
 
-(** Pointwise extension of a binary operation on [T] to a binary operation 
+(** Pointwise extension of a binary operation on [T] to a binary operation
    on functions whose codomain is [T].
    For an operator on [Prop] this lifts the operator to a binary operation. *)
 
@@ -248,7 +256,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
   (l : list Type) : binary_operation (arrows l T) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       fun x => pointwise_extension op tl (R x) (R' x)
   end.
 
@@ -257,7 +265,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
 Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       forall x, pointwise_lifting op tl (R x) (R' x)
   end.
 
@@ -289,7 +297,7 @@ Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_
 
 (** The always [True] and always [False] predicates. *)
 
-Fixpoint true_predicate {l : list Type} : predicate l := 
+Fixpoint true_predicate {l : list Type} : predicate l :=
   match l with
     | nil => True
     | A :: tl => fun _ => @true_predicate tl
@@ -306,17 +314,13 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence :
-  Equivalence (@predicate_equivalence l).
-
+Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-  
   Next Obligation.
     fold pointwise_lifting.
     induction l. firstorder.
@@ -326,59 +330,59 @@ Program Instance predicate_equivalence_equivalence :
 
 Program Instance predicate_implication_preorder :
   PreOrder (@predicate_implication l).
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l. firstorder.
-    unfold predicate_implication in *. simpl in *. 
+    unfold predicate_implication in *. simpl in *.
     intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
-(** We define the various operations which define the algebra on binary relations, 
+(** We define the various operations which define the algebra on binary relations,
    from the general ones. *)
 
 Definition relation_equivalence {A : Type} : relation (relation A) :=
-  @predicate_equivalence (cons _ (cons _ nil)).
+  @predicate_equivalence (_::_::nil).
 
 Class subrelation {A:Type} (R R' : relation A) : Prop :=
-  is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+  is_subrelation : @predicate_implication (A::A::nil) R R'.
 
 Implicit Arguments subrelation [[A]].
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_intersection (cons A (cons A nil)) R R'.
+  @predicate_intersection (A::A::nil) R R'.
 
 Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_union (cons A (cons A nil)) R R'.
+  @predicate_union (A::A::nil) R R'.
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
+Set Automatic Introduction.
+
 Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (@relation_equivalence A).
-Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
 
-Instance relation_implication_preorder : PreOrder (@subrelation A).
-Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
-   We give an equivalent definition, up-to an equivalence relation 
+   We give an equivalent definition, up-to an equivalence relation
    on the carrier. *)
 
 Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
-(** The equivalence proof is sufficient for proving that [R] must be a morphism 
+(** The equivalence proof is sufficient for proving that [R] must be a morphism
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. 
-  pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal.
+  pose proof partial_order_equivalence as poe. do 3 red in poe.
   apply <- poe. firstorder.
 Qed.
 
@@ -392,5 +396,52 @@ Program Instance subrelation_partial_order :
     unfold relation_equivalence in *. firstorder.
   Qed.
 
-Typeclasses Opaque arrows predicate_implication predicate_equivalence 
+Typeclasses Opaque arrows predicate_implication predicate_equivalence
   relation_equivalence pointwise_lifting.
+
+(** Rewrite relation on a given support: declares a relation as a rewrite
+   relation for use by the generalized rewriting tactic.
+   It helps choosing if a rewrite should be handled
+   by the generalized or the regular rewriting tactic using leibniz equality.
+   Users can declare an [RewriteRelation A RA] anywhere to declare default
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class RewriteRelation {A : Type} (RA : relation A).
+
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+Instance: RewriteRelation (@relation_equivalence A).
+
+(** Any [Equivalence] declared in the context is automatically considered
+   a rewrite relation. *)
+
+Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
+
+(** Strict Order *)
+
+Class StrictOrder {A : Type} (R : relation A) := {
+  StrictOrder_Irreflexive :> Irreflexive R ;
+  StrictOrder_Transitive :> Transitive R
+}.
+
+Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+Proof. firstorder. Qed.
+
+(** Inversing a [StrictOrder] gives another [StrictOrder] *)
+
+Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
+Proof. firstorder. Qed.
+
+(** Same for [PartialOrder]. *)
+
+Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances.
+Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances.
+
+Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances.