The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi,
You can use a  predicate  defined inductively
I join a file containing the proof of the lemmas bellow
Hope it helps

Houda

> 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.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>  


--
==============================
| /\    Houda ANOUN     /\   |
|  -       LaBRI        -    |
| 351 Cours de la libération |
|      33405 Talence         |
|phone  : 0540002489         |
|e-mail : 
anoun AT labri.fr
     |
|web    : www.labri.fr/~anoun|
==============================


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
.



Inductive reduce :term -> term -> Prop:=
| EIfTrue  : forall (x y:term),  reduce (If True x y) x
| EIfFalse : forall (x y:term), reduce (If False x y)x
| EIf      : forall (a b x y:term), reduce a b ->
                                    reduce (If a x y) (If
b x y).


Lemma ECant : forall (p q:term), (forall (x y z:term), ~(p=If x y z)) ->
~(reduce p q).
 intros.
 red in |- *.
 intro H1.
 inversion H1.
 rewrite <- H0 in H.
 elim (H True x y).
 auto.
 rewrite <- H0 in H.
 elim (H False x y); auto.
 rewrite <- H2 in H; elim (H a x y); auto.
Qed.

Theorem DeterminacyOfEvaluation :
     forall (t t1 t2:term), (reduce t t1) /\ (reduce t t2) -> t1 = t2.

 intros.
 elim H; clear H.
 intro H; generalize t2.
 elim H.
 intros.
 inversion H0.
 auto.
 inversion H5.
 intros.
 inversion H0.
 auto.
 inversion H5.
 intros.
 inversion H2.
 rewrite <- H4 in H0; inversion H0.
 rewrite <- H4 in H0; inversion H0.
 rewrite (H1 b0 H7).
 auto.
Qed.

End  TaPL1.