Propositions
Here we assert that plus is commutative. There are several parts
to this proposition.
The ∀ n m : nat, ... blah ... part is a quantifier. We're
saying that "for arbitrary n and m of type nat, it is the
case that ... blah ...". Here, our "blah" is n + m = m + n,
i.e., for any n and m, the number n + m is equal to m + n,
i.e., order doesn't matter for addition, i.e., addition is
commutative.
This proposition is also provable.
So far we've seen two ways to form a Prop: equality and
quantification. We can give a grammar in BNF (Backus-Naur Form):
PROP ::= EXPR1 = EXPR2
| ∀ x : TYPE, PROP
where EXPRi refers to an expression and TYPE refers to some
type. When you have multiple variables in a quantifier, it's like
stringing them together:
∀ n m : TYPE, PROP is the same as
∀ n : TYPE, ∀ m : TYPE, PROP You can of course have variables of different types. Here is a proposition asserting that the length of repeat b n is n, for all b and n. This proposition is also provable.
PROP ::= EXPR1 = EXPR2
| ∀ x : TYPE, PROP
∀ n m : TYPE, PROP is the same as
∀ n : TYPE, ∀ m : TYPE, PROP You can of course have variables of different types. Here is a proposition asserting that the length of repeat b n is n, for all b and n. This proposition is also provable.
Note that all syntactically well-formed propositions have type
Prop in Coq, regardless of whether they are true.
Simply being a proposition is one thing; being provable is
something else!
This one seems unlikely. Translating to English, "For any natural
number n, it is the case that n is equal to 2." There are
definitely natural numbers other than 2. Like, say, 1. Or 0. Or
731. None of those are equal to 2. This proposition does not
hold---it is not provable. In fact, it's possible to prove that
this proposition does not hold.
Even more baldly wrong. It is not the case that 3 = 4. It is
possible to prove that this proposition does not hold.
Indeed, propositions don't just have types: they are
first-class objects that can be manipulated in the same ways as
the other entities in Coq's world. Propositions can be used in
many other ways. For example, we can give a name to a proposition
using a Definition, just as we have given names to expressions
of other sorts.
We can also write parameterized propositions -- that is,
functions that take arguments of some type and return a
proposition.
For instance, the following function takes a number
and returns a proposition asserting that this number is equal to
three:
In Coq, functions that return propositions are said to define
properties of their arguments.
For instance, here's a (polymorphic) property defining the notion
of an injective function: no two inputs share the same
output. Literally: if f maps x and y to the same value, then
x has to be the same as y.
The proposition that S, the successor function, is injective. This
property holds.
The proposition that pred, the successor function, is
injective. This property does not hold: pred 0 = pred 1 = 0.
The equality operator = is also a function that returns a
Prop. That's why it showed up in our BNF for Prop earlier!
The expression n = m is syntactic sugar for eq n m (defined
using Coq's Notation mechanism). Because eq can be used with
elements of any type, it is also polymorphic:
(Notice that we wrote @eq instead of eq: The type
argument A to eq is declared as implicit, so we need to turn
off implicit arguments to see the full type of eq.)
Simple proofs
Theorem NAME : PROP.
Proof.
TACTICS...
Qed.
Proof by Simplification
What's happening here? It's worth stepping through the proof
slowly, looking at the various views: there's the main script
screen, the screen with the goal and context, and a response
screen.
We write Theorem and then a name for our theorem---here
plus_O_n. Then we write a proposition, in this case ∀ n
: nat, 0 + n = n, i.e., for any possible natural number n, it
is the case that 0 + n is equal to n. We'll talk more about
what counts as a proposition later in the course.
After we type the Proof. keyword, we're shown a screen like the
following:
1 subgoal, subgoal 1 (ID 50)
============================
∀ n : nat, 0 + n = n The first line says how many cases we're considering in our proof at present: there's 1 subgoal, and we're currently working on it. That is: our proof has only one case.
Then there's a line. Beneath the line is our *goal*---that's what
we're trying to prove. Above the line is our *context*, which is
currently empty.
The way a proof works is that we try to show that given our
context, our goal *holds*, that is, that our goal is a true
proposition.
In Coq, we use tactics to manipulate the goal and context, where
Coq will keep track of the goal and context for us. On paper (or on
a chalkboard or in person), we'll use natural language (for CS 54,
English) to manipulate the goal and context, which we'll keep
track of ourselves.
Throughout the course, we'll try to keep parallel tracks in mind:
how does proof work in Coq and how does it work on paper? We'll
only really be doing proofs in Coq at first, and then we'll
switch and only do proofs on paper. After this course, you'll
probably only use paper proofs. We'll be using Coq as a tool to
help you learn the ropes of paper proof. One of the hardest things
about paper proof is that it can be very easy to get confused and
make mistakes, breaking the "rules". Coq enforces the rules! Using
Coq will help you internalize the rules.
After the Proof. keyword comes our *proof script*, a series of
*tactics* telling Coq how to manipulate the proof state. Each
tactic is followed by a period.
Before explaining the proof script, let's see the above proof in
English.
1 subgoal, subgoal 1 (ID 51)
n : nat
============================
0 + n = n We could have chosen a different name---go back and change it to read intros m and see what goal you get! (It's generally good style to use the name in the quantifier, since it's a little clearer.)
Our next tactic is simpl plus, which asks Coq to simplify our
goal "through" the definition of plus, running a few steps of
computation:
1 subgoal, subgoal 1 (ID 53)
n : nat
============================
n = n Our context remains the same, but our new goal is to show that n = n. To do so, we use the reflexivity tactic, named after the property of equality: all things are equal to themselves.
When we run the tactic, we get a new readout:
No more subgoals.
(dependent evars: (printing disabled) ) Coq is being a little too lowkey here: we proved it! To celebrate (and tell Coq that we're satisfied with our proof), we say Qed., which is short for quod erat demonstrandum, which is Latin for "that which was to be proved" which is perhaps better said as "and we've proved what we want to" or "and that's the proof" or "I told you so!" or "mic drop". Then Coq acknowledges that we're truly done:
plus_O_n is defined The paper and Coq proofs are very much in parallel. Here's the paper proof annotated with Coq tactics:
(You may notice that the above statement looks different in
the .v file in your IDE than it does in the HTML rendition in
your browser, if you are viewing both. In .v files, we write the
∀ universal quantifier using the reserved identifier
"forall." When the .v files are converted to HTML, this gets
transformed into an upside-down-A symbol.)
This is a good place to mention that reflexivity is a bit
more powerful than we have admitted. In the examples we have seen,
the calls to simpl were actually not needed, because
reflexivity can perform some simplification automatically when
checking that two sides are equal; simpl was just added so that
we could see the intermediate state -- after simplification but
before finishing the proof. Here is a shorter proof of the
theorem:
1 subgoal, subgoal 1 (ID 50)
============================
∀ n : nat, 0 + n = n The first line says how many cases we're considering in our proof at present: there's 1 subgoal, and we're currently working on it. That is: our proof has only one case.
- Theorem: For any natural number n,
0 + n = n. Proof: Let n be given. We must show that
0 + n = n. By the definition of plus, we know that 0+n reduces to n. Finally, we have
n = n immediately. Qed.
1 subgoal, subgoal 1 (ID 51)
n : nat
============================
0 + n = n We could have chosen a different name---go back and change it to read intros m and see what goal you get! (It's generally good style to use the name in the quantifier, since it's a little clearer.)
1 subgoal, subgoal 1 (ID 53)
n : nat
============================
n = n Our context remains the same, but our new goal is to show that n = n. To do so, we use the reflexivity tactic, named after the property of equality: all things are equal to themselves.
No more subgoals.
(dependent evars: (printing disabled) ) Coq is being a little too lowkey here: we proved it! To celebrate (and tell Coq that we're satisfied with our proof), we say Qed., which is short for quod erat demonstrandum, which is Latin for "that which was to be proved" which is perhaps better said as "and we've proved what we want to" or "and that's the proof" or "I told you so!" or "mic drop". Then Coq acknowledges that we're truly done:
plus_O_n is defined The paper and Coq proofs are very much in parallel. Here's the paper proof annotated with Coq tactics:
- Theorem: For any natural number n,
0 + n = n. Proof: Let n be given (intros n.). We must show that
0 + n = n. By the definition of plus, we know that 0+n reduces to n (simpl plus.). Finally, we have
n = n immediately (reflexivity.). Qed.
Moreover, it will be useful later to know that reflexivity
does somewhat more simplification than simpl does -- for
example, it tries "unfolding" defined terms, replacing them with
their right-hand sides. The reason for this difference is that,
if reflexivity succeeds, the whole goal is finished and we don't
need to look at whatever expanded expressions reflexivity has
created by all this simplification and unfolding; by contrast,
simpl is used in situations where we may have to read and
understand the new goal that it creates, so we would not want it
blindly expanding definitions and leaving the goal in a messy
state.
The form of the theorem we just stated and its proof are almost
exactly the same as the simpler examples we saw earlier; there are
just a few differences.
First, we've used the keyword Theorem instead of Example.
This difference is mostly a matter of style; the keywords
Example and Theorem (and a few others, including Lemma,
Fact, and Remark) mean pretty much the same thing to Coq.
Second, we've added the quantifier ∀ n:nat, so that our
theorem talks about all natural numbers n. Informally, to
prove theorems of this form, we generally start by saying "Suppose
n is some number..." Formally, this is achieved in the proof by
intros n, which moves n from the quantifier in the goal to a
context of current assumptions.
The keywords intros, simpl, and reflexivity are examples of
tactics. A tactic is a command that is used between Proof and
Qed to guide the process of checking some claim we are making.
We will see several more tactics in the rest of this chapter and
yet more in future chapters.
Other similar theorems can be proved with the same pattern.
(* Add comments to this proof to lay it out informally, as we showed in the examples above.
For example, start with something like:
- _Theorem_: For any natural number n,
0 × n = n. _Proof_: ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of proof.
*)
Theorem mult_0_l : ∀ n:nat, 0 × n = 0.
Proof.
intros n.
simpl mult.
reflexivity.
Qed.
(* Do not modify the following line: *)
Definition manual_grade_for_mult_0_l_informal : option (nat×string) := None.
☐
For example, start with something like:
- _Theorem_: For any natural number n,
0 × n = n. _Proof_: ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of proof.
*)
Theorem mult_0_l : ∀ n:nat, 0 × n = 0.
Proof.
intros n.
simpl mult.
reflexivity.
Qed.
(* Do not modify the following line: *)
Definition manual_grade_for_mult_0_l_informal : option (nat×string) := None.
☐
The intros and apply Tactics
Let a proposition A be given such that A holds (call this
hypothesis HA).
We must prove that A holds.
apply HA.
We find A by HA.
Qed.
Lemma modus_ponens : ∀ P Q,
(P → Q) →
P →
Q.
Proof.
intros P Q HPQ HP.
apply HPQ.
apply HP.
Qed.
Lemma modus_ponens : ∀ P Q,
(P → Q) →
P →
Q.
Proof.
intros P Q HPQ HP.
apply HPQ.
apply HP.
Qed.
modus_ponens is the first theorem we've seen that has multiple
hypotheses. How should we parse the following proposition?
(P → Q) →
P →
Q.
The answer is that implication is right associative, that is,
we assume that parentheses go on the right, as in:
(P → Q) →
(P →
Q).
If we were to read this proposition aloud, we could naively
read it as:
But we can read it more naturally as:
That is, we've translated nested implications to a conjuction,
with the word "and". We'll talk more about conjunctions soon.
We can translate the proof above as something like:
Use intros and apply to show that if P implies Q and Q
implies R and P holds, then R holds.
Hint: you'll want to use backwards reasoning. To prove that R
holds, it suffices to show that Q holds (because Q → R). To
prove that Q holds, it suffices to show that P holds (because
P → Q). But we know P holds, so...
(P → Q) →
P →
Q.
(P → Q) →
(P →
Q).
if it is the case that [P -> Q],
then if it is the case that [P]
then it is the case that [Q].
if it is the case that [(P -> Q)]
and [P],
then it is the case that [Q].
- Theorem: For any propositions P and Q,
(P → Q) → P → Q Proof: Let P and Q be given, and assume P → Q and P hold. (intros P Q HPQ HP.). We must show that Q holds.
Exercise: 2 stars, standard (implies_PQR)
Remove "Admitted." and fill in the proof.
Lemma implies_PQR : ∀ P Q R : Prop,
(P → Q) →
(Q → R) →
P →
R.
Proof.
(* FILL IN HERE *) Admitted.
☐
(P → Q) →
(Q → R) →
P →
R.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* Add comments to your proof of implies_PQR to lay it out informally, as we showed in the examples above.
For example, start with something like:
- _Theorem_: For all properties P, Q, and R, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of _modus ponens_ above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_implies_PQR_informal : option (nat×string) := None.
☐
For example, start with something like:
- _Theorem_: For all properties P, Q, and R, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of _modus ponens_ above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_implies_PQR_informal : option (nat×string) := None.
☐
Logical connectives
Conjunction
- For all propositions A and B, if it is the case that A
- For all propositions A and B, if A and B hold, then A ∧ B holds.
Lemma and_intro : ∀ A B : Prop, A → B → A ∧ B.
Proof.
intros A B HA HB.
(* Let propositions A and B be given. Suppose that A holds
(call this hypothesis HA) and B holds (call this hypothesis
HB. *)
split.
(* We need to prove A ∧ B. To prove a conjunction, we must prove
both of its parts.
Whenever you start working on a subpart, you should use a bullet
-. Like in an outline for a paper, bullets nest. You can use
-, +, and × as bullets. The order doesn't matter, but each
level has to be homogeneous. If you run out of bullets, you can
start doubling or tripling them, as in --, +++, **, etc.
*)
- (* To prove the left-hand side of the conjunction, we need to show
A. We have this by hypothesis HA. *)
apply HA.
- (* To prove the left-hand side of the conjunction, we need to show
B. We have this by hypothesis HB. *)
apply HB.
Qed.
Proof.
intros A B HA HB.
(* Let propositions A and B be given. Suppose that A holds
(call this hypothesis HA) and B holds (call this hypothesis
HB. *)
split.
(* We need to prove A ∧ B. To prove a conjunction, we must prove
both of its parts.
Whenever you start working on a subpart, you should use a bullet
-. Like in an outline for a paper, bullets nest. You can use
-, +, and × as bullets. The order doesn't matter, but each
level has to be homogeneous. If you run out of bullets, you can
start doubling or tripling them, as in --, +++, **, etc.
*)
- (* To prove the left-hand side of the conjunction, we need to show
A. We have this by hypothesis HA. *)
apply HA.
- (* To prove the left-hand side of the conjunction, we need to show
B. We have this by hypothesis HB. *)
apply HB.
Qed.
In addition to the outlining marks -, +, and ×, you can use
curly braces to enter new outline levels. Every time you use curly
braces, you reset the tracking of outlines, and you can reuse any
outlining symbol.
Lemma and_intro_braces : ∀ A B : Prop, A → B → A ∧ B.
Proof.
intros A B HA HB.
split.
{ apply HA. }
{ apply HB. }
Qed.
Proof.
intros A B HA HB.
split.
{ apply HA. }
{ apply HB. }
Qed.
Formatting matters. Coq will accept proofs in any valid
formatting, but humans... less so. Keeping things clean is very
important: for now, it helps us grade your work. Later on, clean
formatting will make it much easier to work with other people.
Many software development projects care so much about clean
formatting that they use automatic formatters, and no code can be
added to the project unless it meets the formatting guidelines!
Lemma and_intro_sloppy : ∀ A B : Prop, A → B → A ∧ B.
Proof.
intros A B HA HB. split. apply HA.
apply HB.
Qed.
Example and_example : 3 + 4 = 7 ∧ 2 × 2 = 4.
Proof.
intros A B HA HB. split. apply HA.
apply HB.
Qed.
Example and_example : 3 + 4 = 7 ∧ 2 × 2 = 4.
To prove a conjunction, use the split tactic. It will generate
two subgoals, one for each part of the statement:
Proof.
(* WORKED IN CLASS *)
split.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
(* WORKED IN CLASS *)
split.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Since applying a theorem with hypotheses to some goal has the
effect of generating as many subgoals as there are hypotheses for
that theorem, we can apply and_intro to achieve the same effect
as split.
Example and_example' : 3 + 4 = 7 ∧ 2 × 2 = 4.
Proof.
(* apply works with everything defined so far, not just
hypotheses/assumptions in your context. *)
apply and_intro.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
Proof.
(* apply works with everything defined so far, not just
hypotheses/assumptions in your context. *)
apply and_intro.
- (* 3 + 4 = 7 *) reflexivity.
- (* 2 + 2 = 4 *) reflexivity.
Qed.
By the way, the infix notation ∧ is actually just syntactic
sugar for and A B. That is, and is a Coq operator that takes
two propositions as arguments and yields a proposition.
Exercise: 2 stars, standard (and_PQ)
Some more practice with implications and conjunctions. If P implies Q and you know P, then you know both P and Q.
(* Add comments to your proof of and_PQ above to lay it out informally, as we showed in the examples above.
Maybe start with something like:
- _Theorem_: For all properties P and Q, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of and_intro above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_and_PQ_informal : option (nat×string) := None.
☐
Maybe start with something like:
- _Theorem_: For all properties P and Q, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of and_intro above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_and_PQ_informal : option (nat×string) := None.
☐
Disjunction
Lemma or_intro_l : ∀ A B : Prop, A → A ∨ B.
Proof.
(* Let propositions A and B be given, and assume A holds. *)
intros A B HA.
(* We have to show A ∨ B. We do this by proving A. *)
left.
(* But A was just our assumption! *)
apply HA.
Qed.
Lemma or_intro_r : ∀ A B : Prop, B → A ∨ B.
Proof.
intros A B HB.
(* A fork in the road! Hang a right this time. *)
right.
apply HB.
Qed.
Check or.
(* ===> or : Prop -> Prop -> Prop *)
Proof.
(* Let propositions A and B be given, and assume A holds. *)
intros A B HA.
(* We have to show A ∨ B. We do this by proving A. *)
left.
(* But A was just our assumption! *)
apply HA.
Qed.
Lemma or_intro_r : ∀ A B : Prop, B → A ∨ B.
Proof.
intros A B HB.
(* A fork in the road! Hang a right this time. *)
right.
apply HB.
Qed.
Check or.
(* ===> or : Prop -> Prop -> Prop *)
In natural language 'or' is often interpreted to be exclusive (one
or the other) rather than inclusive (at least one, possibly
both). In formal work, disjunction is inclusive, meaning 'at least
one'.
Consider the proposition 2 = 2 ∨ 4 = 4. Both sides are true,
but a proof need only show one side. In fact, it would be a little
bit strange---not wrong, but strange---for a proof to show both!
Lemma or_inclusive1 : 2 = 2 ∨ 4 = 4.
Proof. left. reflexivity. Qed.
Lemma or_inclusive2 : 2 = 2 ∨ 4 = 4.
Proof. right. reflexivity. Qed.
Proof. left. reflexivity. Qed.
Lemma or_inclusive2 : 2 = 2 ∨ 4 = 4.
Proof. right. reflexivity. Qed.
(* Add comments to your proof of or_which above to lay it out informally, as we showed in the examples above.
Maybe start with something like:
- _Theorem_: For all properties P and Q, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of or_intro_l above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_or_which_informal : option (nat×string) := None.
☐
Maybe start with something like:
- _Theorem_: For all properties P and Q, ...
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of or_intro_l above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_or_which_informal : option (nat×string) := None.
☐
Truth
If you can't remember that I is the single proof of True, you
can also just use the reflexivity tactic.
Lemma True_is_true' : True.
Proof. reflexivity. Qed.
Lemma True_and_id : True ∧ True.
Proof.
split.
- apply I.
- apply I.
Qed.
Lemma True_or_l : ∀ A : Prop, True ∨ A.
Proof.
left. apply I.
Qed.
Lemma True_or_r : ∀ A : Prop, A ∨ True.
Proof.
right. apply I.
Qed.
Proof. reflexivity. Qed.
Lemma True_and_id : True ∧ True.
Proof.
split.
- apply I.
- apply I.
Qed.
Lemma True_or_l : ∀ A : Prop, True ∨ A.
Proof.
left. apply I.
Qed.
Lemma True_or_r : ∀ A : Prop, A ∨ True.
Proof.
right. apply I.
Qed.
True is used quite rarely, since it is trivial (and therefore
uninteresting) to prove as a goal, and it carries no useful
information as a hypothesis.
But True can be quite useful when defining complex Props using
conditionals or as a parameter to higher-order Props. We may
see examples of such uses of True later on.
Instead of making a universal claim about all numbers n
and m, it talks about a more specialized property that only
holds when n = m. The arrow symbol is pronounced "implies."
We've already defined a notion of implies on booleans impb; now
we have a notion of implies on propositions.
The way a proof with implies works is: you have to prove what's to
the right of the arrow... but you may assume what's to the
left. That is, to show that n + n = m + m, we know (in our
context) not only that n and m are natural numbers, but in
fact it is the case that n = m.
As before, we need to be able to reason by assuming we are given
such numbers n and m. We also need to assume the hypothesis
n = m. The intros tactic will serve to move all three of these
from the goal into assumptions in the current context.
Since n and m are arbitrary numbers, we can't just use
simplification to prove this theorem. Instead, we prove it by
observing that, if we are assuming n = m, then we can replace
n with m in the goal statement and obtain an equality with the
same expression on both sides. The tactic that tells Coq to
perform this replacement is called rewrite.
Proof.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite → H.
reflexivity. Qed.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite → H.
reflexivity. Qed.
The first line of the proof moves the universally quantified
variables n and m into the context. The second moves the
hypothesis n = m into the context and gives it the name H.
The third tells Coq to rewrite the current goal (n + n = m + m)
by replacing the left side of the equality hypothesis H with the
right side.
(The arrow symbol in the rewrite has nothing to do with
implication: it tells Coq to apply the rewrite from left to right.
To rewrite from right to left, you can use rewrite <-. Try
making this change in the above proof and see what difference it
makes.) Here's a paper proof of the same theorem, with the tactics
interwoven.
- Theorem: For any natural numbers n and m,
if
n = m then
n + n = m + m.
n + n = m + m.
m + m = m + m immediately (reflexivity.). Qed.
Exercise: 1 star, standard (plus_id_exercise)
Theorem plus_id_exercise : ∀ n m o : nat,
n = m → m = o → n + m = m + o.
Proof.
(* FILL IN HERE *) Admitted.
☐
n = m → m = o → n + m = m + o.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem mult_0_plus : ∀ n m : nat,
(0 + n) × m = n × m.
Proof.
intros n m.
rewrite → plus_O_n.
reflexivity. Qed.
(0 + n) × m = n × m.
Proof.
intros n m.
rewrite → plus_O_n.
reflexivity. Qed.
Note that we've just rewritten by an existing theorem: the proof
of mult_0_plus uses the proof of plus_O_n.
In an informal proof, we might use language by "by plus_0_n, we
know...". For example:
- Theorem: For any natural number n and m,
(0 + n) × m = n × m.
(0 + n) × m = n × m.
n × m = n × m immediately (reflexivity.). Qed.
Exercise: 2 stars, standard (mult_S_1)
Optional exerises are just good practice. They're worth no points.
Theorem mult_S_1 : ∀ n m : nat,
m = S n →
m × (1 + n) = m × m.
Proof.
(* FILL IN HERE *) Admitted.
(* (N.b. This proof can actually be completed without using rewrite,
but please do use rewrite for the sake of the exercise.) *)
☐
m = S n →
m × (1 + n) = m × m.
Proof.
(* FILL IN HERE *) Admitted.
(* (N.b. This proof can actually be completed without using rewrite,
but please do use rewrite for the sake of the exercise.) *)
☐
(* Add comments to your proof of mult_S_1 above to lay it out informally, as we showed in the examples above.
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of mult_0_plus above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_mult_S_1_informal : option (nat×string) := None.
☐
It's OK if you want to add the lines in one large comment block, or sneak them in between lines of the proof. It might look a bit like our proof of mult_0_plus above.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_mult_S_1_informal : option (nat×string) := None.
☐
(* Let's look at a silly theorem about natural numbers: *)
Theorem silly1 : ∀ (n m o p : nat),
n = m →
[n;o] = [n;p] →
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
rewrite <- eq1.
Theorem silly1 : ∀ (n m o p : nat),
n = m →
[n;o] = [n;p] →
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
rewrite <- eq1.
Here, we could finish with "rewrite → eq2. reflexivity." as we
have done several times before. We can achieve the same effect in
a single step by using the apply tactic instead:
apply eq2. Qed.
The apply tactic also works with conditional hypotheses
and lemmas: if the statement being applied is an implication, then
the premises of this implication will be added to the list of
subgoals needing to be proved. If there are no premises (i.e., H
isn't an implication), then you're done!
Theorem silly2 : ∀ (n m o p : nat),
n = m →
(∀ (q r : nat), q = r → [q;o] = [r;p]) →
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.
n = m →
(∀ (q r : nat), q = r → [q;o] = [r;p]) →
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.
Typically, when we use apply H, the statement H will
begin with a ∀ that binds some universal variables. When
Coq matches the current goal against the conclusion of H, it
will try to find appropriate values for these variables. For
example, when we do apply eq2 in the following proof, the
universal variable q in eq2 gets instantiated with n and r
gets instantiated with m.
Theorem silly2a : ∀ (n m : nat),
(n,n) = (m,m) →
(∀ (q r : nat), (q,q) = (r,r) → [q] = [r]) →
[n] = [m].
Proof.
intros n m eq1 eq2.
apply eq2. apply eq1. Qed.
(n,n) = (m,m) →
(∀ (q r : nat), (q,q) = (r,r) → [q] = [r]) →
[n] = [m].
Proof.
intros n m eq1 eq2.
apply eq2. apply eq1. Qed.
It's often helpful to look at definitions before doing proofs!
Theorem silly_ex :
(∀ n, evenb n = true → oddb (S n) = true) →
evenb 3 = true →
oddb 4 = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
(∀ n, evenb n = true → oddb (S n) = true) →
evenb 3 = true →
oddb 4 = true.
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem silly3_firsttry : ∀ (n : nat),
true = eqb n 5 →
eqb (S (S n)) 7 = true.
Proof.
intros n H.
simpl eqb.
true = eqb n 5 →
eqb (S (S n)) 7 = true.
Proof.
intros n H.
simpl eqb.
Here we cannot use apply directly, but we can use the symmetry
tactic, which switches the left and right sides of an equality in
the goal.
symmetry.
apply H.
Qed.
apply H.
Qed.
To sum up, one can say apply H when H is a hypothesis in the
context or a previously proven lemma of the form ∀ x1 ...,
H1 → H2 → ... → Hn and the current goal is shape Hn (for
some instantatiation of each of the xi). After running apply H
in such a state, you will have a subgoal for each of H1 through
Hn-1. In the special case where H isn't an implication, your
proof will be completed.
The informal analogue of the apply tactic is phrasing like "by
H, it suffices to show Hn by proving each of H1, ..., Hn-1",
followed by a proof of those subsidiary parts. In the case where
H isn't an implication, you can try using language like "we are
done by H" or "which H proves exactly".
The following silly example uses two rewrites in a row to
get from [a,b] to [e,f].
Example trans_eq_example : ∀ (a b c d e f : nat),
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
rewrite → eq1. rewrite → eq2.
reflexivity.
Qed.
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
rewrite → eq1. rewrite → eq2.
reflexivity.
Qed.
Since this is a common pattern, we might like to pull it out
as a lemma recording, once and for all, the fact that equality is
transitive.
Theorem trans_eq : ∀ (X:Type) (n m o : X),
n = m → m = o → n = o.
Proof.
intros X n m o eq1 eq2.
rewrite → eq1. rewrite → eq2.
reflexivity.
Qed.
n = m → m = o → n = o.
Proof.
intros X n m o eq1 eq2.
rewrite → eq1. rewrite → eq2.
reflexivity.
Qed.
Now, we should be able to use trans_eq to prove the above
example. However, to do this we need to be very clear about how we are apply-ing trans_eq.
Example trans_eq_example' : ∀ (a b c d e f : nat),
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
If we simply tell Coq apply trans_eq at this point, it can tell
(by matching the goal against the conclusion of the lemma) that it
should instantiate X with [nat], n with [a,b], and o
with [e,f]. However, the matching process doesn't determine an
instantiation for m: we have to supply one explicitly by being
more specific about the theorem we're using. The proofs we have
give us truths with parameters, and just as with function
parameters we can specify those when we use the proof.
(* apply (trans_eq (list nat) a;b c;d e;f). *)
(* or even better: *)
apply (trans_eq _ _ [c;d] _).
apply eq1. apply eq2.
Qed.
(* or even better: *)
apply (trans_eq _ _ [c;d] _).
apply eq1. apply eq2.
Qed.
Most of the time, context is enough and Coq can guess the
right parameters using parameter synthesis; we might have instead
written apply (trans_eq _ [a;b] [c;d] [e;f]) or even apply
(trans_eq _ _ [c;d] _).
Why do we need to specify [c;d] at all? Because that particular
list is our "bridge" between the two facts we know, and Coq
doesn't look at the theorems in scope when guessing what to apply,
only at the goal we're matching the applied proof against.
Informally, we might say "by the transitivity of equality via [c;d]".
In fact, the assumptions themselves can act as parameters for trans_eq and other proofs with premises:
Example trans_eq_example'' : ∀ (a b c d e f : nat),
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* We can provide the two premises eq1 and eq2 in the order we would have applied them... *)
(* apply (trans_eq _ _ c;d _ eq1 eq2). *)
(* But since the premises themselves give values for all three parameters we can use them to make Coq pick [c;d] for us! *)
apply (trans_eq _ _ _ _ eq1 eq2).
Qed.
[a;b] = [c;d] →
[c;d] = [e;f] →
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
(* We can provide the two premises eq1 and eq2 in the order we would have applied them... *)
(* apply (trans_eq _ _ c;d _ eq1 eq2). *)
(* But since the premises themselves give values for all three parameters we can use them to make Coq pick [c;d] for us! *)
apply (trans_eq _ _ _ _ eq1 eq2).
Qed.
Exercise: 3 stars, standard (trans_eq_exercise)
Here's a lemma to practice applying theorems with parameters.
Definition minustwo (n : nat) : nat :=
match n with
| O ⇒ O
| S O ⇒ O
| S (S n') ⇒ n'
end.
Example trans_eq_exercise : ∀ (n m o p : nat),
m = (minustwo o) →
(n + p) = m →
(n + p) = (minustwo o).
Proof.
(* FILL IN HERE *) Admitted.
☐
match n with
| O ⇒ O
| S O ⇒ O
| S (S n') ⇒ n'
end.
Example trans_eq_exercise : ∀ (n m o p : nat),
m = (minustwo o) →
(n + p) = m →
(n + p) = (minustwo o).
Proof.
(* FILL IN HERE *) Admitted.
☐
Propositions so far
Tactics so far
- intros
- simpl
- reflexivity
- apply
- split
- left, right
- rewrite
- symmetry
- apply
What's happening here?
(* 2022-01-12 10:20 *)