Отслеживание "состояния" при написании доказательств равенства, представляющих собой длинные цепочки транзитивно связанных шагов

Question

Я написал следующее доказательство в Идрисе:

  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

Но, конечно, это не совсем то, что я написал. Вместо этого я написал следующее:

  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

Если бы я писал это в Агде, я мог бы использовать ≡-Reasoning модуль для отслеживания того, где я нахожусь; например, вышеприведенное можно сделать следующим образом (без фактических шагов проверки, поскольку они будут точно такими же):

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

Есть ли способ сделать подобное в Идрисе?

(Примечание: конечно, в Agda я не стал бы доказывать это вручную: я бы просто использовал решатель полукольцев и покончил с этим; но решатель полуколец Idris по адресу https://github.com/FranckS/RingIdris кажется, нацеливаться на Idris 0.11, а я использую 1.1.1...)

Answer 1

the Ваш друг, и избегает необходимости каких-либо комментариев. Также используйте let так что доказательство может продолжаться в прямом направлении.

Я не мог легко переписать ваш пример (потому что у меня не было всех доступных лемм), поэтому вот мой собственный пример кода, который успешно компилируется (с двумя пробелами, потому что я оставил доказательства plus_assoc а также 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