The Coq mailing list

[Ben Lerner <blerner AT cs.brown.edu>]

Hi,

(Apologies if this has been answered before; I couldn't find an answer 
in the list archives.)  I'm working through some examples from the 
Software Foundations book, and trying to gain familiarity with morphisms 
and setoid rewriting by converting some of them to use morphisms instead 
of applying lemmas directly.  And I've gotten stuck on morphisms that 
have preconditions, so to speak.  As a concrete example, suppose we have 
the language of constants and addition, where constants are the only 
values and with left-to-right small-step evaluation:

Inductive tm : Set :=
| C : nat -> tm
| P : tm -> tm -> tm.

Inductive value : tm -> Prop :=
| v_const : forall n, value (C n).

Inductive step : tm -> tm -> Prop :=
| ST_PlusNM : forall n m, step (P (C n) (C m)) (C (n + m))
| ST_Plus1 : forall t1 t1' t2, step t1 t1' -> step (P t1 t2) (P t1' t2)
| ST_Plus2 : forall t1 t2 t2', value t1 -> step t2 t2' -> step (P t1 t2) (P 
t1 t2').

Inductive stepmany : tm -> tm -> Prop :=
| SM_refl : forall t, stepmany t t
| SM_step : forall t1 t2 t3, step t1 t2 -> stepmany t2 t3 -> stepmany t1 t3.


It's straightforward to show that stepmany is a PreOrder (using Add 
Relation...).  It's equally easy to show that P is a morphism (using Add 
Morphism...) in its first argument with signature (stepmany ==> eq ==> 
stepmany).  Once I've gotten that far, I can solve the following by 
"rewrite H":

t1 : tm
t1' : tm
t2 : tm
H : stepmany t1 t1'
=============================
stepmany (P t1 t2) (P t1' t2)


But to show that P is a morphism in its second argument, I need the 
precondition that its first argument is a value.  Concretely, I can 
prove both the following instance declarations:

Instance Tm_plus_r1 (n : nat) : Proper (stepmany ==> stepmany) (P (C n)).
Instance Tm_plus_r2 (t : tm) : value t -> Proper (stepmany ==> stepmany) (P 
t).


But when I try to prove the following:

n : nat
t2 : tm
t2' : tm
H : stepmany t2 t2'
=============================
stepmany (P (C n) t2) (P (C n) t2')


Only the first instance allows me to use "rewrite H" successfully; the 
second gives an error about satisfying constraints.  I think the 
constraint at issue is

 ?5318==[n t2 t2' H (do_subrelation:=do_subrelation)
          |- Proper (stepmany ==> ?5317) (P (C n))] (internal placeholder)


Which makes sense; Tm_plus_r2 isn't defined for (P t1) for all t1; it's 
defined conditionally, for t1 that are values.  But Tm_plus_r2 seems far 
easier to generalize to larger languages; I wouldn't want to have to 
prove the same morphism once for every value form in my language...  Is 
there a way to write some form of Add Morphism (or Add Parametric 
Morphism) that would let me define the second instance above, allow me 
to "rewrite H", and generate the subgoal of proving "value t1"?

Thanks,
Ben Lerner