Mercurial > cpdt > repo

comparison src/Predicates.v @ 210:b149a07b9b5b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most old Sestoft suggestions processed
author Adam Chlipala <adamc@hcoop.net>
date Mon, 09 Nov 2009 13:18:46 -0500
parents 90af611e2993
children c4b1c0de7af9
comparison
equal deleted inserted replaced
209:90af611e2993 210:b149a07b9b5b
132 (** %\vspace{-.15in}% [[ 132 (** %\vspace{-.15in}% [[
133 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B 133 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B
134 134
135 ]] 135 ]]
136 136
137 The interested reader can check that [and] has a Curry-Howard doppleganger called [prod], the type of pairs. However, it is generally most convenient to reason about conjunction using tactics. An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks. [/\] is an infix shorthand for [and]. *) 137 The interested reader can check that [and] has a Curry-Howard doppelganger called [prod], the type of pairs. However, it is generally most convenient to reason about conjunction using tactics. An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks. [/\] is an infix shorthand for [and]. *)
138 138
139 Theorem and_comm : P /\ Q -> Q /\ P. 139 Theorem and_comm : P /\ Q -> Q /\ P.
140 140
141 (* begin thide *) 141 (* begin thide *)
142 (** We start by case analysis on the proof of [P /\ Q]. *) 142 (** We start by case analysis on the proof of [P /\ Q]. *)