## Stream: general

### Topic: tauto! fails on ne

#### Bhavik Mehta (Aug 23 2022 at 23:14):

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 (Aug 24 2022 at 08:57):

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

#### Jason Rute (Aug 24 2022 at 12:04):

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 (Aug 24 2022 at 12:06):

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 (Aug 24 2022 at 12:09):

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

#### Damiano Testa (Aug 24 2022 at 12:11):

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 (Aug 24 2022 at 12:15):

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 (Aug 24 2022 at 12:17):

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

#### Damiano Testa (Aug 24 2022 at 12:17):

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

#16232

#### FR (Aug 24 2022 at 12:22):

Maybe it can also support ¬ _ ∉ _ etc.

#### Damiano Testa (Aug 24 2022 at 12:24):

@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 (Aug 24 2022 at 12:27):

∉ is just notation for ¬ \mem iirc

#### Damiano Testa (Aug 24 2022 at 12:27):

Ah, while ne is notation for -> false?

#### Eric Rodriguez (Aug 24 2022 at 12:28):

ne is not notation sadly it's a whole def

docs#ne

#### Eric Rodriguez (Aug 24 2022 at 12:29):

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

#### Eric Rodriguez (Aug 24 2022 at 12:29):

i'm not sure where it's declared though

#### Eric Rodriguez (Aug 24 2022 at 12:30):

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

#### Damiano Testa (Aug 24 2022 at 12:33):

I see, thanks for the information!

#### Eric Rodriguez (Aug 24 2022 at 19:40):

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 (Aug 24 2022 at 19:46):

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

#### Mario Carneiro (Aug 24 2022 at 19:47):

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

#### Mario Carneiro (Aug 24 2022 at 19:48):

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 (Aug 24 2022 at 19:49):

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.

which one?

#### Mario Carneiro (Aug 24 2022 at 19:49):

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

#### Yaël Dillies (Aug 24 2022 at 19:54):

All three would be best.

#### Yaël Dillies (Aug 24 2022 at 19:56):

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 (Aug 24 2022 at 19:58):

I thought pi and function worked in lean4

#### Eric Rodriguez (Aug 24 2022 at 20:01):

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

#### Damiano Testa (Aug 25 2022 at 08:12):

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

#### Kyle Miller (Aug 25 2022 at 17:14):

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 (Aug 25 2022 at 17:18):

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 (Aug 25 2022 at 17:20):

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 (Aug 25 2022 at 18:23):

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.

Last updated: Dec 20 2023 at 11:08 UTC