Keeping track of "state" when writing equality proofs that are long chains of transitively linked steps

Question

I was writing the following proof in Idris:

  n : Nat
  n = S (k + k)

  lemma:  n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
  lemma = sym $
    rewrite plusZeroRightNeutral ((k * n) + k) in
    rewrite plusAssociative ((k * n) + k) 1 ((k * n) + k) in
    rewrite plusCommutative ((k * n) + k) 1 in
    rewrite mult2 ((k * n) + k) in
    rewrite multDistributesOverPlusRight 2 (k * n) k in
    rewrite multAssociative 2 k n in
    rewrite sym (mult2 k) in
    rewrite plusCommutative ((k + k) * n) (k + k) in
    Refl

But of course that's not really what I wrote. What I wrote instead is this:

  lemma:  n * n = ((k * n) + k) + (1 + (((k * n) + k) + 0))
  lemma = sym $
    -- ((k * n) + k) + (1 + ((k * n) + k) + 0) =
    rewrite plusZeroRightNeutral ((k * n) + k) in
    -- ((k * n) + k) + (1 + (k * n) + k) =
    rewrite plusAssociative ((k * n) + k) 1 ((k * n) + k) in
    -- (((k * n) + k) + 1) + (k * n) + k) =
    rewrite plusCommutative ((k * n) + k) 1 in
    -- 1 + ((k * n) + k)) + ((k * n) + k) =
    rewrite mult2 ((k * n) + k) in
    -- 1 + 2 * ((k * n) + k) =
    rewrite multDistributesOverPlusRight 2 (k * n) k in
    -- 1 + 2 * (k * n) + 2 * k
    rewrite multAssociative 2 k n in
    -- 1 + (2 * k) * n + 2 * k =
    rewrite sym (mult2 k) in
    -- 1 + (k + k) * n + (k + k) =
    rewrite plusCommutative ((k + k) * n) (k + k) in
    -- (k + k) * n + (1 + k + k) =
    -- (k + k) * n + n =
    -- (1 + k + k) * n =
    -- n * n
    Refl

If I were writing this in Agda, I could use the ≡-Reasoning module to keep track of where I am; for example, the above can be done like this (omitting the actual proof steps, since they'd be exactly the same):

lemma : ((k * n) + k) + (1 + (((k * n) + k) + 0)) ≡ n * n
lemma =
  begin
    ((k * n) + k) + (1 + (((k * n) + k) + 0)) ≡⟨ {!!} ⟩
    ((k * n) + k) + (1 + (((k * n) + k)))     ≡⟨ {!!} ⟩
    ((k * n) + k) + 1 + ((k * n) + k)         ≡⟨ {!!} ⟩
    1 + ((k * n) + k) + ((k * n) + k)         ≡⟨ {!!} ⟩
    1 + 2 * ((k * n) + k)                     ≡⟨ {!!} ⟩
    1 + 2 * (k * n) + 2 * k                   ≡⟨ {!!} ⟩
    1 + (2 * k) * n + 2 * k                   ≡⟨ {!!} ⟩
    1 + (k + k) * n + (k + k)                 ≡⟨ {!!} ⟩
    (k + k) * n + (1 + k + k)                 ≡⟨⟩
    (k + k) * n + n                           ≡⟨ {!!} ⟩
    n + (k + k) * n                           ≡⟨⟩
    (1 + k + k) * n                           ≡⟨⟩
    n * n
  ∎
  where
    open ≡-Reasoning

Is there a way to do similarly in Idris?

(Note: of course, in Agda I wouldn't hand-prove this: I'd just use the semiring solver and be done with it; but the Idris semiring solver at https://github.com/FranckS/RingIdris seems to be targeting Idris 0.11 and I'm using 1.1.1...)

Unrelated but `_≡⟨ refl ⟩_` is `_≡⟨⟩_`. – gallais Oct 04 '17 at 11:09 — gallais, Oct 04 '17 at 11:09
@gallais thanks I didn't know about that one! – Cactus Oct 04 '17 at 11:11 — Cactus, Oct 04 '17 at 11:11

score 4 · Accepted Answer · answered Oct 05 '17 at 07:21

the is your friend, and avoids the need for any comments. Also use let so that the proof can proceed in a forwards direction.

I couldn't easily rewrite your example (because I didn't have all the lemmas available), so here is my own code example, which successfully compiles (with two holes because I've left out the proofs of plus_assoc and plus_comm):

%default total

plus_assoc : (x : Nat) -> (y : Nat) -> (z : Nat) -> (x + y) + z = x + (y + z)

plus_comm : (x : Nat) -> (y : Nat) -> x + y = y + x

abcd_to_acbd_lemma : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> 
                (a + b) + (c + d) = (a + c) + (b + d)
abcd_to_acbd_lemma a b c d = 
    let e1 = the ((a + b) + (c + d) = ((a + b) + c) + d) $ sym (plus_assoc (a + b) c d)
        e2 = the (((a + b) + c) + d = (a + (b + c)) + d) $ rewrite (plus_assoc a b c) in Refl
        e3 = the ((a + (b + c)) + d = (a + (c + b)) + d) $ rewrite (plus_comm b c) in Refl
        e4 = the ((a + (c + b)) + d = ((a + c) + b) + d) $ rewrite (plus_assoc a c b) in Refl
        e5 = the ((((a + c) + b) + d) = (a + c) + (b + d)) $ plus_assoc (a + c) b d
    in trans e1 $ trans e2 $ trans e3 $ trans e4 e5

Keeping track of "state" when writing equality proofs that are long chains of transitively linked steps

1 Answers1