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

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

  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

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

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


idris proof agda equational-reasoning
person Cactus    schedule 03.10.2017    source источник
comment
Не связаны, но _≡⟨ refl ⟩_ _≡⟨⟩_.   -  person gallais    schedule 04.10.2017
comment
@gallais спасибо, я не знал об этом!   -  person Cactus    schedule 04.10.2017

Ответы (1)


arrow_upward
4
arrow_downward

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
person Philip Dorrell    schedule 05.10.2017