Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 32:77e1a7eda0b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Little fixes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 10 Sep 2008 12:16:54 -0400
parents 1a82839f83b7
children 8b34dade70e1
comparison
equal deleted inserted replaced
31:1a82839f83b7 32:77e1a7eda0b8
85 85
86 Theorem the_sky_is_falling : forall x : Empty_set, 2 + 2 = 5. 86 Theorem the_sky_is_falling : forall x : Empty_set, 2 + 2 = 5.
87 destruct 1. 87 destruct 1.
88 Qed. 88 Qed.
89 89
90 (** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and dependent function types.) 90 (** Because [Empty_set] has no elements, the fact of having an element of this type implies anything. We use [destruct 1] instead of [destruct x] in the proof because unused quantified variables are relegated to being referred to by number. (There is a good reason for this, related to the unity of quantifiers and implication. An implication is just a quantification over a proof, where the quantified variable is never used. It generally makes more sense to refer to implication hypotheses by number than by name, and Coq treats our quantifier over an unused variable as an implication in determining the proper behavior.)
91 91
92 We can see the induction principle that made this proof so easy: *) 92 We can see the induction principle that made this proof so easy: *)
93 93
94 Check Empty_set_ind. 94 Check Empty_set_ind.
95 (** [[ 95 (** [[