Add new files theories/Program/Basics.v and theories/Classes/Relations.v

for basic functional programming and relation
definitions respectively. 
Classes.Relations also includes the definition of Morphism
and instances for the standard morphisms and relations (eq, iff, impl,
inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic
has been reimplemented on top of these definitions, hence it doesn't
require a setoid implementation anymore. It also generates obligations
for missing reflexivity proofs, like the current setoid_rewrite. It has
not been tested on large examples but it should handle directions and
occurences. Works with in if no obligations are generated at this time.
What's missing is being able to rewrite by a lemma instead of a simple
hypothesis with no premises.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 66 insertions, 256 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f61b4a415..78e53aa01 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -22,72 +22,48 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** We first define setoids on a carrier, it amounts to an equivalence relation. 
-   Now [equiv] is overloaded for every [Setoid].
-*)
+Require Export Coq.Classes.Relations.
 
-Require Export Coq.Relations.Relations.
+(** A setoid wraps an equivalence. *)
 
-Class Setoid (carrier : Type) (equiv : relation carrier) :=
-  equiv_prf : equivalence carrier equiv.
+Class Setoid A :=
+  equiv : relation A ;
+  setoid_equiv :> Equivalence A equiv.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+(** Shortcuts to make proof search easier. *)
 
-Definition equiv [ Setoid A R ] : _ := R.
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
-Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
+(** Standard setoids. *)
 
-Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
-Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
-Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
+Program Instance eq_setoid : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
 
-Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =/= y -> y =/= x.
-Proof.
-  intros ; red ; intros.
-  apply equiv_sym in H0...
-  apply (H H0).
-Qed.
-
-(** Tactics to do some progress on the goal, called by the user. *)
-
-Ltac do_setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
-    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
-    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
-    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
-  end.
+Program Instance iff_setoid : Setoid Prop :=
+  equiv := iff ; setoid_equiv := iff_equivalence.
 
-Ltac refl := do_setoid_refl.
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
-Ltac do_setoid_sym := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- not (@equiv ?A ?R ?s ?X ?Y) ] => apply (nequiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
-  end.
+(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
+(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
 
-Ltac sym := do_setoid_sym.
+Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Ltac do_setoid_trans Y := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
-  end.
+Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
 
-Ltac trans y := do_setoid_trans y.
+Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
+Proof with auto.
+  intros ; red ; intros.
+  apply H.
+  sym...
+Qed.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -106,66 +82,24 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-(** Tactics to immediately solve the goal without user help. *)
-
-Ltac setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ H : ?X =/= ?X |- _ ] => elim H ; setoid_refl
-  end.
-
-Ltac setoid_sym := 
-  match goal with
-    | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H)
-    | [ H : ?X =/= ?Y |- ?Y =/= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
-  end.
-
-Ltac setoid_trans := 
-  match goal with
-    | [ H : ?X == ?Y, H' : ?Y == ?Z |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z) H H')
-  end.
-
-(** To immediatly solve a goal on setoid equality. *)
-
-Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans.
-
 Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(z == y) by setoid_sym.
-  assert(x == y) by setoid_trans.
+  assert(z == y) by relation_sym.
+  assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
 Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y == x) by setoid_sym.
-  assert(y == z) by setoid_trans.
+  assert(y == x) by relation_sym.
+  assert(y == z) by relation_trans.
   contradiction.
 Qed.
 
 Open Scope type_scope.
 
-(** Need to fix fresh to not fail if some arguments are not identifiers. *)
-(* Ltac setoid_sat ::= *)
-(*   match goal with *)
-(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
-(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
-(*   end. *)
-
-Ltac setoid_sat :=
-  match goal with
-    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
-    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
-  end.
-
 Ltac setoid_simplify_one :=
   match goal with
     | [ H : ?x == ?x |- _ ] => clear H
@@ -175,192 +109,68 @@ Ltac setoid_simplify_one :=
 
 Ltac setoid_simplify := repeat setoid_simplify_one.
 
-Ltac setoid_saturate := repeat setoid_sat.
-
 Ltac setoidify_tac :=
   match goal with
-    | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Setoid ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+    | [ s : Setoid ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Setoid ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
   end.
 
 Ltac setoidify := repeat setoidify_tac.
 
-Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] 
-  (m : a -> b) : Prop :=
-  forall x y, eqa x y -> eqb (m x) (m y).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => 
-  Morphism (m : a -> b) :=
-  respect : respectful m.
-
-(** Here we build a setoid instance for functions which relates respectful ones only. *)
-
-Definition respecting [ Setoid a R, Setoid b R' ] : Type := 
-  { morph : a -> b | respectful morph }.
-
-Ltac obligations_tactic ::= try red ; program_simpl ; try tauto.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => 
-  arrow_setoid : 
-  Setoid ({ morph : a -> b | respectful morph })
-
-  (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-
-  Next Obligation.
-  Proof.
-    trans (y x0) ; eauto.
-    apply H.
-    refl.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    sym ; apply H.
-    sym ; auto.
-  Qed.
-
-(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
-   some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
-
-Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ]
-  (m : a -> b -> c) : Prop :=
-  forall x y, eqa x y -> 
-    forall z w, eqb z w -> eqc (m x z) (m y w).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => 
-  BinaryMorphism (m : a -> b -> c) :=
-  respect2 : binary_respectful m.
-
-Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ]
-  (m : a -> b -> c -> d) : Prop :=
-  forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => 
-  TernaryMorphism (m : a -> b -> c -> d) :=
-  respect3 : ternary_respectful m.
-
-(** Definition of the usual morphisms in [Prop]. *)
-
-Program Instance iff_setoid : Setoid Prop iff :=
-  equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
-
-Program Instance not_morphism : Morphism Prop iff Prop iff not.
-
-Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
-
-(* We make the setoids implicit, they're always [iff] *)
-
-Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]].
-
-Program Instance or_morphism : ? BinaryMorphism or.
-
-Definition impl (A B : Prop) := A -> B.
-
-Program Instance impl_morphism : ? BinaryMorphism impl.
-
-Next Obligation.
-Proof.
-  unfold impl. tauto.
-Qed.
-
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
-Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R.
+Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
+  trans_sym_morphism.
 
-Next Obligation.
-Proof with auto.
-  split ; intros.
-  trans x. sym... trans z...
-  trans y... trans w... sym...
-Qed.
-  
-Definition iff_morphism : BinaryMorphism iff := setoid_morphism.
+(** Add this very useful instance in the database. *)
 
-Existing Instance iff_morphism.
+Implicit Arguments setoid_morphism [[!sa]].
+Existing Instance setoid_morphism.
 
-Implicit Arguments eq [[A]].
+Definition type_eq : relation Type :=
+  fun x y => x = y.
 
-Program Instance eq_setoid : Setoid A eq :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+Program Instance type_equivalence : Equivalence Type type_eq.
 
-Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq.
+  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
 
-Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m.
+Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Implicit Arguments arrow_morphism [[A] [B] [C]].
+Ltac obligations_tactic ::= morphism_tac.
 
-Program Instance type_setoid : Setoid Type (fun x y => x = y) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+(** These are morphisms used to rewrite at the top level of a proof, 
+   using [iff_impl_id_morphism] if the proof is in [Prop] and
+   [eq_arrow_id_morphism] if it is in Type. *)
 
-Lemma setoid_subst : forall (x y : Type), x == y -> x -> y.
-Proof.
-  intros.
-  rewrite <- H.
-  apply X.
-Qed.
+Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y.
-Proof.
-  intros.
-  clrewrite <- H.
-  apply H0.
-Qed.
+Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
 
-Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
-  mg : ? Morphism sb sc g, mf : ? Morphism sa sb f ] => 
-  compose_morphism : ? Morphism sa sc (fun x => g (f x)).
+(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
+    
 
-Next Obligation.
-Proof.
-  apply (respect (m0:=mg)).
-  apply (respect (m0:=mf)).
-  assumption.
-Qed.
+(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)
+(*   compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
+
+(* Next Obligation. *)
+(* Proof. *)
+(*   apply (respect (m0:=mg)). *)
+(*   apply (respect (m0:=mf)). *)
+(*   assumption. *)
+(* Qed. *)
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-Class PartialSetoid (carrier : Type) (equiv : relation carrier) :=
-  pequiv_prf : PER carrier equiv.
+Class PartialSetoid (carrier : Type) :=
+  pequiv : relation carrier ;
+  pequiv_prf :> PER carrier pequiv.
 
 (** Overloaded notation for partial setoid equivalence. *)
 
-Definition pequiv [ PartialSetoid A R ] : _ := R.
-
 Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
-Definition pequiv_sym [ s : PartialSetoid A R ] : forall x y : A, R x y -> R y x := per_sym _ _ pequiv_prf.
-Definition pequiv_trans [ s : PartialSetoid A R ] : forall x y z : A, R x y -> R y z -> R x z := per_trans _ _ pequiv_prf.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_partial_setoid : 
-  PartialSetoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  pequiv_prf := Build_PER _ _ _ _.
-
-Next Obligation.
-Proof.
-  sym.
-  apply H.
-  sym ; assumption.
-Qed.
-
-Next Obligation.
-Proof.
-  trans (y x0).
-  apply H ; auto.
-  trans y0 ; auto.
-  sym ; auto.
-  apply H0 ; auto.
-Qed.
-
-(** The following is not definable. *)
-(*
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
-  Setoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-*)
-
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.