tauto! fails on ne

Stream: general

[Bhavik Mehta]

I'm not sure if this counts as a bug, but it surprised me so I'll mention it anyway:

import tactic.tauto

example {x y : ℕ} (h : ¬x ≠ y) : x = y :=
begin
  tauto!,
end

fails

[Anne Baanen]

Is this tauto not knowing that ≠ is defined as ¬ = or tauto not doing double negation elimination?

[Jason Rute]

Double negation works, so it is maybe the former.

import tactic.tauto

example {x y : ℕ} (h : ¬¬x = y) : x = y :=
begin
  tauto!,
end

[Jason Rute]

But it can do this too, so it does know about ≠.

import tactic.tauto

example {x y : ℕ} : ¬ x ≠ y ↔ ¬¬x = y :=
begin
  tauto!,
end

[Damiano Testa]

The last example is also true by refl, so this is why tauto might "know" about it?

[Damiano Testa]

I have not looked at the implementation, but this

meta def tautology (cfg : tauto_cfg := {}) : tactic unit := focus1 $
  let basic_tauto_tacs : list (tactic unit) :=
        [reflexivity, solve_by_elim,
          constructor_matching none [``(_ ∧ _),``(_ ↔ _),``(Exists _),``(true)]],
...

suggests that tauto will try reflexivity.

[Damiano Testa]

completely untested, but

         | `(_ ≠ _)   := replace h.local_pp_name ``(mt iff.to_eq %%h)   --  <-- look here
         | `(_ = _)   := replace h.local_pp_name ``(eq.to_iff %%h)
         | `(¬ (_ ∧ _))  := replace h.local_pp_name ``(decidable.not_and_distrib'.mp %%h) <|>
                            replace h.local_pp_name ``(decidable.not_and_distrib.mp %%h)
         | `(¬ (_ ∨ _))  := replace h.local_pp_name ``(not_or_distrib.mp %%h)
         | `(¬ ¬ _)      := replace h.local_pp_name ``(decidable.of_not_not %%h)  -- <-- and here

suggests that maybe adding a further case

         | `(¬ _ ≠ _)      := replace h.local_pp_name ``(decidable.of_not_not %%h)

may fix the issue?

[Damiano Testa]

maybe it is a fluke, but that actually does the job!

[Damiano Testa]

who knows if it breaks something else: I'll PR this.

[Damiano Testa]

#16232

[FR]

Maybe it can also support ¬ _ ∉ _ etc.

[Damiano Testa]

@FR if this is what you had in mind:

example {α} {x : α} {s : set α} (h : ¬x ∉ s) : x ∈ s :=
begin
  tauto!,
end

then it works. I am on the branch with the PR, so I do not know if it is a consequence of the change or whether it would have worked before as well.

[Eric Rodriguez]

∉ is just notation for ¬ \mem iirc

[Damiano Testa]

Ah, while ne is notation for -> false?

[Eric Rodriguez]

ne is not notation sadly it's a whole def

[Eric Rodriguez]

docs#ne

[Eric Rodriguez]

try clicking on the ∉ in docs#set.not_mem_Ioo instead for example

[Eric Rodriguez]

i'm not sure where it's declared though

[Eric Rodriguez]

https://github.com/leanprover-community/lean/blob/741670c439f1ca266bc7fe61ef7212cc9afd9dd8/library/init/core.lean#L339

[Damiano Testa]

I see, thanks for the information!

[Eric Rodriguez]

does anyone know why it was done this way fwiw? I will say that having ne as a definition has never caused anything but trouble

[Mario Carneiro]

It means that (h : a != b).symm calls ne.symm instead of not.symm

[Mario Carneiro]

I don't think that's the reason per se, this decision predates me and mathlib

[Mario Carneiro]

There is some default desire to use reducible definitions over notations when possible, as evidenced by the fact that ge still exists

[Yaël Dillies]

I wish we could redirect dot notation by hand sometimes. The other example I'm thinking of is resolving dot notation on f : α → β to pi, imp and function.

[Mario Carneiro]

which one?

[Mario Carneiro]

we can certainly tweak the rules there but it's annoying to switch preferences

[Yaël Dillies]

All three would be best.

[Yaël Dillies]

The only name clashes I can think that could happen between pi, imp and function are instance names, and that's irrelevant to dot notation.

[Eric Rodriguez]

I thought pi and function worked in lean4

[Eric Rodriguez]

and ge barely exists, if anything exists it's gt and pretty much solely for eps > 0

[Damiano Testa]

The PR just got merged, so the example above should work now!

[Kyle Miller]

Yaël Dillies said:

I wish we could redirect dot notation by hand sometimes. The other example I'm thinking of is resolving dot notation on f : α → β to pi, imp and function.

lean#757 is now in, which backports some Lean 4 dot notation features (rss link). Once mathlib is using it, when you do f.foo it'll resolve to function.f foo. I had a version that would use the pi and forall namespaces too depending on whether the function was dependent or was for a Prop, but seeing as Lean 4 doesn't do this (yet?) I went for Lean 4 compatibility.

You might like that extended dot notation will now respect extends without needing to use any tricks that relied on coercions. It can also (to a limited extent) use aliases, i.e. names introduced using export.

[Kyle Miller]

There's a bug that mathlib has been relying on, it turns out. When you do x.foo in a non-function-application position and x : S a b c, then it would always do S.foo x with x in the first argument without checking whether S.foo was even a function. You can see this used when S.foo is an equiv (for example a.of_dual here). This "feature" doesn't work when you supply additional arguments, like x.foo 37, since applied dot notation uses a different resolution procedure.

In the meantime, we have tweaked the resolution procedure to resolve x.foo 37 to be S.foo x 37 when there is no argument of type S a b c (i.e., it inserts x first). This will be until either we fix mathlib (and remove this feature) or until Lean 4 potentially changes.

[Kyle Miller]

It might be nice to have dot notation respect has_coe_to_fun instances as it resolves where to put an argument. It also might be nice keeping this insert-as-first-argument feature for adding "extension methods" to a type via aliases, where the first argument is a term that satisfies some typeclass constraint.

[Eric Rodriguez]

so this is why some polynomial definitions (e.g. docs#polynomial.derivative) work with dot notation, whilst some others don't (docs#polynomial.map_ring_hom). I do think it'd be really good if things with a coe_to_fun could work reliably with dot notation, but maybe that's a lot to ask for. They definitely wont be prettyprinted that way, as things stand.