Mercurial > cpdt > repo
comparison src/Predicates.v @ 426:5f25705a10ea
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 *) |