Check for sorry in tactic proof

Stream: metaprogramming / tactics

[Jason Rute]

Does there exist a tactic, or is there a way to write one to check that sorry hasn't been applied so far in the proof? Something like:

begin
induction n,
{sorry},
proof_is_sorry_free, -- fails
end

[Jason Rute]

cc @Stanislas Polu @Jesse Michael Han

[Scott Morrison]

src#tactic.sorry_if_contains_sorry should show you how to do this

[Scott Morrison]

I think I wrote this long again for obviously when run as an auto_param: if the user hasn't specified the relevant data fields of the structure, there's little point trying to prove the axiom fields automatically.

[Jason Rute]

So one would use docs#expr.contains_sorry to check docs#tactic.result?

[Stanislas Polu]

Hi! Following up on this thread. When considering the following example:

import data.nat.basic

theorem induction_divisibility_3divnto3m2n
  (n : ℕ) :
  3 ∣ n^3 + 2 * n :=
begin
  rw [add_comm],
  have h3 : 1 * (n + 1) ≤ (n + 1),
  rw one_mul,
  apply dvd_trans,
  swap,
  simp [],
end

The type of the resulting proof mismatches the type of the theorem despite the final tactic state being "no goals".

What would be the best way to check that the constructed proof's type matches the target goal? I presume something along the line of comparing the type of docs#tactic.result with docs#tactic.target?

[Scott Morrison]

I'm curious where this proof came from. I'd be tempted to call this a bug in simp.

[Stanislas Polu]

It's been generated by our models, which are if anything else, good fuzzers :)

[Stanislas Polu]

Is docs#tactic.type_check applied to docs#tactic.result a good path forward here? I presume it does not guard against sorry so this would have to be checked separately?

[Jannis Limperg]

type_check only makes sure that result is a well-typed term. After you've done this, you can infer_type on result, then compare that to target using is_def_eq. (infer_type without type_check is unreliable since it may return a bogus type if the term is not well-typed.) I believe you're right that none of this checks for sorry-freedom.

[Kevin Buzzard]

Oh wow, even recover does not fix this one. This is surely a bug.

[Stanislas Polu]

This is the solution I'm working on: https://github.com/openai/lean-gym/pull/5 Feedback greatly appreciated!

[Damiano Testa]

Just a silly remark: you can minimize slightly your example to

theorem induction_divisibility_3divnto3m2n
  (n : ℕ) :
  0 ∣ n :=
begin
  apply dvd_trans,
  swap,
  simp [],
end

An "advantage" of this formulation is that the conclusion is now actually false, rather than only the argument being fallacious!

[Jannis Limperg]

   src ← tactic.infer_type pf,
    tgt ← tactic.result,
    tactic.is_def_eq tgt src

I think this should be

   src ← tactic.infer_type pf,
   tgt ← tactic.target, -- !
   tactic.is_def_eq tgt src

prf is already tactic.result. Otherwise the validation logic looks good to me.

[Stanislas Polu]

Thanks a lot @Jannis Limperg

[Stanislas Polu]

Note: as we manually set the goal in the context of lean-gym we can't rely on tactic.result and tactic.target (h/t @Jason Rute). Finalized PR: https://github.com/openai/lean-gym/pull/5

If anybody has a minute to look at it, this now properly fails on the presence of sorry as well as the example above. The example above fails not on the check that the target type matches the proof term type but before due to the presence of meta variables guard (bnot pf.has_meta_var) in the proof term, but I'm still wondering if running tgt ← tactic.infer_type g where g is the meta-variable representing the top-level goal gives me the type of that initial goal or the type of the assignment of the meta-variable (in which case the final check is a no-op).

[Jason Rute]

Stanislas Polu said:

I'm still wondering if running tgt ← tactic.infer_type g where g is the meta-variable representing the top-level goal gives me the type of that initial goal or the type of the assignment of the meta-variable (in which case the final check is a no-op).

Aren't those two things the same? When you create a metavariable g with type t, then all assignments to g should have type t, no?

[Stanislas Polu]

Well if the assignment still has meta variables that seems untrue as per the example proof above?

[Jason Rute]

Oh, interesting. Ok, my guess then is that if you do infer type before instanting the metavariables, you will get the desired target.

[Stanislas Polu]

hmmm right now I infer_type on the final tactic state so the metavariable is instantiated...

[Stanislas Polu]

Let me try to get the type on the initial tactic_state and pass it to validate_proof

[Stanislas Polu]

This works as well. Let's do that as there's higher probability that it will do the right thing: Updated diff here: https://github.com/openai/lean-gym/pull/5/files

[Stanislas Polu]

Hi! Following up again on this thread, our models came up with this proof which passed our current checks:

import data.pnat.basic

theorem mathd_numbertheory_13
  (u v : ℕ+)
  (h₀ : 100 ∣ (14*u - 46))
  (h₁ : 100 ∣ (14*v - 46))
  (h₂ : u < 50)
  (h₃ : v < 100)
  (h₄ : 50 < v) :
  ((u + v):ℕ) / 2 = 64 :=
begin
  revert h₄,
  contrapose h₃,
  intro hn,
  exact not_lt_of_lt hn undefined,
end

Where can I read more about undefined and is there a canonical way to check that the resulting proof does not rely on it?

(I presume what happens is something along the lines of the last exact assigning undefined to a meta-variable left unassigned, but I'm surprised it passes the infer_type checks discussed yesterday)

[Patrick Massot]

It's defined (!) here which gets replaced by this.

[Patrick Massot]

I never met this before, and I have no idea how to detect it non-interactively

[Stanislas Polu]

But how comes running infer_type on the assignment of the top-goal meta-variable even gives something meaningful here? (I'll check what it outputs precisely to better understand what's going on).

[Stanislas Polu]

The proof indeed contains undefined:

fun (u : pnat) (v : pnat) (hu : has_dvd.dvd.{0} pnat (monoid_has_dvd.{0} pnat (right_cancel_monoid.to_monoid.{0} pnat (cancel_monoid.to_right_cancel_monoid.{0} pnat (cancel_comm_monoid.to_cancel_monoid.{0} pnat (ordered_cancel_comm_monoid.to_cancel_comm_monoid.{0} pnat pnat.ordered_cancel_comm_monoid))))) (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (has_sub.sub.{0} pnat pnat.has_sub (has_mul.mul.{0} pnat pnat.has_mul (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))) u) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) (hv : has_dvd.dvd.{0} pnat (monoid_has_dvd.{0} pnat (right_cancel_monoid.to_monoid.{0} pnat (cancel_monoid.to_right_cancel_monoid.{0} pnat (cancel_comm_monoid.to_cancel_monoid.{0} pnat (ordered_cancel_comm_monoid.to_cancel_comm_monoid.{0} pnat pnat.ordered_cancel_comm_monoid))))) (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (has_sub.sub.{0} pnat pnat.has_sub (has_mul.mul.{0} pnat pnat.has_mul (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))) v) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) (hsum : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) u (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (h : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))), (imp_of_not_imp_not (has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) ((has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))) v) -> (eq.{1} nat (has_div.div.{0} nat nat.has_div (has_add.add.{0} nat nat.has_add (coe.{1 1} pnat nat (coe_to_lift.{1 1} pnat nat (coe_base.{1 1} pnat nat coe_pnat_nat)) u) (coe.{1 1} pnat nat (coe_to_lift.{1 1} pnat nat (coe_base.{1 1} pnat nat coe_pnat_nat)) v)) (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))) (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))))))))) (fun (h : not ((has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))) v) -> (eq.{1} nat (has_div.div.{0} nat nat.has_div (has_add.add.{0} nat nat.has_add (coe.{1 1} pnat nat (coe_to_lift.{1 1} pnat nat (coe_base.{1 1} pnat nat coe_pnat_nat)) u) (coe.{1 1} pnat nat (coe_to_lift.{1 1} pnat nat (coe_base.{1 1} pnat nat coe_pnat_nat)) v)) (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one))) (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one)))))))))), (id.{0} (not (has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))))) (fun (hn : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))), (not_lt_of_lt.{0} pnat (has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid)))) (has_lt.lt.is_strict_order.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) hn (undefined.{0} (has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) v)))))) h)

But running infer_type on it does return a valid type:

Pi (u : pnat) (v : pnat) (hu : has_dvd.dvd.{0} pnat (monoid_has_dvd.{0} pnat (right_cancel_monoid.to_monoid.{0} pnat (cancel_monoid.to_right_cancel_monoid.{0} pnat (cancel_comm_monoid.to_cancel_monoid.{0} pnat (ordered_cancel_comm_monoid.to_cancel_comm_monoid.{0} pnat pnat.ordered_cancel_comm_monoid))))) (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (has_sub.sub.{0} pnat pnat.has_sub (has_mul.mul.{0} pnat pnat.has_mul (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))) u) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) (hv : has_dvd.dvd.{0} pnat (monoid_has_dvd.{0} pnat (right_cancel_monoid.to_monoid.{0} pnat (cancel_monoid.to_right_cancel_monoid.{0} pnat (cancel_comm_monoid.to_cancel_monoid.{0} pnat (ordered_cancel_comm_monoid.to_cancel_comm_monoid.{0} pnat pnat.ordered_cancel_comm_monoid))))) (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (has_sub.sub.{0} pnat pnat.has_sub (has_mul.mul.{0} pnat pnat.has_mul (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))) v) (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) (hsum : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) u (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one))))))) (h : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) v (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (bit0.{0} pnat pnat.has_add (bit0.{0} pnat pnat.has_add (bit1.{0} pnat pnat.has_one pnat.has_add (has_one.one.{0} pnat pnat.has_one)))))))) (h₄ : has_lt.lt.{0} pnat (preorder.to_has_lt.{0} pnat (partial_order.to_preorder.{0} pnat (ordered_cancel_comm_monoid.to_partial_order.{0} pnat pnat.ordered_cancel_comm_monoid))) (bit0.{0} pnat pnat.has_add (bit1.{0}

[Stanislas Polu]

Now trying to test for this with something like docs#expr.contains_expr_or_mvar or occurs

[Stanislas Polu]

Unfortunately this does not seem to catch it?

guard (bnot (pf.has_local_in $ mk_name_set.insert `undefined)),

[Stanislas Polu]

And guard (bnot (pf.occurs undefined)), does not cut it as undefined gets eval-ed and crashes

[Stanislas Polu]

Using this:

meta def guard_undefined : expr → tactic unit := λ e, do {
  contains_undefined ← e.mfold ff (λ e' _ acc, do { tactic.trace format! "{e'}", if acc then pure acc else pure $ bor acc $ do { e'.has_local_in $ mk_name_set.insert "undefined" }}),
  guard $ bnot contains_undefined
}

I do run over an exp which is undefined.{0} but the has_local_in call does not detect that. Any idea how I can properly detect this?

[Stanislas Polu]

Ah! This seems to cut it:

meta def guard_undefined : expr → tactic unit := λ e, do {
  contains_undefined ← e.mfold ff (λ e' _ acc, if acc then pure acc else pure $ bor acc $ e'.app_symbol_in [`undefined]),
  guard $ bnot contains_undefined
}

Not sure if it is universally correct though?

[Jason Rute]

@Jesse Michael Han suggested that we could list all the axioms used. That should be a general solution for this sort of thing. (I assume a constant is considered an axiom, right?) However, I don’t know if there is currently a tactic which will tell you what axioms are used in an expression. Does anyone know if there is and if not what obstacles exist in making one?

[Stanislas Polu]

This is the only example of undefined I think in mathlib, probably where the model learned about it: https://github.com/leanprover-community/mathlib/blob/76a3b82dc0ae6c9a60a8714d74c6cf2b854cf17b/src/data/fp/basic.lean#L113 cc @Mario Carneiro

[Mario Carneiro]

undefined is a meta constant, so it shouldn't be valid in a normal proof

[Mario Carneiro]

rather than looking for undefined specifically, you should screen out any references to meta things

[Stanislas Polu]

How would one achieve that?

[Mario Carneiro]

The easy way is to try to send the definition to the kernel and see if it complains

[Mario Carneiro]

like this example shouldn't actually pass lean

[Mario Carneiro]

the metaprogramming way is to use environment.get_decl to get the declaration and see if trusted is set (false means meta)