The goal of this lecture note is to introduce how to prove properties about trees by structural induction, i.e., by induction over their structure.
Let us revisit polymorphic binary trees:
Inductive binary_tree (V : Type) : Type :=
Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.
This representation is both sound and complete:
This definition is inductive in that it consists of a base case (the leaves) and an induction step (the nodes): given a value, we construct a leaf with Leaf, and given two trees, we construct a new tree with Node.
Because of completeness, for any given type V, any binary tree was constructed using Leaf V and Node V, and in turn any binary tree that was constructed using Node V was constructed out of two binary trees, which themselves were constructed using Leaf V and Node V, etc., as captured in the following Gallina fragment:
match t with
Leaf _ n =>
...
| Node _ t1 t2 =>
match (t1, t2) with
(Leaf _ n1, Leaf _ n2) =>
...
| (Leaf _ n1, Node _ t21 t22) =>
...
| (Node _ t11 t12, Leaf _ n2) =>
...
| (Node _ t11 t12, Node _ t21 t22) =>
...
end
end
And so the induction principle associated with this data type, for any given type V and property P indexed with a binary tree with payloads of type V, reads as follows:
| IND | forall v : V, P (Leaf V v) | forall t1 : binary_tree V, P t1 -> forall t2 : binary_tree V, P t2 -> P (Node V t1 t2) | |
| forall t : binary_tree V, P t | |||
If a property holds for any leaf (base case), and, (induction step) assuming it holds for any two trees, it holds for the node containing these two trees (which are the induction hypotheses), then this property holds for any tree.
So in the inference rule above,
Side note: every time we define a data type in Gallina, tCPA manufactures the corresponding induction principle, naming it as the name of this data type concatenated with “_ind”. (TCPA also manufactures the corresponding fold function, but more about that later.) For example, after declaring binary_tree, we can visualize its associated induction principle using the Check command:
Check binary_tree_ind.
The *response* window then reads:
binary_tree_ind
: forall (V : Type) (P : binary_tree V -> Prop),
(forall v : V, P (Leaf V v)) ->
(forall b : binary_tree V, P b -> forall b0 : binary_tree V, P b0 -> P (Node V b b0)) ->
forall b : binary_tree V, P b
We shall come back to binary_tree_ind at the end of this chapter.
Bong-sun: So every time we declare a data type, say foo, tCPA declares foo_ind?
Dana: Yup.
Bong-sun: But what if foo_ind already exists?
Dana: Ah, that should not be possible, because names are uniquely declared in Gallina.
Bong-sun: Let’s see about that. First, we can declare foo_ind:
Definition foo_ind : nat := 0.
Pablito (obligingly): The *response* buffer reads:
foo_ind is defined
Bong-sun: Thank you. And now we declare a data type that we name foo:
Inductive foo (V : Type) : Type :=
Foo : V -> foo V.
Pablito: Ah, the *response* buffer reads:
Error: foo_ind already exists.
Dana: So no can’t do. OK, that makes sense.
Here is a specification of the mirror function over binary trees. Since binary trees are defined inductively, the specification is inductive too:
Definition specification_of_mirror (mirror : forall V : Type, binary_tree V -> binary_tree V) : Prop :=
(forall (V : Type)
(v : V),
mirror V (Leaf V v) =
Leaf V v)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
mirror V (Node V t1 t2) =
Node V (mirror V t2) (mirror V t1)).
The result of applying the mirror function to a given tree is a mirror image of the given tree.
Here is a specification of a function that counts the number of leaves in a given binary tree:
Definition specification_of_number_of_leaves (number_of_leaves : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_leaves V (Leaf V v) =
1)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_leaves V (Node V t1 t2) =
number_of_leaves V t1 + number_of_leaves V t2).
Here is a specification of a function that counts the number of nodes in a given binary tree:
Definition specification_of_number_of_nodes (number_of_nodes : forall V : Type, binary_tree V -> nat) : Prop :=
(forall (V : Type)
(v : V),
number_of_nodes V (Leaf V v) =
0)
/\
(forall (V : Type)
(t1 t2 : binary_tree V),
number_of_nodes V (Node V t1 t2) =
S (number_of_nodes V t1 + number_of_nodes V t2)).
Let us prove that a function that satisfies the specification of the mirror function is involutory, i.e., an involution:
Theorem mirror_is_involutory :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t : binary_tree V),
mirror V (mirror V t) = t.
In words: any function mirror that satisfies the specification of the mirror function has the property that applying mirror to the result of applying mirror to any given binary tree yields this binary tree.
The property is proved by structural induction over binary trees, hinging on the soundness and uniqueness of their representation.
Let us get started:
Proof.
The *goals* window reads:
1 subgoal, subgoal 1 (ID 4)
============================
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror -> forall (V : Type) (t : binary_tree V), mirror V (mirror V t) = t
The identifier of the current goal is irrelevant, so we shall ignore it. Let us name the components of the conjunction in the specification:
intro mirror.
unfold specification_of_mirror.
intros [S_Leaf S_Node].
intros V t.
The *goals* window then reads as follows (ignoring the identifier of the current goal):
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t : binary_tree V
============================
mirror V (mirror V t) = t
The induction tactic, applied to t, implements the induction principle associated with the data type of binary trees. Therefore it creates two subgoals: one for the base case, and one for the induction step. Courtesy of tCPA, we can control the names in these subgoals:
intro t.
induction t as [v | t1 IHt1 t2 IHt2].
The whole *goals* window then reads as follows:
2 subgoals, subgoal 1 (ID 19)
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
v : V
============================
mirror V (mirror V (Leaf V v)) = Leaf V v
subgoal 2 (ID 24) is:
mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
Let us focus on the base case:
-
The *goals* window then reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
v : V
============================
mirror V (mirror V (Leaf V v)) = Leaf V v
This goal is the base case, and we can connect it to the induction principle written above using the revert tactic:
- revert V v.
The *goals* window then reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
============================
forall (V : Type) (v : V), mirror V (mirror V (Leaf V v)) = Leaf V v
The current goal is an instance of the base case forall (V : Type) (v : V), P(Leaf V v), where P(Leaf V v) stands for the property we want to prove, i.e., mirror V (mirror V (Leaf V v)) = Leaf V v. As a courtesy to us, tCPA has anticipated our writing intros V v. to accelerate our proving:
intros V v.
So the *goals* window reads:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
v : V
============================
mirror V (mirror V (Leaf V v)) = Leaf V v
Part of the left-hand side of the goal is an instance of S_Leaf:
Check (S_Leaf V v).
Indeed the *response* window now reads:
S_Leaf V v
: mirror V (Leaf V v) = Leaf V v
We can thus replace mirror V (Leaf V v) by Leaf V v in the goal using the rewrite tactic from left to right:
rewrite -> (S_Leaf V v).
Indeed the *goals* window now reads:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
v : V
============================
mirror V (Leaf V v) = Leaf V v
The goal is an instance of S_Leaf:
Check (S_Leaf V v).
Indeed the *response* window now reads:
S_Leaf V v
: mirror V (Leaf V v) = Leaf V v
We can thus conclude this subgoal with this instance:
exact (S_Leaf V v).
And indeed the *response* window now reads:
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.
Alternatively to using the exact tactic, we could have used the rewrite tactic:
rewrite -> (S_Leaf V v).
The *goals* window would then read:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
v : V
============================
Leaf V v = Leaf V v
The left-hand side and the right-hand side are identical, and therefore we can prove this goal using the reflexivity tactic:
reflexivity.
Either way, the base case is now proved. Let us turn to the induction step:
-
The *goals* window reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1, t2 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
IHt2 : mirror V (mirror V t2) = t2
============================
mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
This goal is the induction step, and we can connect it to the induction principle written above using the revert tactic:
- revert IHt2.
revert t2.
revert IHt1.
revert t1.
The *goals* window then reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
============================
forall t1 : binary_tree V,
mirror V (mirror V t1) = t1 ->
forall t2 : binary_tree V, mirror V (mirror V t2) = t2 -> mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
The current goal is an instance of the induction step forall (V : Type) (t1 : binary_tree V), P(t1) -> forall (t2 : binary_tree V), P(t2) -> P(Node V t1 t2) where P(t) stands for the property we want to prove, i.e., mirror V (mirror V (Node V t1 t2)) = Node V t1 t2. As a courtesy to us, tCPA has anticipated our writing intros t1 IHt1 t2 IHt2. to accelerate our proving:
intros t1 IHt1 t2 IHt2.
So the *goals* window reads:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
t2 : binary_tree V
IHt2 : mirror V (mirror V t2) = t2
============================
mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
The left-hand side of the goal contains an instance of S_Node:
Check (S_Node V t1 t2).
Indeed the *response* window now reads:
S_Node V t1 t2
: mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
We can thus replace mirror V (Node V t1 t2) by Node V (mirror V t2) (mirror V t1) in the goal using the rewrite tactic from left to right:
rewrite -> (S_Node V t1 t2).
Indeed the *goals* window now reads:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
t2 : binary_tree V
IHt2 : mirror V (mirror V t2) = t2
============================
mirror V (Node V (mirror V t2) (mirror V t1)) = Node V t1 t2
The left-hand side of the goal contains an instance of S_Node:
Check (S_Node V (mirror V t2) (mirror V t1)).
Indeed the *response* window now reads:
S_Node V (mirror V t2) (mirror V t1)
: mirror V (Node V (mirror V t2) (mirror V t1)) = Node V (mirror V (mirror V t1)) (mirror V (mirror V t2))
We can thus replace mirror V (Node V (mirror V t2) (mirror V t1)) by Node V (mirror V (mirror V t1)) (mirror V (mirror V t2)) in the goal using the rewrite tactic from left to right:
rewrite -> (S_Node V (mirror V t2) (mirror V t1)).
And indeed the *goals* window now reads:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
t2 : binary_tree V
IHt2 : mirror V (mirror V t2) = t2
============================
Node V (mirror V (mirror V t1)) (mirror V (mirror V t2)) = Node V t1 t2
As canonical in an induction proof, let us use the induction hypothesis on t1 and the induction hypothesis on t2:
rewrite -> IHt1.
rewrite -> IHt2.
The *goals* window reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
t2 : binary_tree V
IHt2 : mirror V (mirror V t2) = t2
============================
Node V t1 t2 = Node V t1 t2
The left-hand side and the right-hand side are identical, and therefore we can prove this goal using the reflexivity tactic:
reflexivity.
This proof step completes the goal and the proof.
That being said, there is a more convenient way to write this proof:
Restart.
Indeed we do not need all the assumptions at the same time. So let us delay their naming:
intros mirror S_mirror V t.
The *goals* window now reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_mirror : specification_of_mirror mirror
V : Type
t : binary_tree V
============================
mirror V (mirror V t) = t
Let us being the induction proof, as before, and focus on the base case:
induction t as [n | t1 IHt1 t2 IHt2].
-
The *goals* window now reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_mirror : specification_of_mirror mirror
V : Type
t : binary_tree V
============================
mirror V (mirror V t) = t
We can now replace the name specification_of_mirror by its denotation in the corresponding assumption, using the extra keyword in:
- unfold specification_of_mirror in S_mirror.
The *goals* window now reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_mirror : (forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v) /\
(forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1))
V : Type
v : V
============================
mirror V (mirror V (Leaf V v)) = Leaf V v
We can then destructure the conjunction into its components, only naming the first one since the second one is irrelevant here:
destruct S_mirror as [S_Leaf _].
The *goals* window now reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Leaf : forall (V : Type) (v : V), mirror V (Leaf V v) = Leaf V v
V : Type
v : V
============================
mirror V (mirror V (Leaf V v)) = Leaf V v
(Note how S_mirror has disappeared and S_Leaf has appeared.)
We can then proceed as in the first proof and focus on the induction step:
Check (S_Leaf V v).
rewrite -> (S_Leaf V v).
Check (S_Leaf V v).
exact (S_Leaf V v).
-
The *goals* window now reads as follows:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_mirror : specification_of_mirror mirror
V : Type
t1, t2 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
IHt2 : mirror V (mirror V t2) = t2
============================
mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
We can now replace the names specification_of_mirror by its denotation in the corresponding assumption and destructure the conjunction into its components, only naming the second ones since the first one is irrelevant here:
- unfold specification_of_mirror in S_mirror.
destruct S_mirror as [_ S_Node].
The *goals* window now reads as follows, and is less cluttered than in the first proof since its assumptions only deal with nodes, not with leaves:
mirror : forall V : Type, binary_tree V -> binary_tree V
S_Node : forall (V : Type) (t1 t2 : binary_tree V), mirror V (Node V t1 t2) = Node V (mirror V t2) (mirror V t1)
V : Type
t1, t2 : binary_tree V
IHt1 : mirror V (mirror V t1) = t1
IHt2 : mirror V (mirror V t2) = t2
============================
mirror V (mirror V (Node V t1 t2)) = Node V t1 t2
The rest of the proof does not change:
Check (S_Node V t1 t2).
rewrite -> (S_Node V t1 t2).
Check (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> (S_Node V (mirror V t2) (mirror V t1)).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
As a corollary of Theorem mirror_is_involutory, prove that mirror reverses itself:
Proposition mirror_reverses_itself :
forall mirror : forall V : Type, binary_tree V -> binary_tree V,
specification_of_mirror mirror ->
forall (V : Type)
(t t' : binary_tree V),
mirror V t = t' ->
mirror V t' = t.
The accompanying resource file contains a proof of the following theorem:
Theorem about_the_relative_number_of_leaves_and_nodes_in_a_tree :
forall number_of_leaves : forall V : Type, binary_tree V -> nat,
specification_of_number_of_leaves number_of_leaves ->
forall number_of_nodes : forall V : Type, binary_tree V -> nat,
specification_of_number_of_nodes number_of_nodes ->
forall (V : Type)
(t : binary_tree V),
number_of_leaves V t = S (number_of_nodes V t).
This theorem captures that any functions number_of_leaves and number_of_nodes that satisfy each of the specifications above have the following property: for any binary tree of any shape, applying these functions to this tree yields two natural numbers that differ by 1. In words: a binary tree contains one more leaf than it contains nodes – 1 leaf and 0 node, 2 leaves and 1 node, 3 leaves and 2 nodes, etc., no matter its shape.
The proof is “routine” in that it takes the same steps as the proof above. After using the induction hypotheses, the *goals* window reads:
nol : forall V : Type, binary_tree V -> nat
S_nol_Node : forall (V : Type) (t1 t2 : binary_tree V), nol V (Node V t1 t2) = nol V t1 + nol V t2
non : forall V : Type, binary_tree V -> nat
S_non_Node : forall (V : Type) (t1 t2 : binary_tree V), non V (Node V t1 t2) = S (non V t1 + non V t2)
V : Type
t1, t2 : binary_tree V
IHt1 : nol V t1 = S (non V t1)
IHt2 : nol V t2 = S (non V t2)
============================
S (non V t1) + S (non V t2) = S (S (non V t1 + non V t2))
And we are left to do some arithmetic reasoning. To this end, let us query the libraries:
Search (S _ + _ = _).
Among the responses in the *response* window (well, there is only one here, but there would be more if we had imported the Arith library), one stands out, which we recognize as the induction step for addition when it is defined inductively over its first argument:
Check (plus_Sn_m (non V t1) (S (non V t2))).
The *response* window now reads:
plus_Sn_m (non V t1) (S (non V t2))
: S (non V t1) + S (non V t2) = S (non V t1 + S (non V t2))
We can thus replace S (non V t1) + S (non V t2) in the goal by S (non V t1 + S (non V t2)) using the rewrite tactic from left to right:
rewrite -> (plus_Sn_m (non V t1) (S (non V t2))).
And indeed the *goals* window now reads:
nol : forall V : Type, binary_tree V -> nat
S_nol_Node : forall (V : Type) (t1 t2 : binary_tree V), nol V (Node V t1 t2) = nol V t1 + nol V t2
non : forall V : Type, binary_tree V -> nat
S_non_Node : forall (V : Type) (t1 t2 : binary_tree V), non V (Node V t1 t2) = S (non V t1 + non V t2)
V : Type
t1, t2 : binary_tree V
IHt1 : nol V t1 = S (non V t1)
IHt2 : nol V t2 = S (non V t2)
============================
S (non V t1 + S (non V t2)) = S (S (non V t1 + non V t2))
Let us patiently query the libraries some more. After a few tries:
Search (_ = _ + S _).
Among the responses in the *response* window (again, there is only one here, for the aforementioned reason), one stands out, which we recognize as the induction step for addition when it is defined inductively over its second argument:
Check (plus_n_Sm (non V t1) (non V t2)).
The *response* window now reads:
plus_n_Sm (non V t1) (non V t2)
: S (non V t1 + non V t2) = non V t1 + S (non V t2)
We can thus replace non V t1 + S (non V t2) in the goal by S (non V t1 + non V t2) using the rewrite tactic from right to left:
rewrite <- (plus_n_Sm (non V t1) (non V t2)).
And indeed the *goals* window now reads:
nol : forall V : Type, binary_tree V -> nat
S_nol_Node : forall (V : Type) (t1 t2 : binary_tree V), nol V (Node V t1 t2) = nol V t1 + nol V t2
non : forall V : Type, binary_tree V -> nat
S_non_Node : forall (V : Type) (t1 t2 : binary_tree V), non V (Node V t1 t2) = S (non V t1 + non V t2)
V : Type
t1, t2 : binary_tree V
IHt1 : nol V t1 = S (non V t1)
IHt2 : nol V t2 = S (non V t2)
============================
S (non V t1 + S (non V t2)) = S (S (non V t1 + non V t2))
The left-hand side and the right-hand side are identical, and therefore we can prove this goal using the reflexivity tactic:
reflexivity.
This proof step completes the goal and the proof.
Alfrothul: Remember our first induction proof, at the beginning of this week?
Anton: Er... Yes?
Alfrothul: We used nat_ind explicitly, and then we used the induction tactic.
Anton: OK. So?
Alfrothul: Well, in the proof just above, we used the induction tactic.
Anton: Right. And since its argument was t, which is of type binary_tree V, the induction principle associated to binary trees was invoked, and off we went.
Pablito (helpfully): This induction principle is binary_tree_ind, look:
forall (V : Type)
(P : binary_tree V -> Prop),
(forall v : V, P (Leaf V v)) ->
(forall t1 : binary_tree V, P t1 -> forall t2 : binary_tree V, P t2 -> P (Node V t1 t2)) ->
forall t : binary_tree V, P t
Alfrothul: How about we re-do the proof by using binary_tree_ind explicitly?
Anton: I’m game:
Restart.
intros nol S_nol non S_non.
Check binary_tree_ind.
Pablito: The *response* window then reads:
binary_tree_ind
: forall (V : Type) (P : binary_tree V -> Prop),
(forall v : V, P (Leaf V v)) ->
(forall b : binary_tree V, P b -> forall b0 : binary_tree V, P b0 -> P (Node V b b0)) ->
forall b : binary_tree V, P b
Bong-sun: Wow, the implicit names are not very readable.
Halcyon: C’est la vie, let’s move on.
Anton: First thing first:
intro V.
Check (binary_tree_ind
V).
Pablito (dutiful): The *response* window then reads:
binary_tree_ind
: forall P : binary_tree V -> Prop,
(forall v : V, P (Leaf V v)) ->
(forall b : binary_tree V, P b -> forall b0 : binary_tree V, P b0 -> P (Node V b b0)) ->
forall b : binary_tree V, P b
Bong-sun: Let’s see. Which proposition do we want to prove by induction?
Pablito: Well, the *goals* window reads:
nol : forall V : Type, binary_tree V -> nat
S_nol : specification_of_number_of_leaves nol
non : forall V : Type, binary_tree V -> nat
S_non : specification_of_number_of_nodes non
V : Type
============================
forall t : binary_tree V, nol V t = S (non V t)
Anton: So – I am guessing here:
Check (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))).
Dana: Good guess, Anton. The *response* window reads:
binary_tree_ind V (fun t : binary_tree V => nol V t = S (non V t))
: (forall v : V, nol V (Leaf V v) = S (non V (Leaf V v))) ->
(forall b : binary_tree V,
nol V b = S (non V b) ->
forall b0 : binary_tree V, nol V b0 = S (non V b0) -> nol V (Node V b b0) = S (non V (Node V b b0))) ->
forall b : binary_tree V, nol V b = S (non V b)
Halcyon: The implicit names are not very readable, mais c’est la vie and let’s keep moving on.
Alfrothul: OK... The antecedent of the top implication is the base case, right?
Anton: Well, spotted, Alfrothul. Let’s make it a named assumption:
assert (wanted_Leaf :
forall v : V, nol V (Leaf V v) = S (non V (Leaf V v))).
Alfrothul: Thanks. Now we can just copy-paste the fragment of the proof above for the base case:
{ intro v.
unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [S_nol_Leaf _].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [S_non_Leaf _].
Check (S_non_Leaf V v).
rewrite -> (S_non_Leaf V v).
Check (S_nol_Leaf V v).
exact (S_nol_Leaf V v). }
Halcyon: Yay!
Bong-sun: Let’s see:
Check (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))
wanted_Leaf).
Pablito (celeritous): The *response* window reads:
binary_tree_ind V (fun t : binary_tree V => nol V t = S (non V t)) wanted_Leaf
: (forall b : binary_tree V,
nol V b = S (non V b) ->
forall b0 : binary_tree V, nol V b0 = S (non V b0) -> nol V (Node V b b0) = S (non V (Node V b b0))) ->
forall b : binary_tree V, nol V b = S (non V b)
Alfrothul: An implication whose goal is the current goal, that’s a job for the apply tactic:
apply (binary_tree_ind
V
(fun t : binary_tree V => nol V t = S (non V t))
wanted_Leaf).
Pablito: Well, the *goals* window reads:
nol : forall V : Type, binary_tree V -> nat
S_nol : specification_of_number_of_leaves nol
non : forall V : Type, binary_tree V -> nat
S_non : specification_of_number_of_nodes non
V : Type
wanted_Leaf : forall v : V, nol V (Leaf V v) = S (non V (Leaf V v))
============================
forall b : binary_tree V,
nol V b = S (non V b) ->
forall b0 : binary_tree V, nol V b0 = S (non V b0) -> nol V (Node V b b0) = S (non V (Node V b b0))
Anton: Ah! Never mind the implicit names, that’s the induction step.
Alfrothul: How about we copy-paste the fragment of the proof above for the induction step:
intros t1 IHt1 t2 IHt2.
unfold specification_of_number_of_leaves in S_nol.
destruct S_nol as [_ S_nol_Node].
unfold specification_of_number_of_nodes in S_non.
destruct S_non as [_ S_non_Node].
Check (S_nol_Node V t1 t2).
rewrite -> (S_nol_Node V t1 t2).
Check (S_non_Node V t1 t2).
rewrite -> (S_non_Node V t1 t2).
rewrite -> IHt1.
rewrite -> IHt2.
Search (S _ + _).
Check (plus_Sn_m (non V t1) (S (non V t2))).
rewrite -> (plus_Sn_m (non V t1) (S (non V t2))).
Search (_ + S _ = _).
Search (_ = _ + S _).
Check (plus_n_Sm (non V t1) (non V t2)).
rewrite <- (plus_n_Sm (non V t1) (non V t2)).
reflexivity.
Pablito: Guys, the *goals* window reads:
No more subgoals.
(dependent evars:)
Alfrothul: So we are done:
Qed.
Halcyon: Yay!