Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Question on morphisms and "conditional" setoid rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question on morphisms and "conditional" setoid rewriting


Chronological Thread 
  • From: Ben Lerner <blerner AT cs.brown.edu>
  • To: Coq club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Question on morphisms and "conditional" setoid rewriting
  • Date: Thu, 14 Mar 2013 13:52:52 -0400

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



Archive powered by MHonArc 2.6.18.

Top of Page