output of push_neg

Stream: general

[Heather Macbeth]

Would it be possible to write a function which, given an expression H, outputs the result of running push_neg on H? So

#check push_neg_fun (¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n))
-- displays ∃ (n : ℕ), ∀ (p q : ℝ), p < ↑n → q ≤ ↑n

[Scott Morrison]

See https://leanprover-community.github.io/mathlib_docs/tactic/reassoc_axiom.html#category_theory.reassoc_of.

[Heather Macbeth]

@Scott Morrison interesting, can you please remind me what the . in

theorem category_theory.reassoc_of {α} (hh : α) {β}
  (x : tactic.calculated_Prop β hh . tactic.derive_reassoc_proof) : β := x

does?

[Scott Morrison]

The . is an "auto_param", which says "if this argument is omitted, please run this tactic to synthesize a value"

[Scott Morrison]

I trying/failing to adapt this to your request at the moment. :-)

[Heather Macbeth]

I should say, the motivation is to allow my students to check their work for section 2.10 here:
https://www.people.vcu.edu/~rhammack/BookOfProof/Main.pdf#page=72

[Alex J. Best]

If you just want something usable, then this doesn't need to be a literal function, and could be a tactic, this would hopefully let you reuse more of the internals of push_neg

[Heather Macbeth]

It's true that I can already do something like

example (H : ¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n)) : true :=
begin
  push_neg at H,
  -- now look at H
end

but it's rather unwieldy. Is that what you mean?

[Alex J. Best]

Well it would essentially be doing that under the hood, but it could be wrapped up in a nice user command like https://leanprover-community.github.io/mathlib_docs/commands.html##simp

[Heather Macbeth]

Oh, I've never seen #simp before! Indeed that (a push_neg version of that) seems exactly what I want.

[Scott Morrison]

The reassoc_of solution translates to:

import tactic.push_neg
import data.real.basic

open push_neg

namespace tactic

def calculated_Prop {α} (β : Prop) (hh : α) := β

meta def derive_push_neg_proof : tactic unit :=
do `(calculated_Prop %%v %%h) ← target,
   ty ← infer_type h,
   (t,pr) ← normalize_negations ty,
   unify v t,
   pr ← to_expr ``(eq.mp %%pr %%h),
   exact pr

end tactic

theorem push_neg_of {α} (hh : α) {β}
  (x : tactic.calculated_Prop β hh . tactic.derive_push_neg_proof) : β := x

variables (h : ¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n))
#check push_neg_of h

[Alex J. Best]

Yeah I don't think it would be too hard to make, changing the function at src#tactic.simp_cmd to call src#push_neg.normalize_negations instead of where it calls e.simp might already give something passable. Unfortunately its a bit late for me now to try it :smile:

[Scott Morrison]

Probably the separate variables line can be avoided.

[Scott Morrison]

It may be too messy for your students: it prints out the x argument, which is the proof that the before and after props are equivalent...

[Scott Morrison]

They don't want to see that.

[Heather Macbeth]

Indeed -- as opposed to just the "after prop", which I guess is what I was originally asking about ...

[Heather Macbeth]

The normalize_negations comes from the internals of push_neg, is that right?

[Alex J. Best]

Oh lol Scott I just understood thats a really sneaky way of calling tactics from #check!

[Scott Morrison]

The #simp solution is much better:

import tactic
import data.real.basic

setup_tactic_parser

open push_neg
namespace tactic

@[user_command] meta def push_neg_cmd (_ : parse $ tk "#push_neg") : lean.parser unit :=
do
  e ← types.texpr,

  (ts, mappings) ← synthesize_tactic_state_with_variables_as_hyps [e],

  result ← lean.parser.of_tactic $ λ _, do
  { e ← to_expr e,
    prod.fst <$> normalize_negations e } ts,
  trace result

end tactic

#push_neg (¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n)) -- prints `∃ (n : ℕ), ∀ (p q : ℝ), p < ↑n → q ≤ ↑n`

[Scott Morrison]

Maybe we should factor out the generic code from #simp.

[Heather Macbeth]

This is so cool. Thank you so much @Scott Morrison and @Alex J. Best!

[Heather Macbeth]

I can put it in some bespoke mathlib version for my students if needed, but do you think it's worthy of joining mathlib proper?

[Rob Lewis]

A hackish version of the reassoc approach, but agreed that the custom command is the proper solution:

import tactic data.real.basic

def pn_calculated_Prop {α} (hh : α) : Type := Prop

open tactic

meta def derive_pn_proof : tactic unit :=
do `(pn_calculated_Prop %%h) ← target,
   prod.fst <$> push_neg.normalize_negations h >>= exact

theorem pn_of {α} (hh : α)
  (x : pn_calculated_Prop hh . derive_pn_proof) : Prop := x

notation `normalized:` b := pn_of _ b

#check pn_of (¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n))

[Rob Lewis]

This generalizes to any tactic that works on the goal (norm_cast, ring_nf, ...). There could be one generic command. Coming up with the right syntax is the hard part.

[Rob Lewis]

(This being the #simp approach that is)

[Johan Commelin]

I vote for #run some_tactic on (my wonderful expression)

[Johan Commelin]

#run ring_nf on (x + y) * (a + b + 3) - x * a
#run simp on f (x + y)
#run push_neg on ¬ (∀ n : ℕ, ∃ p q : ℝ, p < n ∧ q > n)

[Patrick Massot]

Heather, you can also have a look at how this is done in the beginning of https://github.com/leanprover-community/tutorials/blob/master/src/exercises/08_limits_negation.lean

[Yaël Dillies]

Maybe #run_tactic to avoid confusion with run_cmd?

[Johan Commelin]

But that's sooo longgg :rofl:

[Yaël Dillies]

Whatabout #run_tac?

[Johan Commelin]

Certainly better :smiley:

[Heather Macbeth]

To bump this old thread: I wrote a user command for push_neg, see #16775 and post, and then remembered I'd already asked for it a year ago. I am posting here in case anyone discovers the previous discussion. My PR is pretty close to what Scott came up with, but it would still be nice to generalize according to Johan's idea of a #run user command.

[Mario Carneiro]

By the way, I think in mathlib4 I want to have something like #conv (tac) e rather than doing this kind of thing for every conv tactic

[Heather Macbeth]

Yes, this was Scott/Rob/Johan's idea in the old thread.

[Mario Carneiro]

with the distinction that what we actually care about here are conv tactics, not regular tactics