Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] beginner's question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] beginner's question


chronological Thread 
  • From: Stefano Zacchiroli <zack AT bononia.it>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] beginner's question
  • Date: Sat, 8 Jan 2005 11:51:29 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Fri, Jan 07, 2005 at 10:01:13PM -0500, Robert Dockins wrote:
> 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.

I would use an inductive predicate for that.

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

This is my development for your example (I changed name for the terms
since I don't like clashing with True and False built in proposition):

  Inductive term: Set :=
    | tTrue: term
    | tFalse: term
    | tIf: term -> term -> term -> term.

  Inductive value: term -> Prop :=
    | valueT: value tTrue
    | valueF: value tFalse.

  Inductive reduce: term -> term -> Prop :=
    | reduceT: forall (t1 t2:term), reduce (tIf tTrue t1 t2) t1
    | reduceF: forall (t1 t2:term), reduce (tIf tFalse t1 t2) t2.
      
  Theorem DeterminacyOfEvaluation:
    forall (t t1 t2:term),
      reduce t t1 /\ reduce t t2 -> t1 = t2.
    induction t;
      try (intros t1 t2 H; elim H; intros H1 _; inversion H1; fail).
    intros t4 t5 H; elim H; intros H1 H2; clear H.  
    inversion H1; inversion H2;
      (rewrite <- H9; rewrite <- H5; trivial ||
        rewrite <- H6 in H0; discriminate H0).
  Qed.

Maybe there's a simpler proof ...

-- 
Stefano Zacchiroli -*- Computer Science PhD student @ Uny Bologna, Italy
zack@{cs.unibo.it,debian.org,bononia.it}
 -%- http://www.bononia.it/zack/
If there's any real truth it's that the entire multidimensional infinity
of the Universe is almost certainly being run by a bunch of maniacs. -!-




Archive powered by MhonArc 2.6.16.

Top of Page