congr

「f₁ = f₂ かつ a₁ = a₂ ならば f₁ a₁ = f₂ a₂」という事実は、等号が合同(congruence)関係であると解釈できますが、congr はこれを使ってゴールを分解するタクティクです。

congr は、⊢ f as = f bs という形のゴールがあったときに、ゴールを ⊢ as = bs に変えます。再帰的に適用されるので、⊢ g (f as) = g (f bs) という形のゴールでも ⊢ as = bs というゴールになります。

variable (X : Type) (x : Int) (f : Int → Int)

example (h : x = 0) : f (2 + x) = f 2 := by
  congr
  show 2 + x = 2

  simp [h]

congr は等号以外の関係は扱えません。等号以外の関係の合同性も扱えるタクティクに gcongr があります。

variable (a b : Int)

example (h : a = b) : a + 1 = b + 1 := by
  -- 等号の場合はOK
  congr

example (h : a < b) : a + 1 < b + 1 := by
  -- 不等号の場合エラーにはならないが何も起こらない
  congr
  show a + 1 < b + 1

  exact Int.add_lt_add_right h 1

再帰の深さの調節

congr が適用される再帰の深さを引数として渡すことができます。これは、主に単に congr とするだけだと「行き過ぎ」になるときに調整する目的で使用されます。

example (g : Int → X) (h : x = 0) (hf : ∀ x, f x = f (- x)) :
    g (f (2 + x)) = g (f (- 2)) := by

  -- congr の再帰がアグレッシブすぎて上手くいかないことがある
  try
    congr

    -- 分解しすぎた
    show 2 + x = -2

    -- これでは示すことができない
    fail

  -- 再帰の深さを数値として指定できる
  congr 1

  -- ちょうどよい分解になった
  show f (2 + x) = f (-2)

  simp only [h, Nat.add_zero]
  exact hf _