type_check

Stream: general

[Jesse Michael Han]

i found an example where tactic.type_check seems to accept a mis-formed proof term

actually writing this out as an example causes the kernel to complain, but is there a way to get that same behavior in the tactic monad?

import data.nat.basic

meta def main : tactic unit := do {
  g ← tactic.mk_meta_var `(0 = 1),
  tactic.set_goals [g],
  ts ← tactic.read,
  `[apply multiplicative.of_add.injective, rw of_add_zero, change 1 = 1, refl],
  pf ← tactic.get_assignment g >>= tactic.instantiate_mvars,
  tactic.pp pf >>= λ x, tactic.trace format! "PROOF TERM: {x}",
  tactic.type_check pf tactic.transparency.all -- type_check succeeds??
}

#eval main

[Chris Hughes]

I'm not sure exactly what the question is, but I have certainly seen the kernel reject a tactics proof before after the goals accomplished message. e.g.

example : (0 : ℕ) = @has_zero.zero ℕ ⟨1⟩ :=
begin
  refl,
end

I've also seen it happen with induction using ... where it gets the motive wrong.

[Notification Bot]

Mario Carneiro has marked this topic as resolved.

[Notification Bot]

Mario Carneiro has marked this topic as unresolved.

[Mario Carneiro]

@Jesse Michael Han The type_check function uses the elaborator, just like unify, with the only difference being that it fails instead of unifying metavariables. It differs from the kernel, which does not understand metavariables, local constants, macros and other elaborator-specific things. Unfortunately, the elaborator's "kernel" has some soundness issues around numeral typeclasses like this, which is usually good enough for proof construction but isn't really intended for perfect theorem verification.

If you want to run the kernel, one way to do so is to create an example from a tactic. That is, create the complete proof, add a declaration to the environment, and then roll back the environment to before the addition. If the kernel fails to check the declaration then this process will fail.

[Mario Carneiro]

#eval do
  let pf : expr := expr.app `(@id ((0 : ℕ) = @has_zero.zero ℕ ⟨1⟩)) `(eq.refl (0 : ℕ)),
  tactic.type_check pf tactic.transparency.all, -- succeeds
  let us := expr.collect_univ_params pf,
  ty ← tactic.infer_type pf,
  env ← tactic.get_env,
  env.add (declaration.defn `_ us ty pf reducibility_hints.opaque ff), -- fails
  pure ()

[Jesse Michael Han]

thanks Mario! this works perfectly