🙌
Leanパズル【解答編】「隣接要素について連鎖」を反転
この記事は、以下のパズルの解答編です。
回答例
いきなり回答例を載せると、こんな感じです。
variable {α : Type}
/-- リストの連接要素に対して、二項関係 `R` が成り立つ。
たとえば `IsChain R [a, b, c] ↔ R a b ∧ R b c` が成立する。 -/
@[grind]
inductive IsChain (R : α → α → Prop) : List α → Prop
/-- 空リストに対しては常に成立する -/
| nil : IsChain R []
/-- 要素が一つだけのリストに対しては常に成立する -/
| single (a : α) : IsChain R [a]
/-- `IsChain` の定義の再帰的な部分。
`R a b` かつ `IsChain R (b :: l)` ならば、 `IsChain R (a :: b :: l)` が成立する。-/
| cons_cons {a b : α} {l : List α} (hab : R a b) (hchain : IsChain R (b :: l)) :
IsChain R (a :: b :: l)
variable {R : α → α → Prop}
/-- `IsChain`の定義を再帰関数として書き直したもの -/
def IsChainRec (R : α → α → Prop) (xs : List α) : Prop :=
match xs with
| [] => True
| [_] => True
| a :: b :: l => R a b ∧ IsChainRec R (b :: l)
@[grind =]
theorem IsChain.append_two_iff {a b : α} {l : List α} :
IsChain R (l ++ [a, b]) ↔ IsChain R (l ++ [a]) ∧ R a b := by
induction l using IsChainRec.induct with grind
theorem IsChain.reverse {l : List α} :
IsChain R l ↔ IsChain (fun a b => R b a) (l.reverse) := by
induction l using IsChainRec.induct with grind
解説
ポイントは以下の２点かなと思います。
- ヒントでも示唆していたように、
l ++ [a, b]という形のリストに対してIsChainがどのように振る舞うかという補題が何かあった方がいいと思います。 - 帰納的述語
IsChainは通常のリストに対する帰納法とは異なる方法で定義されているため、IsChainRecという再帰関数を定義しています。こうするとIsChainRecに対して自動生成される帰納法の原理を利用することができて、自前で帰納法の原理を定義する手間が省けます。
IsChainRec.induct のようなものを使わなくてもできます。たとえば、以下のような感じですね。IsChain.cons 定理で場合分けを使っていますが、grind は賢いので勝手にケース分割をやってくれます。
@[grind =]
theorem IsChain.cons {a : α} {l : List α} :
IsChain R (a :: l) ↔
match l with
| [] => True
| b :: bs => R a b ∧ IsChain R (b :: bs) := by
grind
@[grind =]
theorem IsChain.append_two_iff {a b : α} {l : List α} :
IsChain R (l ++ [a, b]) ↔ IsChain R (l ++ [a]) ∧ R a b := by
induction l with
| nil => grind
| cons hd tl ih =>
cases tl <;> grind
theorem IsChain.reverse {l : List α} :
IsChain R l ↔ IsChain (fun a b => R b a) (l.reverse) := by
induction l with grind
Discussion