Life after the midterm project¶

The midterm project is over, and so let us lift the restriction of applying lemmas to all their arguments. Consider proving that addition is associative, for example. Here how we did it so far, a routine induction that does not use the Light of Inductil:

Definition fold_unfold_add_O := Nat.add_0_l.
Definition fold_unfold_add_S := plus_Sn_m.

Proposition add_assoc :
  forall i j k : nat,
    i + (j + k) = (i + j) + k.
Proof.
  intros i j k.
  induction i as [ | i' IHi'].
  - rewrite -> (fold_unfold_add_O (j + k)).
    rewrite -> (fold_unfold_add_O j).
    reflexivity.
  - rewrite -> (fold_unfold_add_S i' (j + k)).
    rewrite -> (fold_unfold_add_S i' j).
    rewrite -> IHi'.
    rewrite -> (fold_unfold_add_S (i' + j) k).
    reflexivity.

The fourth wall: May we?

Mimer: Of course.

Interlude¶

Bong-sun: Thanks, Fourth Wall.

The fourth wall: You are most welcome.

Alfrothul: Let us restart the proof up to the base case:

Restart.

intros i j k.
induction i as [ | i' IHi'].
-

Anton: And let’s not provide arguments to the fold-unfold lemma. Instead of writing rewrite -> (fold_unfold_add_O (j + k))., let’s write rewrite -> fold_unfold_add_O.

Alfrothul: And Instead of writing rewrite -> (fold_unfold_add_O j)., let’s write rewrite -> fold_unfold_add_O.

Pablito (diligent): Let me try, let me try:

rewrite -> fold_unfold_add_O.
rewrite -> fold_unfold_add_O.
reflexivity.

Halcyon (to himself): Looks like it works.

Bong-sun: May I?

Alfrothul: By all means.

Bong-sun: Let’s see. We are rewriting the same tactic twice in a row, so why don’t we make that explicit:

Restart.

intros i j k.
induction i as [ | i' IHi'].
- rewrite ->2 fold_unfold_add_O.
  reflexivity.

Dana: Right. That works too.

Mimer (the voice of reason): And that may or may not be a good idea, if the situation is more complicated. But yes, here it works fine.

Pablito: May I?

Bong-sun: By all means.

Pablito: Let’s see. Rather than writing rewrite -> (fold_unfold_add_S i' (j + k))., I write rewrite -> fold_unfold_add_S., and rather than writing rewrite -> (fold_unfold_add_S i' j)., I also write rewrite -> fold_unfold_add_S.. But then I am writing rewrite -> fold_unfold_add_S. twice in a row, so:

- rewrite ->2 fold_unfold_add_S.

Pablito (continuing): Yep, that works. Now rewriting the induction hypothesis doesn’t change:

rewrite -> IHi'.

Pablito (ending): And rather than writing rewrite -> (fold_unfold_add_S (i' + j) k)., I write rewrite -> fold_unfold_add_S. and I complete the proof:

rewrite -> fold_unfold_add_S.
reflexivity.

Halcyon (still to himself): It all seems to work.

The fourth wall: May I?

Pablito: By all means.

The fourth wall: It’s about the last rewrite. Let’s see:

Restart.

intros i j k.
induction i as [ | i' IHi'].
- rewrite ->2 fold_unfold_add_O.
  reflexivity.
- rewrite ->2 fold_unfold_add_S.
  rewrite -> IHi'.
  Check (fold_unfold_add_S (i' + j) k).

Bong-sun (helpfully): The *response* window reads:

fold_unfold_add_S (i' + j) k
     : S (i' + j) + k = S (i' + j + k)

The fourth wall: Right. Swapping the two sides of this Leibniz equality:

Check (eq_sym (fold_unfold_add_S (i' + j) k)).

Bong-sun: Aha. The *response* window reads:

eq_sym (fold_unfold_add_S (i' + j) k)
     : S (i' + j + k) = S (i' + j) + k

Halcyon: ...which is the goal.

The fourth wall: Exactly:

  exact (eq_sym (fold_unfold_add_S (i' + j) k)).
Qed.

Everybody claps their hands (even Mimer, if you can believe that).