grind_pattern

grind_pattern コマンドは、定理を grind タクティクに再利用させるためのパターンを指定するコマンドです。

/-- 何らかの二項関係 -/
opaque R : Nat → Nat → Prop

/-- R は推移的 -/
axiom Rtrans {x y z : Nat} : R x y → R y z → R x z

-- ローカルコンテキストに `R x y` と `R y z` が現れたとき、
-- `Rtrans` をインスタンス化しなさいと grind に指示している
grind_pattern Rtrans => R x y, R y z

example (x y z : Nat) (h₁ : R x y) (h₂ : R y z) : R x z := by
  -- grind で証明できる
  grind

[grind] 属性では登録できない例

多くの場合、わざわざ grind_pattern コマンドでパターンを手動指定しなくても [grind] 属性にパターンを自動で推測させることができますが、自動推測に失敗することがあります。このような場合は grind_pattern コマンドでパターンを明示する必要があります。

variable {α : Type}

/-- 二項関係 `R` がリストの隣接要素に対して成立するという述語。 -/
inductive IsChain (R : α → α → Prop) : List α → Prop
  | nil : IsChain R []
  | single (a : α) : IsChain R [a]
  | cons_cons {a b : α} {l : List α} (hab : R a b) (hchain : IsChain R (b :: l)) :
    IsChain R (a :: b :: l)

attribute [grind cases] IsChain
attribute [simp] IsChain.nil IsChain.single
attribute [grind <=] IsChain.cons_cons IsChain.single IsChain.nil

variable {R : α → α → Prop}

/-- リストの最後の要素を取得する。 -/
@[simp]
def last? (xs : List α) : Option α :=
  match xs with
  | [] => none
  | [a] => some a
  | _ :: b :: bs => last? (b :: bs)

theorem last?_cons_exists (xs : List α) (x : α) :
    ∃ y : α, some y = last? (x :: xs) := by
  induction xs generalizing x with simp_all

-- `[grind]` 属性は、登録すべきパターンを見つけられない。
/-
error: invalid `grind` theorem, failed to find an usable pattern using different modifiers
-/
attribute [grind] last?_cons_exists

-- `grind_pattern` コマンドなら、`last? (x :: xs)` を見たときに
-- `last?_cons_exists` を使うよう明示的に指定できる。
grind_pattern last?_cons_exists => last? (x :: xs)

@[grind =]
theorem IsChain.append {xs ys : List α} :
    IsChain R (xs ++ ys) ↔
      match last? xs, ys with
      | none, _ => IsChain R ys
      | _, [] => IsChain R xs
      | some x, b :: _ => IsChain R xs ∧ R x b ∧ IsChain R ys := by
  fun_induction last? xs with grind

ワイルドカード

パターンの中でワイルドカード _ を使用することができます。この機能は、条件を厳しすぎず緩すぎない、ちょうどよい強さに調整するのに役立ちます。

/-- 何らかの関数 -/
opaque f : Nat → Nat

/-- f は単調増加 -/
axiom f_monotone {a b : Nat} (h : a ≤ b) : f a ≤ f b

section Part1
  /- ## 厳しすぎるパターン指定の例 -/

  grind_pattern f_monotone => f a, f b, f a ≤ f b

  example (a b : Nat) (h : a ≤ b) : f a ≤ f b := by
    -- grind の中の前処理等で `f a ≤ f b` の形が崩れるため、
    -- grind が `f a ≤ f b` のパターンを見つけられない。
    -- そのため grind で証明できない
    fail_if_success grind

    apply f_monotone <;> assumption

end Part1

section Part2
  /- ## ワイルドカードでパターンを緩める例 -/

  grind_pattern f_monotone => f a, f b, f _ ≤ f _

  example (a b : Nat) (h : a ≤ b) : f a ≤ f b := by
    -- grind で証明できるようになった！
    grind

end Part2

where による制御

grind_pattern コマンドは、grind タクティクに定理を再利用させることができるという点では [grind] 属性とできることが同じですが、grind_pattern コマンドの方がより細かい制御を行えます。

典型的な例として、grind_pattern コマンドでは where で制約を追加することができ、不要なインスタンスが暴発することを防ぐことができます。

=/= 制約

=/= 制約を追加すると、両辺が definitionally equal でないときにのみ定理がインスタンス化されるようになります。

variable {α : Type} [Mul α] [One α]

/-- リストの積 -/
@[grind =]
def List.myprod (xs : List α) : α :=
  xs.foldr (· * ·) 1

-- 注意: 既に定義されているものが存在する
#check List.prod

-- α がモノイドという仮定を足す
variable [@Std.LawfulIdentity α (· * ·) 1]
variable [@Std.Associative α (· * ·)]

@[simp, grind =]
theorem List.myprod_cons (x : α) (xs : List α) :
    (x :: xs).myprod = x * xs.myprod := by
  grind

theorem List.myprod_append (xs ys : List α) :
    (xs ++ ys).myprod = xs.myprod * ys.myprod := by
  induction xs with
  | nil => grind
  | cons x xs ih =>
    simp_all [Std.Associative.assoc]

section
  -- 単に「左辺を見つけたらインスタンス化」というルールにすると...
  local grind_pattern List.myprod_append => (xs ++ ys).myprod

  /-
  trace: [grind.ematch.instance] List.myprod.eq_1: ([] ++ []).myprod = List.foldr (fun x1 x2 => x1 * x2) 1 ([] ++ [])
  [grind.ematch.instance] List.myprod_append: ([] ++ []).myprod = [].myprod * [].myprod
  [grind.ematch.instance] List.append_nil: [] ++ [] = []
  [grind.ematch.instance] List.nil_append: [] ++ [] = []
  [grind.ematch.instance] List.foldr_append: List.foldr (fun x1 x2 => x1 * x2) 1 ([] ++ []) =
        List.foldr (fun x1 x2 => x1 * x2) (List.foldr (fun x1 x2 => x1 * x2) 1 []) []
  [grind.ematch.instance] List.foldr_nil: List.foldr (fun x1 x2 => x1 * x2) 1 [] = 1
  -/
  example : ([] ++ []).myprod = 1 := by
    -- `[] ++ []` に対しても暴発して余計なインスタンス化が実行される
    set_option trace.grind.ematch.instance true in

    grind
end

-- `=/=` 制約を追加して、空リストが混ざっているときはインスタンス化しないように指示
grind_pattern List.myprod_append => (xs ++ ys).myprod where
  xs =/= []
  ys =/= []

/-
trace: [grind.ematch.instance] List.myprod.eq_1: ([] ++ []).myprod = List.foldr (fun x1 x2 => x1 * x2) 1 ([] ++ [])
[grind.ematch.instance] List.append_nil: [] ++ [] = []
[grind.ematch.instance] List.nil_append: [] ++ [] = []
[grind.ematch.instance] List.foldr_append: List.foldr (fun x1 x2 => x1 * x2) 1 ([] ++ []) =
      List.foldr (fun x1 x2 => x1 * x2) (List.foldr (fun x1 x2 => x1 * x2) 1 []) []
[grind.ematch.instance] List.foldr_nil: List.foldr (fun x1 x2 => x1 * x2) 1 [] = 1
-/
example : ([] ++ []).myprod = 1 := by
  -- `[] ++ []` に対して暴発しなくなる
  set_option trace.grind.ematch.instance true in

  grind

guard 制約

guard 制約を追加すると、与えられた条件が成り立つときにだけ定理がインスタンス化されるようになります。

grind_pattern コマンドでは様々なパターンが登録できるのですが、等式を登録することはできません。 したがって A = B が成り立つときにインスタンス化してほしい定理がある場合は、guard 制約を追加するのが良いでしょう。

theorem Nat.zero_of_divide_lt_right {a b c : Nat} (hac : c < a) (h : a * b = c) :
    b = 0 ∧ c = 0 := by
  cases b with grind

-- invalid pattern というエラーになり、登録できない
-- これは等式をパターンとして登録しようとしたため
/-
error: invalid pattern, (non-forbidden) application expected
  @Eq (Nat) (@HMul.hMul (Nat) (Nat) (Nat) (@instHMul (Nat) (instMulNat)) #4 #3) #2
-/
grind_pattern Nat.zero_of_divide_lt_right => c < a, a * b = c

-- 等式を避ければパターンとして登録できる
grind_pattern Nat.zero_of_divide_lt_right => c < a, a * b where
  guard a * b = c

/-- 割り算と剰余の定理の、一意性パート -/
theorem Int.division_with_remainder_unique {a b q r q' r' : Int} (hb : 0 < b)
    (h : a = b * q + r) (hr : 0 ≤ r) (hrb : r < b)
    (h' : a = b * q' + r') (hr' : 0 ≤ r') (hrb' : r' < b) :
    q = q' ∧ r = r' := by

  -- 両辺引いて、以下の等式を得る。
  have h_abs_eq : b.natAbs * (q - q').natAbs = (r' - r).natAbs := by
    grind only [natAbs_eq_iff_mul_eq_zero]

  -- `0 ≤ r < b` と `0 ≤ r' < b` から、`|r' - r| < b` が成り立つ
  have : (r' - r).natAbs < b.natAbs := by grind

  -- `0 < b` と `|r' - r| < b` から、`q - q' = 0` が成り立つ
  have : (q - q').natAbs = 0 := by
    -- ここで grind_pattern で登録した上記の定理を使用している
    grind only [usr Nat.zero_of_divide_lt_right]
  have q_eq_q' : q - q' = 0 := by grind

  -- さらに `r = a - b * q` と `r' = a - b * q'` より `r = r'` が成り立つ。
  have r_eq_r' : r = r' := by
    grind

  grind only

また、不等式 A ≤ B 等はパターンとしては登録できるのですが、動作が不安定になるためお勧めできません。なるべく guard 制約などとして扱うことが望ましいでしょう。

-- 整数全体を表す記号
notation:max "ℤ" => Int

/-- 絶対値。値は整数(自然数ではない) -/
def Int.abs (a : ℤ) : ℤ := max a (- a)

@[inherit_doc]
notation:max "|" a "|" => Int.abs a

/-- 0 以上の数については、絶対値は元の数に等しい -/
theorem Int.abs_of_nonneg {a : ℤ} (ha : 0 ≤ a) : |a| = a := by
  grind only [abs, = Int.max_def]

section
  -- `0 ≤ a` を探索パターンとして登録してみると
  local grind_pattern Int.abs_of_nonneg => |a|, 0 ≤ a

  -- 何故か `ha : 0 ≤ a` という仮定を見つけてくれず、
  -- `grind` で証明できない。
  example {a : ℤ} (ha : 0 ≤ a) : |a| = a := by
    fail_if_success grind
    sorry
end

-- `guard` 制約としていれてやると上手く動作する
grind_pattern Int.abs_of_nonneg => |a| where
  guard 0 ≤ a

example {a : ℤ} (ha : 0 ≤ a) : |a| = a := by
  grind