Mercurial > cpdt > repo

comparison src/Predicates.v @ 426:5f25705a10ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 18:10:26 -0400
parents 10a6b5414551
children 393b8ed99c2f
comparison
equal deleted inserted replaced
425:6ed5ee4845e4 426:5f25705a10ea
23 Inductive sum := . 23 Inductive sum := .
24 Inductive prod := . 24 Inductive prod := .
25 Inductive and := conj. 25 Inductive and := conj.
26 Inductive or := or_introl | or_intror. 26 Inductive or := or_introl | or_intror.
27 Inductive ex := ex_intro. 27 Inductive ex := ex_intro.
28 Inductive eq := refl_equal. 28 Inductive eq := eq_refl.
29 Reset unit. 29 Reset unit.
30 (* end thide *) 30 (* end thide *)
31 (* end hide *) 31 (* end hide *)
32 32
33 (** %\chapter{Inductive Predicates}% *) 33 (** %\chapter{Inductive Predicates}% *)
464 464
465 For instance, our definition [isZero] makes the predicate provable only when the argument is [0]. We can see that the concept of equality is somehow implicit in the inductive definition mechanism. The way this is accomplished is similar to the way that logic variables are used in %\index{Prolog}%Prolog, and it is a very powerful mechanism that forms a foundation for formalizing all of mathematics. In fact, though it is natural to think of inductive types as folding in the functionality of equality, in Coq, the true situation is reversed, with equality defined as just another inductive type!%\index{Gallina terms!eq}\index{Gallina terms!refl\_equal}% *) 465 For instance, our definition [isZero] makes the predicate provable only when the argument is [0]. We can see that the concept of equality is somehow implicit in the inductive definition mechanism. The way this is accomplished is similar to the way that logic variables are used in %\index{Prolog}%Prolog, and it is a very powerful mechanism that forms a foundation for formalizing all of mathematics. In fact, though it is natural to think of inductive types as folding in the functionality of equality, in Coq, the true situation is reversed, with equality defined as just another inductive type!%\index{Gallina terms!eq}\index{Gallina terms!refl\_equal}% *)
466 466
467 Print eq. 467 Print eq.
468 (** [[ 468 (** [[
469 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x 469 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
470 470
471 ]] 471 ]]
472 472
473 Behind the scenes, uses of infix [=] are expanded to instances of [eq]. We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type. The type of [eq] allows us to state any equalities, even those that are provably false. However, examining the type of equality's sole constructor [refl_equal], we see that we can only _prove_ equality when its two arguments are syntactically equal. This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition. Another way of stating that definition is: equality is defined as the least reflexive relation. 473 Behind the scenes, uses of infix [=] are expanded to instances of [eq]. We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type. The type of [eq] allows us to state any equalities, even those that are provably false. However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal. This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition. Another way of stating that definition is: equality is defined as the least reflexive relation.
474 474
475 Returning to the example of [isZero], we can see how to work with hypotheses that use this predicate. *) 475 Returning to the example of [isZero], we can see how to work with hypotheses that use this predicate. *)
476 476
477 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n. 477 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n.
478 (* begin thide *) 478 (* begin thide *)