The Coq mailing list

[Brian Emre Aydemir <baydemir AT cis.upenn.edu>]

On Jan 7, 2005, at 22:01, Robert Dockins wrote:

> 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.  [...]  My question 
> is, how is the best way to go about defining "the smallest binary 
> relation such that..." in coq?

Relations can be defined inductively much as you defined the set of 
terms inductively.  For example, the following code snippet defines the 
evaluation relation.

==== BEGIN CODE ====

Reserved Notation "A --> B" (at level 40, left associativity).

Inductive evalsTo : term -> term -> Prop :=
  | EIfTrue:  forall (x y:term), (If True x y) --> x
  | EIfFalse: forall (x y:term), (If False x y) --> y
  | EIf: forall (a b x y:term),
      (a --> b) ->
      ((If a x y) --> (If b x y))
where "A --> B" := (evalsTo A B).

==== END CODE ====

This seems to work pretty well in practice.  In particular, you now get 
an induction principle for the evaluation relation.

Cheers,
Brian

--
Brian Emre Aydemir
http://www.cis.upenn.edu/~baydemir/