Understanding tauto.lean (mathlib3)

Stream: mathlib4

[Thomas Murrills]

I'm trying to understand tauto.lean in mathlib3 (just as a way to learn how tactic-writing works), and I thought it might be worth asking a couple questions as to what's going on. I think understand what "should" be going on for the most part mathematically, but the meaning and usage of some lean operations is throwing me. Figured I'd gather them all here instead of creating a bunch of topics! (Unless that's frowned upon for some reason, in which case I'll make a bunch of topics. :smile: )

[Thomas Murrills]

First, what is local_pp_name is meant to do (or where is documentation for this)? The source code doesn't seem to be commented, and I can't find it in the reference manual.

[Thomas Murrills]

Equivalently, what would the analogue in Lean 4 be? Or would a totally different approach be used? Here, local_pp_name is used like this:

...
do h ← get_local h.local_pp_name,
         e ← infer_type h,
         match e with
         | `(¬ _ = _)   := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | `(_ ≠ _)     := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | ...

[Mario Carneiro]

local_pp_name returns the pretty-printing name (the thing users see) for a local constant (now known as an fvar)

[Thomas Murrills]

My current guess is h.local_pp_name is equivalent to h.userName where h might be provided by something like for h in ← getLCtx. But it seems a bit unsafe to me to use replace with what I understand to be a user-facing name to replace hypotheses after doing syntax matching. (Though I'm not sure if that is indeed what's happening here.)

Is there a better pattern for modifying a hypothesis in lean 4, in general?

[Mario Carneiro]

what does replace do in this code?

[Mario Carneiro]

it looks like a local function

[Thomas Murrills]

here's how the function starts—it's the first in the file

/--
  find all assumptions of the shape `¬ (p ∧ q)` or `¬ (p ∨ q)` and
  replace them using de Morgan's law.
-/
meta def distrib_not : tactic unit :=
do hs ← local_context,
   hs.for_each $ λ h,
    all_goals' $
    iterate_at_most' 3 $
      do h ← get_local h.local_pp_name,
         e ← infer_type h,
         match e with
         | `(¬ _ = _)   := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | `(_ ≠ _)     := replace h.local_pp_name ``(mt iff.to_eq %%h)
         | ...

[Thomas Murrills]

-

[Mario Carneiro]

I mean, where is the replace function defined?

[Mario Carneiro]

it might not mean what you think

[Thomas Murrills]

VS Code says it's tactic.replace

[Mario Carneiro]

which is?

[Thomas Murrills]

"replace h p elaborates the pexpr p, clears the existing hypothesis named h from the local context, and adds a new hypothesis named h. The type of this hypothesis is the type of p. Fails if there is nothing named h in the local context."

[Thomas Murrills]

which seems to me like it's finding the local hypothesis by the pretty-printed name

[Thomas Murrills]

which sounds unsafe

[Mario Carneiro]

It's true, that is imprecise

[Mario Carneiro]

most likely it's written like that to fit the signature of tactic.replace which is defined in core or something

[Thomas Murrills]

hmmm

[Mario Carneiro]

that kind of thing is reasonable for user-facing tactics since the name is coming from something the user wrote anyway

[Mario Carneiro]

I should mention that I'm not really happy with the original lean 3 implementation of tauto, so I'm okay with it getting a rewrite on the way to lean 4 as long as it does basically similar things

[Mario Carneiro]

although I realize that's a bit much to ask of someone who doesn't have a lot of experience writing lean tactics

[Thomas Murrills]

I see, cool! In general, is there better functionality in Lean 4 for modifying a hypothesis (seeing as we're just iterating over all of them)?

[Mario Carneiro]

You shouldn't "modify" hypotheses for the most part

[Mario Carneiro]

instead, you revert them and intro the modified versions

[Mario Carneiro]

it is important for lean's internal coherence that an fvar only ever has a single type in a single local context

[Thomas Murrills]

although I realize that's a bit much to ask of someone who doesn't have a lot of experience writing lean tactics

I mean, I'm willing to try! I just wouldn't want to prevent other people with more experience from potentially making better choices, lol

[Mario Carneiro]

Well there's always review time :P

[Mario Carneiro]

but it's great to hear you want to try it, I'll help however I can

[Thomas Murrills]

ok, that sounds great! :)

[Thomas Murrills]

instead, you revert them and intro the modified versions

hmmm... so would we start with something like for h in <- getLCtx at all, as I initially thought, then? reverting then introing seems to suggest we do a bunch of reversions then inspect the type of the goal, then do a bunch of intros based on that

[Thomas Murrills]

however, in this case it seems we might only want to revert a hypothesis based on its type in the first place. so maybe the for still works (thinking out loud)

[Mario Carneiro]

The usual pattern is that you say "revert h" and it reverts h and also h' which depended on h, and it gives you an array which you later pass to introN to re-intro them after rewriting

[Thomas Murrills]

ah, ok

[Thomas Murrills]

Ok, general question: I'm not totally sure what tauto! is meant to do in opposition to tauto; according to the documentation "The variants tautology! and tauto! use the law of excluded middle", but tauto seems to use LEM anyway, as example (p : Prop) : p ∨ ¬ p := by tauto works. Is there something I'm missing? (I see that tauto! runs classical first, but I can't quite tell what meaningful effect that has.)

[Mario Carneiro]

It's kind of broken, don't worry about it. I wrote itauto exactly because tauto wasn't living up to its LEM-free claim. I think you should just implement one version of tauto and use classical logic.

[Kevin Buzzard]

Yes, mathlib is designed to be a classical library and the main issue at stake here is porting it to lean 4 so classical assumptions are fine.

[Mario Carneiro]

it is easy enough to translate both tauto and tauto! to tauto in mathport, so we can remove the option entirely

[Thomas Murrills]

Ok, sounds good! I'm thinking about how we might improve the functionality tauto in general now...

[Thomas Murrills]

For example, it seems like currently it applies solve_by_elim at the end to address ∃ expressions, but doesn't address tautologies within those. e.g. example (p q : Prop) (hq : q) : ∃ (hq : q), p → p := by tauto fails. It seems easy enough to make it recursive—would it be alright to make it succeed here?

[Mario Carneiro]

yes

[Mario Carneiro]

as long as you can do the test cases, it's okay to do more

[Thomas Murrills]

great! where are the test cases located, by the way?

[Mario Carneiro]

test/tauto.lean in mathlib

[Thomas Murrills]

oop. of course

[Thomas Murrills]

(I was looking in testing by mistake)

[Thomas Murrills]

also, thinking of improving the functionality: it seems strange to me that tauto is exclusively a finishing tactic when it produces a bunch of goals. wouldn't it be useful for a user to be able to carry on from that point, and supply the remaining goals after tauto does some work? (or is that named/would that be named something else?)

[Mario Carneiro]

can you describe the goals that are generated in a clear way, such that the user can predict them?

[Thomas Murrills]

hmmm

[Mario Carneiro]

If you just do a bunch of mumbo jumbo and end up somewhere and hand control back to the user, that's not very robust to tactic changes

[Thomas Murrills]

I see, makes sense

[Mario Carneiro]

The standard is a lot higher on non-"finishing tactics" to produce subgoals deterministically

[Mario Carneiro]

so most of the really high powered and heuristic based tactics are either finishing tactics by construction or convention

[Thomas Murrills]

that's a good convention! (but hmmm...and, it's not necessary for reimplementing tauto, but...I wonder if there exists a sort of canonical "tautological normalization" one can perform which reduces a proposition "as much as possible" in a certain mathematically-unique way. I kind of doubt that there does, but it'd be neat! After all, some of the goals that tauto produces anyway are pretty intelligible...but that's a generalization for later :) )

[Alex J. Best]

One thing that might be useful is rather than setting new subgoals (which may indeed be a bit random), to print some sufficient facts (when tauto fails but does reduce the problem a bit) that the user can have := into context above, so that tauto will then finish.

[Thomas Murrills]

Okay, finally feeling well enough to start working on tauto again! I'm still working through the existing file to see what it does.

[Thomas Murrills]

First question: consider the definition of add_symm_proof.

/--
  If there exists a symmetry lemma that can be applied to the hypothesis `e`,
  store it.
-/
meta def add_symm_proof (r : tauto_state) (e : expr) : tactic (expr × expr) :=
do env ← get_env,
   let rel := e.get_app_fn.const_name,
   some symm ← pure $ environment.symm_for env rel
     | add_refl r e,
   (do e' ← mk_meta_var `(Prop),
       iff_t ← to_expr ``(%%e = %%e'),
       (_,p) ← solve_aux iff_t
         (applyc `iff.to_eq ; () <$ split ; applyc symm),
       e' ← instantiate_mvars e',
       m ← read_ref r,
       write_ref r $ (m.insert e (e',p)).insert e' none,
       return (e',p) )
   <|> add_refl r e

[Thomas Murrills]

What exactly does () <$ split do, for one? I understand what <$ does in isolation, and have an idea what split does, but I'm not sure how they're used together in context with () (the inhabitant of unit, as in tactic unit, somehow, maybe?).

[Mario Carneiro]

() <$ tac is an idiom similar to discard tac or _ <- tac, it runs tac and then returns () instead of whatever the tactic was going to return

[Thomas Murrills]

ah, ok, thanks!