Idris2でn + k = k + nを証明する

succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n

が解きたい。

kat0

succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n
succNIsNPlus Z Z = Refl

これはいいはず。。。
コンパイルすると、

Error: succNIsNPlus is not covering.

pwgen:23:1--23:55
 23 | succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Missing cases:
    succNIsNPlus 0 (S _)
    succNIsNPlus (S _) _

って教えてくれた。

kat0

succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n
succNIsNPlus Z Z = Refl
succNIsNPlus Z (S k) = ?succNIsNPlus_rhs
succNIsNPlus (S n) _ = ?succNIsNPlus_rhs1

これでコンパイル通った!
ホールを2箇所埋めよう。

kat0

succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n
succNIsNPlus Z Z = Refl
succNIsNPlus Z (S k) =
  rewrite succNIsNPlus Z k in
  Refl
succNIsNPlus (S n) _ = ?succNIsNPlus_rhs1

kをZになるまで?再帰的に渡していく。

Error: While processing right hand side of succNIsNPlus. Can't
solve constraint between: plus k 0 and k.

pwgen:27:3--27:7
 23 | succNIsNPlus : (n : Nat) -> (k : Nat) -> n + k = k + n
 24 | succNIsNPlus Z Z = Refl
 25 | succNIsNPlus Z (S k) =
 26 |   rewrite succNIsNPlus Z k in
 27 |   Refl

。。。;(