Garder la trace de « l'état » lors de l'écriture des preuves d'égalité qui sont de longues chaînes d'étapes liées transitive

Question

j'écrivais la preuve suivante: 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 

Mais bien sûr, ce n'est pas vraiment ce que je l'ai écrit. Ce que j'écrit est plutôt ceci:

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 

Si je devais écrire ceci dans Agda, je pouvais utiliser le module ≡-Reasoning de garder une trace de l'endroit où je suis; par exemple, ce qui précède peut être fait comme celui-ci (en omettant les étapes de preuve réelle, car ils seraient exactement les mêmes):

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 

Est-il possible de le faire de la même à Idris?

(Note: bien sûr, dans Agda, je ne prouverais pas cela: j'utiliserais simplement le solveur de semi- fini et j'en ferais, mais le solveur de semis d'Idris à https://github.com/FranckS/RingIdris semble cibler Idris 0.11 et I 'm using 1.1.1 ...)

Answer 1

the est votre ami, et évite le besoin de tous les commentaires. Utilisez également let pour que l'épreuve puisse avancer dans une direction vers l'avant.

Je ne pouvais pas facilement réécrire votre exemple (parce que je n'ai pas toutes les lemmes disponibles), voici donc mon exemple de code, qui compile avec succès (avec deux trous parce que je l'ai laissé les preuves de plus_assoc et 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