In Week 04, we saw what to do when an existential declaration occurs in the goal (namely use the exists tactic and supply a witness). But what to do when an existential declaration occurs among the assumptions?
Internally, tCPA represents existential declarations that occur among the assumptions as pairs – the name of the witness and the assumption that depends on this witness.
So we can use the destruct tactic to decompose these existential declarations into pairs. The first component of the pair is the name of the witness and the second the name of the assumption that depends on this witness.
Here is a simple example:
Lemma truism :
forall P : nat -> Prop,
(exists n : nat,
P n) ->
exists n : nat,
P n.
The proof starts as usual:
Proof.
intros P H_P.
At that point the *goals* window reads:
P : nat -> Prop
H_P : exists n : nat, P n
============================
exists n : nat, P n
We could make short work of this proof by writing exact H_P., but instead, for the sake of the illustration, let us deconstruct H_P into a pair, the first component of which is the name of the witness (n, our choice of name) and the second the name of the assumption that depends on this witness (H_Pn, our choice of name):
destruct H_P as [n H_Pn].
The *goals* window then reads:
P : nat -> Prop
n : nat
H_Pn : P n
============================
exists n0 : nat, P n0
Henk Barendregt: Ah, it’s just a naming convention.Kris Rose: A convenient one, though.Mimer: Prof. Barendregt, Dr. Rose, thanks for passing by!
Two things have happened:
The rest of the proof is smooth sailing: n is obviously the witness we are looking for, and the goal then coincides with the assumption named H_Pn:
exists n.
exact H_Pn.
As usual, the intros / destruct proof steps can be conflated into one:
intros P [n H_Pn].
exists n.
exact H_Pn.
Qed.
The rest of this chapter is dedicated to studying a series – that, as it happens, ends up to be a family – of mathematical properties of exponentiated numbers:
Fixpoint power (x n : nat) : nat :=
match n with
O =>
1
| S n' =>
x * power x n'
end.
Prove that all powers of four are post-ternary:
Property all_powers_of_4_are_post_ternary :
forall n : nat,
exists q : nat,
power 4 n = S (3 * q).
Hint: The following lemmas might come handy:
Lemma three_times_S :
forall n : nat,
3 * S n = S (S (S (3 * n))).
Lemma four_times_S :
forall n : nat,
4 * S n = S (S (S (S (4 * n)))).
Alfrothul: Well, the property is indexed by a natural number, so let’s go with an induction over n.
Bong-sun: Okeedokee. Here is the skeleton for the proof:
intro n.
induction n as [ | n' IHn'].
- rewrite -> (fold_unfold_power_O 4).
...
- rewrite -> (fold_unfold_power_S 4 n').
...
Pablito (helpful): In the base case, after using fold_unfold_power_O, the *goals* window reads:
============================
exists q : nat, 1 = S (3 * q)
Anton: How about we pick 0 as a witness:
exists 0.
Pablito: The *goals* window reads:
============================
1 = S (3 * 0)
Anton: The RHS is a constant expression, let’s compute it:
compute.
Pablito: The *goals* window reads:
============================
1 = 1
Halcyon: So we are done here. Let’s use the reflexivity tactic and focus on the induction step:
reflexivity.
- rewrite -> (fold_unfold_power_S 4 n').
Pablito: The *goals* window reads:
n' : nat
IHn' : exists q : nat, power 4 n' = S (3 * q)
============================
exists q : nat, 4 * power 4 n' = S (3 * q)
Bong-sun: Guys, the induction hypothesis is an existential.
Anton: Let’s deconstruct it into a witness and the property of this witness:
destruct IHn' as [q' H_q'].
Pablito: The *goals* window reads:
n', q : nat
H_q' : power 4 n' = S (3 * q)
============================
exists q0 : nat, 4 * power 4 n' = S (3 * q0)
Dana: Alternatively, we could anticipate and deconstruct the induction hypothesis as part of its declaration, look:
Restart.
intro n.
induction n as [ | n' [q' H_q']].
- rewrite -> (fold_unfold_power_O 4).
exists 0.
compute.
reflexivity.
- rewrite -> (fold_unfold_power_S 4 n').
Anton: Yes, we could do that.
Pablito: The *goals* window ends up the same, look:
n', q : nat
H_q' : power 4 n' = S (3 * q)
============================
exists q0 : nat, 4 * power 4 n' = S (3 * q0)
Alfrothul: Let’s get rid of power 4 n' in the goal:
rewrite -> H_q'.
Pablito: The *goals* window reads:
n', q' : nat
H_q' : power 4 n' = S (3 * q')
============================
exists q : nat, 4 * S (3 * q') = S (3 * q)
Bong-sun: OK... Somehow we need to transmogrify the quantified left-hand side into S (3 * ...).
Pablito: Well, the quantified left-hand side looks like a candidate for four_times_S, look:
rewrite -> (four_times_S (3 * q')).
Halcyon (helpful): The *goals* window reads:
n', q' : nat
H_q' : power 4 n' = S (3 * q')
============================
exists q : nat, S (S (S (S (4 * (3 * q'))))) = S (3 * q)
Anton: Now what.
Dana: How about we swap 4 and 3 in the goal?
Alfrothul: Right, some shuffling is in order:
Search (_ * (_ * _)).
Pablito: The *response* window contains a bunch of results, and I think Nat.mul_shuffle3 is our ticket, look:
Nat.mul_shuffle3: forall n m p : nat, n * (m * p) = m * (n * p)
Anton: Yes it is:
rewrite -> (Nat.mul_shuffle3 4 3 q').
Halcyon: The *goals* window reads:
n', q' : nat
H_q' : power 4 n' = S (3 * q')
============================
exists q : nat, S (S (S (S (3 * (4 * q'))))) = S (3 * q)
Pablito: Well, the quantified left-hand side now looks like a candidate for three_times_S, look:
rewrite <- (three_times_S (4 * q')).
Halcyon: The *goals* window reads:
n', q' : nat
H_q' : power 4 n' = S (3 * q')
============================
exists q : nat, S (3 * S (4 * q')) = S (3 * q)
Bong-sun: Hello, transmogrified left-hand side:
exists (S (4 * q)).
Halcyon: The *goals* window reads:
n', q' : nat
H_q' : power 4 n' = S (3 * q')
============================
S (3 * S (4 * q')) = S (3 * S (4 * q'))
Anton: So we are done:
reflexivity.
Halcyon: Indeed we are – Qed.
The following property seems obvious, considering the equalities 9 = 10 - 1, 99 = 100 - 1, and 999 = 1000 - 1, for example, but still, please prove that all powers of 10 follow a multiple of 9:
Property all_powers_of_10_follow_a_multiple_of_9 :
forall n : nat,
exists q : nat,
power 10 n = S (9 * q).
Hint: The following lemmas might come handy:
Lemma nine_times_S :
forall n : nat,
9 * S n = S (S (S (S (S (S (S (S (S (9 * n))))))))).
Lemma ten_times_S :
forall n : nat,
10 * S n = S (S (S (S (S (S (S (S (S (S (10 * n)))))))))).
Anton: Well, the proof for Exercise 02 is pretty smooth.
Bong-sun: Not just smooth, actually – it has the same structure as our first proof for Exercise 01.
The Greek chorus: EVERYBODY LOOKS BACK AT THE FIRST PROOF.
Halcyon: Guys, I just looked back at the first proof, and Bong-sun is right, it has the same structure as our first proof for Exercise 01.
Dana: Well, not just that – the properties we are asked to prove in Exercise 01 and in Exercise 02 have the same structure.
The Greek chorus: EVERYBODY LOOKS BACK AT THE TWO PROPERTIES.
Halcyon: Guys, I just looked back at the two propertioes, and Dana is right, they have the same structure.
The fourth wall: How about putting your observation to the test?
Prove that all powers of 8 follow a multiple of 7:
Property all_powers_of_8_follow_a_multiple_of_7 :
forall n : nat,
exists q : nat,
power 8 n = S (7 * q).
Anton: Well, the proof for Exercise 03 is just as smooth as the previous proofs.
Pablito: And it has the same structure too.
Anton: Yes it does.
Halcyon: And the following two lemmas did come handy:
Lemma seven_times_S :
forall n : nat,
7 * S n = S (S (S (S (S (S (S (7 * n))))))).
Lemma eight_times_S :
forall n : nat,
8 * S n = S (S (S (S (S (S (S (S (8 * n)))))))).
The fourth wall: Shall I?
Dana: By all means, Fourth Wall, by all means.
Prove that all multiples of a number are followed by a power of the successor of this number:
Property all_powers_of_Sm_follow_a_multiple_of_m :
forall m n : nat,
exists q : nat,
power (S m) n = S (m * q).
Suggestion: Proceed by induction on m and then, in the induction step, by induction on n.
Hint: The following property might come handy:
Property about_exponentiating_one :
forall n : nat,
power 1 n = 1.
Created [05 Jun 2025]