Life after the midterm project¶

Now that the midterm project is over, the restriction of applying lemmas to all their arguments is lifted. So for example, rather than writing:

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.

Dana: And welcome in these lecture notes. We haven’t seen you lately.

The fourth wall: Well, the Hilbert Hotel is a busy place.

Alfrothul: So... Let’s not provide arguments to the fold-unfold lemmas:

Restart.

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

Alfrothul: Yup, 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: And that may or may not be a good idea, if the situation is more complicated. But yes, here it works fine.

Anton: May I?

Bong-sun: By all means.

Anton: Let’s see:

- rewrite ->2 fold_unfold_add_S.
  rewrite -> IHi'.
  rewrite -> fold_unfold_add_S.
  reflexivity.

Anton: Yup, that works too.

The fourth wall: May I?

Anton: By all means.

The fourth wall: 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:

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)).

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