The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I am new to coq and I'm trying to get my feet wet by doing some proofs
from _Types and Programming Languages_ by Pierce.  I have a need to
define a set of evaluation rules on terms.  The evaluation relation is
defined in the book as "the smallest binary relation on terms
satisfying... the rules."

My question is, how is the best way to go about defining "the smallest
binary relation such that..." in coq?  A bungled attempt is given below.
It could work in theory, but defining the axioms which correctly exclude
tuples from the relation looks like it would be a real pain if the
relation gets much more complicated (esp since I haven't gotten this one
right yet).  Surely there is a better way?

Many thanks.



code follows
-----------------

Section TaPL1.

Inductive term : Set :=
  | True : term
  | False : term
  | If : term -> term -> term -> term
.

Definition isValue (t:term) : bool :=
  match t with
  |  True  => true
  |  False => true
  |  If x y z => false
  end
.

Variable TermReduce : term -> term -> Prop.

Notation "A --> B" := (TermReduce A B) (at level 40, left
associativity).

Axiom EIfTrue  : forall (x y:term),   (If True x y) --> x.
Axiom EIfFalse : forall (x y:term),   (If False x y) --> y.
Axiom EIf      : forall (a b x y:term), (a --> b) -> (If a x y) --> (If
b x y).

(* not quite correct... *)
Axiom ECant : forall (p q:term), (forall (x y z:term), ~(p=If x y z)) ->
~(p --> q).
       

(* first thing I'd like to prove *)
Theorem DeterminacyOfEvaluation :
     forall (t t1 t2:term), (t --> t1) /\ (t --> t2) -> t1 = t2.


End TaPL1.