Mercurial > cpdt > repo
comparison src/Predicates.v @ 202:8caa3b3f8fc0
Feedback from Peter Gammie
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 03 Jan 2009 19:57:02 -0500 |
| parents | 55199444e5e7 |
| children | 71ade09024ac |
comparison
equal
deleted
inserted
replaced
| 201:a2b14ba218a7 | 202:8caa3b3f8fc0 |
|---|---|
| 441 (** [[ | 441 (** [[ |
| 442 | 442 |
| 443 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x | 443 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x |
| 444 ]] *) | 444 ]] *) |
| 445 | 445 |
| 446 (** [eq] is the type we get behind the scenes when uses of infix [=] are expanded. We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type. It is crucial that the second argument is untied to the parameter in the type of [eq]; otherwise, we would have to prove that two values are equal even to be able to state the possibility of equality, which would more or less defeat the purpose of having an equality proposition. However, examining the type of equality's sole constructor [refl_equal], we see that we can only %\textit{%#<i>#prove#</i>#%}% 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. | 446 (** [eq] is the type we get behind the scenes when uses of infix [=] are expanded. 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 %\textit{%#<i>#prove#</i>#%}% 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. |
| 447 | 447 |
| 448 Returning to the example of [isZero], we can see how to make use of hypotheses that use this predicate. *) | 448 Returning to the example of [isZero], we can see how to make use of hypotheses that use this predicate. *) |
| 449 | 449 |
| 450 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n. | 450 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n. |
| 451 (* begin thide *) | 451 (* begin thide *) |
| 741 rewrite <- plus_n_Sm in H0. | 741 rewrite <- plus_n_Sm in H0. |
| 742 | 742 |
| 743 (** The induction hypothesis lets us complete the proof. *) | 743 (** The induction hypothesis lets us complete the proof. *) |
| 744 apply IHeven with n0; assumption. | 744 apply IHeven with n0; assumption. |
| 745 | 745 |
| 746 (** As usual, we can rewrite the proof to avoid referencing any locally-generated names, which makes our proof script more readable and more robust to changes in the theorem statement. *) | 746 (** As usual, we can rewrite the proof to avoid referencing any locally-generated names, which makes our proof script more readable and more robust to changes in the theorem statement. We use the notation [<-] to request a hint that does right-to-left rewriting, just like we can with the [rewrite] tactic. *) |
| 747 Restart. | 747 Restart. |
| 748 Hint Rewrite <- plus_n_Sm : cpdt. | 748 Hint Rewrite <- plus_n_Sm : cpdt. |
| 749 | 749 |
| 750 induction 1; crush; | 750 induction 1; crush; |
| 751 match goal with | 751 match goal with |