The Coq mailing list

["Robert" <robdockins AT fastmail.fm>]

(* Friends,

   I'm trying to develop a theory of preorders
   and monotone functions.  I'd like to be able to do
   rewriting up to equivalance, but I'm having some problems
   getting it to work.  In some cases rewriting works as
   expected, but in others I get error messages about not
   being able to solve constraints.  I don't understand what
   is causing the error or how to fix it.  Can anyone
   enlighten me?

   Most of this file is just setup for the problem, which
   appears near the end.

   I'm using Coq 8.2 (CoqIde, Windows build).
*)

Require Import Setoid.

Record preord :=
  { po :> Type
  ; ord : po -> po -> Prop
  ; ord_refl : forall x, ord x x
  ; ord_trans : forall x y z, ord x y -> ord y z -> ord x z
  }.

Hint Resolve ord_refl ord_trans.

Definition equiv {A:preord} (x y:A) := ord A x y /\ ord A y x.
Infix "==" := equiv (at level 75, no associativity).

Lemma equiv_refl : forall (A:preord) (x:A), x == x. 
Proof.
  intros; split; auto.
Qed.

Lemma equiv_sym : forall (A:preord) (x y:A), x == y -> y == x.
Proof.
  unfold equiv; intuition.
Qed.

Lemma equiv_trans : forall (A:preord) (x y z:A), x == y -> y == z -> x
== z.
Proof.
  unfold equiv; intuition eauto.
Qed.

Hint Resolve equiv_refl equiv_trans.

Add Parametric Relation (p:preord) : (po p) (ord p)
  reflexivity proved by (ord_refl p)
  transitivity proved by (ord_trans p)
  as po_ord_relation.

Add Parametric Relation (p:preord) : (po p) (@equiv p)
  reflexivity proved by (equiv_refl p)
  symmetry proved by (equiv_sym p)
  transitivity proved by (equiv_trans p)
  as po_equiv_relation.

Instance equiv_ord_subrelation (p:preord)
  : subrelation (@equiv p) (@ord p).
do 3 (intros; hnf).
unfold equiv; intuition.
Qed.

Record mono_func (A B:preord) :=
  { hfun :>  A -> B
  ; hfun_mono : forall x x',
       ord A x x' -> ord B (hfun x) (hfun x')
  }.

Definition pointwise_ord {A B:preord} (f g:mono_func A B) :=
  forall x, ord B (f x) (g x). 

Definition hom (A B:preord) :=
  Build_preord (mono_func A B) (pointwise_ord)
      (* refl *)  (fun f x => ord_refl B (f x))
      (* trans *) (fun f g h H1 H2 x => ord_trans B (f x) (g x) (h x)
      (H1 x) (H2 x)).

Definition compose {A B C:preord} (f:hom B C) (g:hom A B) : hom A C :=
  Build_mono_func A C (fun x => f (g x)) 
     (fun x x' H => hfun_mono B C f (g x) (g x') (hfun_mono A B g x x'
     H)).
Infix "oo" := compose (at level 55, right associativity).

Lemma compose_assoc : forall A B C D (f:hom C D) (g:hom B C) (h:hom A
B), 
  f oo (g oo h) == (f oo g) oo h.
Proof.
  intros; split; simpl; hnf; intros; simpl; auto.
Qed.

Add Parametric Morphism (A B:preord) : (@hfun A B)
  with signature (ord (hom A B)) ==> (ord A) ==> (ord B)
  as hfun_ord_morphism.
simpl; intros.
apply ord_trans with (hfun A B y x0).
apply H.
apply hfun_mono; auto.
Qed.

Add Parametric Morphism (A B:preord) : (@hfun A B)
  with signature (@equiv (hom A B)) ==> (@equiv A) ==> (@equiv B)
  as hfun_equiv_morphism.
simpl; intros.
apply equiv_trans with (hfun A B y x0).
split.
apply H.
destruct H.
apply H1.
split; apply hfun_mono; destruct H0; auto.
Qed. 

(* Here is an example demonstrating the sort of problems
   I'm having.
*)
Goal forall (A B C D:preord) (f:hom C D) (g:hom B C) (h:hom A B) (x:A),
  ((f oo g oo h) x) == (((f oo g) oo h) x).
Proof.
  intros.
rewrite compose_assoc.
(*
This rewrite doesn't work, and gives me an unintelligible
error about unsatisfied constraints.  I don't know how
to make it happy.

The following, however, does work.  I'd really like
to get the rewriting to work so I don't have to manually
apply morphism proofs.
*)
  apply hfun_equiv_morphism.
  apply compose_assoc.
  apply equiv_refl.
Qed.

-- 
  Robert
  
robdockins AT fastmail.fm