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

where による制御

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

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

=/= 制約

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

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

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

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

theorem List.prod_append (xs ys : List α) :
    (xs ++ ys).prod = xs.prod * ys.prod := by
  induction xs with grind

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

  /-
  trace: [grind.ematch.instance] List.prod.eq_1: ([] ++ []).prod = List.foldr (fun x1 x2 => x1 * x2) 1 ([] ++ [])
  [grind.ematch.instance] List.prod_append: ([] ++ []).prod = [].prod * [].prod
  [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 : ([] ++ []).prod = 1 := by
    -- `[] ++ []` に対しても暴発して余計なインスタンス化が実行される
    set_option trace.grind.ematch.instance true in

    grind
end

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

/--
trace: [grind.ematch.instance] List.prod.eq_1: ([] ++ []).prod = 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 : ([] ++ []).prod = 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