Monomorphize Tactic

Stream: metaprogramming / tactics

[One An]

New monomorphize tactic

@Chase Norman and I developed monomorphize, a new tactic which eliminates typeclass instances from a goal.
It comes pre-packaged with Canonical, and powers its new support for typeclass instance.

In this example, add_comm is specialized to Nat, since the problem is about natural numbers.

import Canonical

example (x y : Nat) : x + y = y + x := by
  monomorphize -canonicalize [add_comm]
  /-
  add_comm_0 : ∀ (a b : ℕ), a + b = b + a
  ⊢ x + y = y + x
  -/

If canonicalize is enabled, all operations involving instances will be replaced with specialized versions.

example (n : Nat) (z : Int) : n + z = n * z := by
  monomorphize
  /-
  HAdd_hAdd_0 : ℤ → ℤ → ℤ
  Nat_cast_0 : ℕ → ℤ
  HMul_hMul_0 : ℤ → ℤ → ℤ
  ⊢ HAdd_hAdd_0 (Nat_cast_0 n) z = HMul_hMul_0 (Nat_cast_0 n) z
  -/

If there are multiple matching instances for a type class, all possible monomorphizations will be generated.

example (x : Nat) (a b : ℝ) : ↑(x + 10) = a + b := by
  monomorphize [add_comm]
  /-
  add_comm_0 : ∀ (a b : ℕ), HAdd_hAdd_0 a b = HAdd_hAdd_0 b a
  add_comm_1 : ∀ (a b : ℝ), HAdd_hAdd_1 a b = HAdd_hAdd_1 b a
  HAdd_hAdd_1 : ℝ → ℝ → ℝ
  HAdd_hAdd_0 : ℕ → ℕ → ℕ
  Nat_cast_0 : ℕ → ℝ
  OfNat_ofNat_0 : ℕ → ℕ
  ⊢ Nat_cast_0 (HAdd_hAdd_0 x (OfNat_ofNat_0 10)) = HAdd_hAdd_1 a b
  -/

Instances with parameters have their parameters propagated to the monomorphized symbol.

example (α : Type) (n : Nat) (v : Vector α n) : v ++ v = v ++ v := by
  monomorphize
  /-
  HAdd_hAdd_0 : ℕ → ℕ → ℕ
  HAppend_hAppend_0 : (α : Type) → (n m : ℕ) → Vector α n → Vector α m → Vector α (HAdd_hAdd_0 n m)
  ⊢ HAppend_hAppend_0 α n n v v = HAppend_hAppend_0 α n n v v
  -/

example (n : Nat) (x y : ZMod n) : x + y = x + y := by
  monomorphize [add_comm]
  /-
  add_comm_0 : ∀ (x_0 : ℕ) (a b : ZMod x_0), HAdd_hAdd_0 x_0 a b = HAdd_hAdd_0 x_0 b a
  HAdd_hAdd_0 : (n : ℕ) → ZMod n → ZMod n → ZMod n
  ⊢ HAdd_hAdd_0 n x y = HAdd_hAdd_0 n x y
  -/

Instances can come from the local context.

example (X : Type*) [Field X] (x : X) : x^2 = x*x := by
  monomorphize [pow_two]
  /-
  pow_two_0 : ∀ (a : X), HPow_hPow_0 a (OfNat_ofNat_0 2) = HMul_hMul_0 a a
  HMul_hMul_0 : X → X → X
  OfNat_ofNat_0 : ℕ → ℕ
  HPow_hPow_0 : X → ℕ → X
  ⊢ HPow_hPow_0 x (OfNat_ofNat_0 2) = HMul_hMul_0 x x
  -/

example (X : Type) [Inhabited X] : X := by
  monomorphize [default]
  /-
  Inhabited_default_0 : X
  ⊢ X
  -/

Instances that are not found by other means can by generated by synthInstance

#check zpowRec -- {G : Type} [One G] [Mul G] [Inv G] : (ℕ → G → G) → ℤ → G → G
example (a b : ℚ) : a * b = a * b := by
  monomorphize [zpowRec]
  /-
  zpowRec_0 : (ℕ → ℚ → ℚ) → ℤ → ℚ → ℚ
  HMul_hMul_0 : ℚ → ℚ → ℚ
  ⊢ HMul_hMul_0 a b = HMul_hMul_0 a b
  -/

Bonus:

example : (10 : ℝ) = 10 := by
  monomorphize
  /-
  OfNat_ofNat_1 : ℕ → ℕ
  OfNat_ofNat_0 : ℕ → ℝ
  ⊢ OfNat_ofNat_0 (OfNat_ofNat_1 8) = OfNat_ofNat_0 (OfNat_ofNat_1 8)
  -/

[Yaël Dillies]

Stupid remark: Isn't the verb for "making things canonical" canonize instead of canonicalize?

[Alok Singh]

I had the same remark for Mario in some PR =)

[(deleted)]

Yaël Dillies said:

Stupid remark: Isn't the verb for "making things canonical" canonize instead of canonicalize?

Canonize doesn't mean to normalize. Canonicalize on the other hand does mean to normalize.

[Chase Norman]

To me, canonize means to add into the canon. Perhaps there is an entirely different name that makes more sense.