The goal of this lecture note is to study proofs by cases and the language support provided by tCPA to carry them out.
In a nutshell, this language support is the ; infix operator between two tactics t1 and t2 to carry them both in one proof step. More precisely, writing t1; t2 has the effect of applying t2 to each of the subgoals generated by t1. One can also specify a choice of tactics in the stead of t2, e.g., (t2a || t2b || ... || t2z): tCPA will then try each of them in turn until one works out or until none does.
The running example of this lecture note is Chantal Keller, Damien Pous and Sylvain Chevillard’s formal study of isometries of the equilateral triangle.
Let us formalize clockwise rotations:
Inductive Rotation : Type :=
R000 : Rotation (* 0 degrees (identity) *)
| R120 : Rotation (* 120 degrees *)
| R240 : Rotation. (* 240 degrees *)
So, writing ABC clockwise for the equilateral triangle whose North vertex (at the top) is A, whose South-East vertex (at the bottom right) is B, and whose South-West vertex (at the bottom left) is C,
Pablito: Now is a pretty good time to make a drawing.Bong-sun: Lemmesee. ABC is drawn clockwise.Mimer: Yup. And it is rotated clockwise too.
Let us formalize reflections:
Inductive Reflection : Type :=
S_NN : Reflection (* North, at the top *)
| S_SE : Reflection (* South-East, at the bottom right *)
| S_SW : Reflection. (* South-West, at the bottom left *)
Again, writing ABC for the equilateral triangle whose North vertex (at the top) is A, whose South-East vertex (at the bottom right) is B, and whose South-West vertex (at the bottom left) is C,
Pablito: Now is a pretty good time to make another drawing.Halcyon: Yup.
The following function composes two rotations, clockwise (“RaR” stands for “a Rotation after a Rotation”):
Definition RaR (r2 r1: Rotation) : Rotation :=
match r1 with
R000 => match r2 with
R000 => R000
| R120 => R120
| R240 => R240
end
| R120 => match r2 with
R000 => R120
| R120 => R240
| R240 => R000
end
| R240 => match r2 with
R000 => R240
| R120 => R000
| R240 => R120
end
end.
Let us prove that R000 is neutral for RaR on the left:
Proposition R000_is_neutral_for_RaR_on_the_left :
forall r : Rotation,
RaR R000 r = r.
Proof.
We can start the proof by picking a name for a rotation (say, r), using the intro tactic, and then distinguishing three cases, one for each possible rotation, using the destruct tactic:
intro r.
destruct r as [ | | ].
Or alternatively we can use the language support provided by tCPA and skip the naming step:
Restart.
intros [ | | ].
Each of the subgoals is proved by (1) inlining the call to RaR using the unfold tactic, which is unproblematic since RaR is not defined recursively, and (2) using the reflexivity tactic since tCPA has simplified away the two nested match-expressions in the definition of RaR as it inlined its call:
- unfold RaR.
reflexivity.
- unfold RaR.
reflexivity.
- unfold RaR.
reflexivity.
The proofs of each subgoal is identical. TCPA provides language support for this kind of situation with the infix notation ; (read: semi-colon): writing t1; t2 has the effect to carry out the proof step associated with t1 and then t2 to each of the subgoals generated by t1.
So here, since all the steps in the proofs of the subgoals start with unfold RaR, we can factor the unfolding step into the previous proof step:
Restart.
intros [ | | ]; unfold RaR.
- reflexivity.
- reflexivity.
- reflexivity.
By the same token, we can also factor the reflexivity step into the previous step:
Restart.
intros [ | | ]; unfold RaR; reflexivity.
So the proof of the proposition is a one-liner, thanks to tCPA that exhaustively enumerates all the cases.
Likewise, we can prove that R000 is neutral for RaR on the right with a proof in one line:
Proposition R000_is_neutral_for_RaR_on_the_right :
forall r : Rotation,
RaR r R000 = r.
Proof.
intros [ | | ]; unfold RaR; reflexivity.
Qed.
So far we have used the reflexivity tactic when the goal is an equality whose left-hand side and right-hand side are syntactically identical.
However, there is more to this tactic than this simple characterization: prior to carrying out the comparison, tCPA also simplifies the left-hand side and the right-hand side in the same manner as it simplified the two nested match-expressions above when we inlined to call to RaR. The simplifications carried out by tCPA also includes replacing names by their denotations.
In other words, there is no need for the unfold proof step before using the reflexivity tactic, and the two proofs above can be written more concisely as follows:
Proposition R000_is_neutral_for_RaR_on_the_left :
forall r : Rotation,
RaR R000 r = r.
Proof.
intros [ | | ]; reflexivity.
Qed.
Proposition R000_is_neutral_for_RaR_on_the_right :
forall r : Rotation,
RaR r R000 = r.
Proof.
intros [ | | ]; reflexivity.
Qed.
Danger, Will Robinson! What was gained in concision was lost in understandability. We just went from “What we see is what we get” to “We don’t see what we get” and we become in danger of not getting what we see, if we see it at all.
You’ve been warned.—Loki
This situation is an illustration of Arthur C. Clarke‘s third law: any sufficiently advanced technology is indistinguishable from magic.
Later in the accompanying file, one comes across the following lemma and its 216 (two hundred and sixteen) cases:
Lemma composing_an_isomorphism_is_injective_on_the_right :
forall i x y : Isomorphism,
C i x = C i y -> x = y.
Proof.
intros [[ | | ] | [ | | ]]
[[ | | ] | [ | | ]]
[[ | | ] | [ | | ]]
H_C.
Each of these cases is either proved using the reflexivity tactic or by applying discriminate to H_C.
TCPA offers language support for this enumeration in that when writing t1; t2, we can specify a choice of tactics in the stead of t2, e.g., (t2a || t2b || ... || t2z): tCPA will then try each of them in turn until one works out or until none does.
In the present case, the proof goes through with the following one-liner:
Restart.
intros [[ | | ] | [ | | ]]
[[ | | ] | [ | | ]]
[[ | | ] | [ | | ]]
H_C; (reflexivity || discriminate H_C).
Qed.
As mentioned earlier, tCPA goes through the 216 subcases, one after each other, trying to prove them first with reflexivity and then with discriminate H_C if the reflexivity tactic failed.
Complete the remaining proofs in the accompanying file.
The learning goal of this exercise is not solely to tuck your head under your arm and prove stuff using brute force by letting tCPA enumerate all possible cases: it is also to prove things as corollaries of other things, as in Proposition C_over_rotations_is_nilpotent_with_order_3 which can either be proved by exhaustive enumeration or as a corollary of RaR_is_nilpotent_with_order_3.