coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. -!-
- [Coq-Club] beginner's question, Robert Dockins
- Re: [Coq-Club] beginner's question, Stefano Zacchiroli
- Re: [Coq-Club] beginner's question, Brian Emre Aydemir
- Re: [Coq-Club] beginner's question, Houda Anoun
- [Coq-Club] Installing Coq for OCamo 3.08p1,
Robert M. Solovay
- Re: [Coq-Club] Installing Coq for OCamo 3.08p1, Florent Kirchner
Archive powered by MhonArc 2.6.16.