在编写作为传递链接步骤的长链的相等性证明时跟踪 "state"

Question

我在 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

当然那不是我写的。我写的是这样的：

  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

如果我在 Agda 中编写此代码，我可以使用 ≡-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

有没有办法在 Idris 中做类似的事情？

（注意：当然，在 Agda 中我不会手动证明这一点：我只会使用半环求解器并完成它；但是 https://github.com/FranckS/RingIdris 处的 Idris 半环求解器似乎是针对 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

在编写作为传递链接步骤的长链的相等性证明时跟踪 "state"

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

proof

agda

idris

equational-reasoning