Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Check for sorry in tactic proof


Jason Rute (Jun 02 2021 at 13:26):

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 (Jun 02 2021 at 13:27):

cc @Stanislas Polu @Jesse Michael Han

Scott Morrison (Jun 02 2021 at 13:27):

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

Scott Morrison (Jun 02 2021 at 13:28):

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 (Jun 02 2021 at 13:29):

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

Stanislas Polu (Jun 07 2021 at 09:04):

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 (Jun 07 2021 at 09:24):

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

Stanislas Polu (Jun 07 2021 at 09:28):

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

Stanislas Polu (Jun 07 2021 at 09:30):

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 (Jun 07 2021 at 09:35):

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 (Jun 07 2021 at 09:40):

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

Stanislas Polu (Jun 07 2021 at 10:27):

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

Damiano Testa (Jun 07 2021 at 10:32):

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 (Jun 07 2021 at 10:46):

   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 (Jun 07 2021 at 11:49):

Thanks a lot @Jannis Limperg

Stanislas Polu (Jun 07 2021 at 13:40):

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 (Jun 07 2021 at 14:12):

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 (Jun 07 2021 at 14:26):

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

Jason Rute (Jun 07 2021 at 15:19):

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 (Jun 07 2021 at 15:23):

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

Stanislas Polu (Jun 07 2021 at 15:23):

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

Stanislas Polu (Jun 07 2021 at 15:31):

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 (Jun 08 2021 at 07:46):

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 (Jun 08 2021 at 07:51):

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

Patrick Massot (Jun 08 2021 at 07:52):

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

Stanislas Polu (Jun 08 2021 at 07:54):

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 (Jun 08 2021 at 08:30):

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 (Jun 08 2021 at 08:34):

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

Stanislas Polu (Jun 08 2021 at 08:49):

Unfortunately this does not seem to catch it?

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

Stanislas Polu (Jun 08 2021 at 08:50):

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

Stanislas Polu (Jun 08 2021 at 09:08):

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 (Jun 08 2021 at 09:30):

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 (Jun 08 2021 at 12:49):

@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 (Jun 08 2021 at 13:05):

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 (Jun 08 2021 at 19:45):

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

Mario Carneiro (Jun 08 2021 at 19:46):

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

Stanislas Polu (Jun 08 2021 at 20:29):

How would one achieve that?

Mario Carneiro (Jun 08 2021 at 20:57):

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

Mario Carneiro (Jun 08 2021 at 20:57):

like this example shouldn't actually pass lean

Mario Carneiro (Jun 08 2021 at 20:58):

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


Last updated: Dec 20 2023 at 11:08 UTC