10 Minute Vim!

Darkest Proof: Day 3

· Read in about 2 min · (220 Words)

Day three working through Software Foundations with Coq. Since I like to rant, and I love Darkest Dungeon, ENTER THE DARKEST PROOF. (Please don’t sue me!)

I am trying to prove a helper proof to use to rewrite another helper proof to use to rewrite another proof for the commutativity of multiplication. You can’t make this stuff up.

I just need to prove this where S n is n + 1:

m * S n = m + m * n.

Should be simple…

Theorem mult_comm_lemma : forall n m, m * S n = m + m * n.
Proof.
  intros m n.
  induction m as [| p].

Gives me:

2 subgoals, subgoal 1 (ID 291)
  n * 1 = n + n * 0

subgoal 2 (ID 295) is:
 n * S (S p) = n + n * S p

Wat.

I expected performing an induction on m to produce something like this:

2 subgoals, subgoal 1 (ID 291)
   0 * S n = 0 + 0 * n

subgoal 2 (ID 294) is:
 S p * S n = S p + S p * n

Instead it is inducting n?!

Wait.

No.

WHY?!

INTROS OVERWRITES THE NAMES IF PUT IN THE WRONG ORDER?!

The poor caretaker, I fear his long-standing duties here have… affected him

steve shogren

software developer, manager, author, speaker

my books:

posts for: