Mercurial > cpdt > repo

comparison src/Equality.v @ 199:cadeb49dc1ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix typo
author Adam Chlipala <adamc@hcoop.net>
date Mon, 01 Dec 2008 08:32:20 -0500
parents bc1f7d3687e7
children f05514cc6c0d
comparison
equal deleted inserted replaced
198:a35eaec19781 199:cadeb49dc1ef
23 23
24 (** * The Definitional Equality *) 24 (** * The Definitional Equality *)
25 25
26 (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's %\textit{%#<i>#definitional equality#</i>#%}%. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal. 26 (** We have seen many examples so far where proof goals follow "by computation." That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially. Exactly when this works and when it does not depends on the details of Coq's %\textit{%#<i>#definitional equality#</i>#%}%. This is an untyped binary relation appearing in the formal metatheory of CIC. CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal.
27 27
28 The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [1] when applied to [0]. *) 28 The [cbv] tactic will help us illustrate the rules of Coq's definitional equality. We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
29 29
30 Definition pred' (x : nat) := 30 Definition pred' (x : nat) :=
31 match x with 31 match x with
32 | O => O 32 | O => O
33 | S n' => let y := n' in y 33 | S n' => let y := n' in y