The goal of this lecture note is to recapitulate what we have seen so far in FPP.
A .v file file contains library imports (e.g., Require Import Arith.), commands (e.g., Check, Compute, and Search), and definitions (e.g., Ltac, Notation, Definition, Fixpoint, Inductive, Property, Proposition, Lemma, Theorem, and Corollary):
Libraries:
- They include Arith (for the type nat), Bool (for the type bool), and List (for lists).
Commands:
- Check provides a way to query the type of an expression (e.g., Check (6 * 9) and Check plus_Sn_m).
- Compute provides a way to evaluate an expression (e.g., Compute (6 * 9) in base 10).
- Search provides a way to search for pre-existing definitions by pattern matching (e.g., Search (S _ + _ = S (_ + _))).
Definitions:
- Definition provides a way to name expressions.
- Fixpoint provides a way to declare recursive functions and to name them.
- Inductive provides a way to declare data types and to name them.
- Ltac provides a way to define one’s own proof tactics, and is out of scope here.
- Notation provides a way to specify, e.g., infix operators, and is out of scope here.
The keywords Property, Proposition, Lemma, Theorem, and Corollary provide a way to declare logical statements and to name them. These logical statements are followed by a proof. A proof is a sequence of tactical steps.
Bong-sun: Semiotics?Halcyon: Semiotics.For a mathematician, a lemma is an auxiliary theorem used for proving a main theorem (even though the auxiliary lemma that accompanies a theorem is often larger than this theorem) and a corollary is a theorem that is proved as a consequence of another theorem. Likewise, a property is a simple theorem (i.e., a theorem with a simple proof), and a proposition is something a mathematician states a priori when they do not know yet whether it will end up as a theorem or as a lemma. In other words, this vocabulary is used to convey the conceptual importance of the corresponding logical statement.
The programming part of tCPA consists in defining functions. The proving part of tCPA consists in formulating logical statements and proving them, starting with the keyword Proof. (which is actually optional, and only used for clarity).
A learning goal of this course is to reason about functional programs using tCPA.
Programs are structured as main functions and auxiliary functions. Typically, the main functions are not recursive but the auxiliary functions are. For example, an auxiliary function
Correspondingly, main functions are reasoned about with a main theorem and auxiliary functions with auxiliary lemmas: often, the main theorem is proved as a corollary of auxiliary lemmas. And structurally recursive functions are reasoned about using structural induction.
clear – is used to remove an assumption from the premises. For example:
Proposition clearly :
forall A B : Prop,
A -> B -> A.
Proof.
intros A B H_A H_B.
The *goals* window reads:
A, B : Prop
H_A : A
H_B : B
============================
A
Since the assumption about B is not needed, we can remove it:
clear H_B.
The *goals* window then reads:
A, B : Prop
H_A : A
============================
A
eqn – is used to add named Leibniz equalities among the current assumptions. For example:
Proposition true_or_false :
forall b : bool,
b = true \/ b = false.
Proof.
intro b.
case b as [ | ] eqn:H_b.
-
The *goals* window then reads:
b : bool
H_b : b = true
============================
true = true \/ true = false
The assumption denoted by H_b indicates that we are in the true case. Continuing the proof:
- left.
reflexivity.
-
The *goals* window then reads:
b : bool
H_b : b = false
============================
false = true \/ false = false
The assumption denoted by H_b indicates that we are in the false case.
Qed – is used to mark the end of the proof. For example, let us mark the proof of the running proposition:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intros A H_A.
exact H_A.
Qed.
The *response* window then reads:
reflexivity_of_implication is defined
Here are the tactics we have seen so far, in alphabetical order:
discriminate – is used when we can derive a Leibniz equality involving distinct data constructors. Example:
Proposition zero_is_not_one :
0 <> 1.
Proof.
unfold not.
(* the goal is now: 0 = 1 -> False *)
intro H_absurd.
discriminate H_absurd.
Qed.
The accompanying .v file contains other examples, e.g., a proposition to the effect that (the list constructor) nil is not (the list constructor) cons.
exact – is applied to the name of an assumption to complete the current proof when this assumption coincides with the current goal. For example, let us complete the proof of the running proposition:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intros A H_A.
exact H_A.
And indeed the *response* window now reads:
No more subgoals.
injection – is used over composite Leibniz equalities to factor them out into atomic equalities. Example:
Proposition a_list_is_not_another_list :
forall (n1 n2 : nat),
n1 :: 2 :: n2 :: nil <> 1 :: n2 :: 3 :: nil.
Proof.
intros n1 n2.
unfold not.
intro H_tmp.
The *goals* window now reads:
n1, n2 : nat
H_tmp : n1 :: 2 :: n2 :: nil = 1 :: n2 :: 3 :: nil
============================
False
Among the assumptions, H_tmp names a composite Leibniz equality where the left-hand side and the right-hand side contain list constructors. Let us factor this composite equality into atomic equalities:
injection H_tmp as eq_n1_1 eq_2_n2 eq_n2_3.
The *goals* window now reads:
n1, n2 : nat
eq_n1_1 : n1 = 1
eq_2_n2 : 2 = n2
eq_n2_3 : n2 = 3
============================
False
The rest of the proof is routine:
rewrite <- eq_2_n2 in eq_n2_3.
The *goals* window now reads:
n1, n2 : nat
eq_n1_1 : n1 = 1
eq_2_n2 : 2 = n2
eq_n2_3 : 2 = 3
============================
False
The assumption eq_n2_3 names a Leibniz equality involving distinct data constructors, namely S (S O) on the left and S (S (S O)) on the right, a job for the discriminate tactic to complete the proof:
discriminate eq_n2_3.
exists – is used to prove an existentially quantified statement. The argument is a witness for this statement. For example, let us prove the following proposition:
Proposition even_or_odd :
forall n : nat,
(exists q : nat,
n = 2 * q)
\/
(exists q : nat,
n = S (2 * q)).
Proof.
intro n.
induction n as [ | n' [[q IHq] | [q IHq]]].
The beginning of the proof is routine – though do note how the induction hypothesis is destructured, since it is the disjunction of two existential statements. The base case is routine:
- ...
-
In the first induction case (corresponding to the left disjunct in the induction hypothesis), the *goals* window reads:
n', q : nat
IHq : n' = 2 * q
============================
(exists q0 : nat, S n' = 2 * q0) \/ (exists q0 : nat, S n' = S (2 * q0))
First thing first:
rewrite -> IHq.
The *goals* window now reads:
n', q : nat
IHq : n' = 2 * q
============================
(exists q0 : nat, S (2 * q) = 2 * q0) \/ (exists q0 : nat, S (2 * q) = S (2 * q0))
Clearly, to prove this disjunction, we should prove its left disjunct:
right.
The *goals* window now reads:
n', q : nat
IHq : n' = 2 * q
============================
exists q0 : nat, S (2 * q) = S (2 * q0)
The witness we provide is q:
exists q.
The *goals* window now reads:
n', q : nat
IHq : n' = 2 * q
============================
S (2 * q) = S (2 * q)
And we can then proceed.
intro:
If the goal is a universally quantified statement, using the intro tactic fixes the universally quantified variable and adds the name of this fixed variable to the assumptions. For example, let us prove the following proposition:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
The *goals* window reads:
============================
forall A : Prop, A -> A
Let us fix the universally quantified variable using the same name:
intro A.
The *goals* window then reads:
A : Prop
============================
A -> A
Had we used another name than A, this other name would occur in the *goals* window instead of A.
Note: the converse tactic is called revert and requantifies a variable, if no other assumption depends on it. For example, let us continue the proof with the revert tactic:
revert A.
The *goals* window then reads:
============================
forall A : Prop, A -> A
If the goal is an implication, using the intro tactic names the premise of the implication and adds this name to the assumptions. For example:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intro A.
intro H_A.
The *goals* window then reads:
A : Prop
H_A : A
============================
A
Note: the converse tactic revert restores the implication in the goal, if no other assumption depends on its premise. For example, let us continue the proof with the revert tactic:
revert H_A.
The *goals* window then reads:
A : Prop
============================
A -> A
intros, basic version – fixes several universally quantified variables in one step. For example, let us revisit the proposition above:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intros A H_A.
The *goals* window then reads:
A : Prop
H_A : A
============================
A
reflexivity – is used when the goal consists in an equality (i.e., the infix =) where both sides are textually identical.
revert, basic version – requantifies a variable or restores an implication if no other assumption depends on it. For example, let us revisit the proposition above:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intro A.
intro H_A.
The *goals* window then reads:
A : Prop
H_A : A
============================
A
As illustrated above, we can apply the revert tactic to H_A since no other assumption depends on H_A. However, should we try to apply this tactic to A:
revert A.
TCPA would refuse this application and the *response* window would read:
Error: A is used in hypothesis H_A.
revert, advanced version – requantifies or restores several variables or several implications in one step. For example, let us revisit the proposition above:
Proposition reflexivity_of_implication :
forall A : Prop,
A -> A.
Proof.
intros A H_A.
The *goals* window then reads:
A : Prop
H_A : A
============================
A
Applying the revert tactic to A and H_A has the same effect as applying revert to H_A and then applying revert to A:
revert A H_A.
The *goals* window then reads:
============================
forall A : Prop, A -> A
The order of the arguments matter. Should we try instead to apply revert to H_A and A:
revert H_A A.
tCPA would refuse this application and the *response* window would read:
Error: A is used in conclusion.
remember – is used to add new Leibniz equalities among the current assumptions. For example:
remember e as x eqn:H_x.
has the effect of adding:
H_x : x = e
to the current assumptions.
So-called fold-unfold lemmas are used to reason about recursive functions over inductive values. If they look like boilerplate lemmas, it is because they are: each of them corresponds to a possible constructor in the inductive value. It is often surprisingly instructive to write them, since they spell the recursive equations that underlie our recursive definitions.
The induction tactic is used to perform a proof by induction over a value having an inductive type (e.g., nat, list, or more generally any type declared using Inductive).
Typically, when reasoning about a recursive program, an induction proof is carried out by first using the fold-unfold lemmas in each case, and then
If nothing else is needed, the proof is said to be “routine”.
Often though, one needs to strengthen the induction proof using the Light of Inductil and/or to write auxiliary / Eureka / helper lemmas.
Inside, tCPA does some normalization steps. So if the goal is:
let (x, y) := foo 0
in x + y
and we have a lemma somewhere that says:
Lemma fold_unfold_foo_0 :
foo 0 = (10, 20).
then the tactic rewrite -> unfold_foo_0. will
replace foo 0 by (10, 20) in the goal, which, internally, gives:
let (x, y) = (10, 20)
in x + y
normalize the let-expression by binding x to 10 and y to 20 and reproducing the body by replacing x by 10 and y by 20, which results in the goal:
10 + 20
Most of the time, the effect of a rewrite tactic on the current goal is unique. On the occasion, though, the effect we seek is not unique: for example, is the goal is:
n : nat
============================
fib_v1 n = visit_fib_v2 n (fib_v1 1) 0
and we have a lemma somewhere that says:
Lemma fold_unfold_fib_v1_0 :
fib_v1 0 = 0.
If we blithely write:
rewrite <- fold_unfold_fib_v1_0.
then the goal becomes:
n : nat
============================
fib_v1 n = visit_fib_v2 n (fib_v1 (S (fib_v1 0))) (fib_v1 0)
because 1 stands for S O and tCPA replaced both instances of 0 in the goal by fib_v1 0.
What we need to do here is tell tCPA where to perform the rewrite, which is the second occurrence of 0 here. This localized rewrite is achieved with the qualifier at, so that writing:
rewrite <- fold_unfold_fib_v1_0 at 2.
tells tCPA that only the second occurrence of 0 should be rewritten. The goal then becomes:
n : nat
============================
fib_v1 n = visit_fib_v2 n (fib_v1 1) (fib_v1 0)
as desired.
Negating a logical statement A is written ~A, which is syntactic sugar for A -> False. And the negation of a Leibniz equality, i.e., not (e1 = e2) is sugared into e1 <> e2.
To visualize all the syntactic sugar currently in place, type:
Print Visibility.
Here are two Propositions:
Proposition this_one :
forall (V : Type)
(v1 v2 : V),
(v1, v2) <> (v2, v1).
Proof.
Abort.
Proposition that_one :
exists (V : Type)
(v1 v2 : V),
(v1, v2) <> (v2, v1).
Proof.
Abort.
Do they both hold? Does neither hold? Or if only one of them holds, which one is it?
Created [22 Feb 2024]