# Zulip Chat Archive

## Stream: general

### Topic: tidy bug

#### Patrick Massot (Oct 02 2018 at 20:01):

Can someone try

import tactic.tidy example (X Y : Type) (f : X → Y) (h : ∀ y : Y, ∃ x : X, f(x) = y) : (∃ g : Y → X, f ∘ g = id) := begin cases classical.axiom_of_choice h with g H, tidy, end

#### Patrick Massot (Oct 02 2018 at 20:02):

Here it says `no goals`

after `tidy`

but red-squiggle `example`

with `type mismatch at application g a term a has type Y_1 but is expected to have type Y types contain aliased name(s): Y remark: the tactic `dedup` can be used to rename aliases`

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:05):

Here it says

`no goals`

after`tidy`

but red-squiggle`example`

with`type mismatch at application g a term a has type Y_1 but is expected to have type Y types contain aliased name(s): Y remark: the tactic `dedup` can be used to rename aliases`

I get the same.

#### Patrick Massot (Oct 02 2018 at 20:07):

Let's wait for @Scott Morrison to wake up, or finish lunch, or whatever it's time to do in Australia

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:08):

Here's the trace:

/- `tidy` says -/ dsimp at *, fsplit, work_on_goal 0 { intros a }, work_on_goal 1 { ext1, dsimp at *, solve_by_elim }

#### Patrick Massot (Oct 02 2018 at 20:08):

I'm working on that demo file we discussed earlier, trying to see what general purpose automation can do what. The problem with magic is it's somewhat unpredictable. It seems `finish`

is pretty powerful in those example, but I'd like to understand when `tidy`

or `tauto`

actually also work (or even work better)

#### Patrick Massot (Oct 02 2018 at 20:10):

Good idea Bryan!

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:10):

Not sure if I misunderstand the meaning of the trace, but throwing it in as a proof fails at the first `dsimp`

#### Patrick Massot (Oct 02 2018 at 20:10):

It's very strange to follow, it seems hopeless and then `solve_by_elim`

pretends to get rid of all meta-vars and do the job

#### Patrick Massot (Oct 02 2018 at 20:11):

here I get exactly the same result as with tidy itself

#### Patrick Massot (Oct 02 2018 at 20:11):

google says Scott may be sleeping

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:12):

I see this:

import tactic.tidy example (X Y : Type) (f : X → Y) (h : ∀ y : Y, ∃ x : X, f(x) = y) : (∃ g : Y → X, f ∘ g = id) := begin dsimp at *, -- squiggly line under dsimp /- Tactic State X Y : Type, f : X → Y, h : ∀ (y : Y), ∃ (x : X), f x = y ⊢ ∃ (g : Y → X), f ∘ g = id scratch.lean:14:0: error dsimplify tactic failed to simplify state: ⊢ ∀ (X Y : Type) (f : X → Y), (∀ (y : Y), ∃ (x : X), f x = y) → (∃ (g : Y → X), f ∘ g = id) -/ fsplit, work_on_goal 0 { intros a }, work_on_goal 1 { ext1, dsimp at *, solve_by_elim } end

#### Patrick Massot (Oct 02 2018 at 20:13):

you erased too much

#### Patrick Massot (Oct 02 2018 at 20:13):

the choice idea is required

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:13):

Oops!

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:26):

Yes, now I see the same.

Nothing seems strange with the intermediate tactic states. Is there a way to use the `discharger`

option for `solve_by_elim`

to make it spit out what it's doing at each stage?

#### Patrick Massot (Oct 02 2018 at 20:29):

How is it possible that none of our general purpose weapon can kill

example (X Y : Type) (f : X → Y) (g : Y → X) (h : f ∘ g = id ) (y : Y) : f (g y) = y

#### Kenny Lau (Oct 02 2018 at 20:30):

I don't use weapons :P

example (X Y : Type) (f : X → Y) (g : Y → X) (h : f ∘ g = id ) (y : Y) : f (g y) = y := congr_fun h y

#### Patrick Massot (Oct 02 2018 at 20:31):

Kenny, this is exactly what I did at https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/demo.lean#L60 but I'm trying to rewrite this file using automation, for comparison

#### Patrick Massot (Oct 02 2018 at 20:32):

I guess this is again because tactic writers don't like function equalities, especially with compositions

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:32):

Replacing `solve_by_elim`

with `apply_assumption`

gives the same strange behavior.

#### Rob Lewis (Oct 02 2018 at 20:32):

Higher order reasoning is hard!

#### Patrick Massot (Oct 02 2018 at 20:33):

`finish`

and its friends could try to turn each function equality assumption into a forall

#### Patrick Massot (Oct 02 2018 at 20:34):

example (X Y : Type) (f : X → Y) (g : Y → X) (h : ∀ z, (f ∘ g) z = id z) (y : Y): f (g y) = y := by finish

does work

#### Patrick Massot (Oct 02 2018 at 20:35):

Of course rewriting `h`

like this is the most un-mathematical thing you could see

#### Kenny Lau (Oct 02 2018 at 20:35):

`finish`

and its friends

#### Patrick Massot (Oct 02 2018 at 20:39):

its friends are `tauto`

and `tidy`

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:43):

Could it be that there's something strange happening with `work_on_goal`

? The following works:

import tactic.tidy example (X Y : Type) (f : X → Y) (h : ∀ y : Y, ∃ x : X, f(x) = y) : (∃ g : Y → X, f ∘ g = id) := begin cases classical.axiom_of_choice h with g H, dsimp at *, fsplit, { exact g }, { ext1, dsimp at *, apply_assumption } end

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:44):

Compare this, which gives the same `no goals`

+ weird error as the initial `tidy`

call:

import tactic.tidy example (X Y : Type) (f : X → Y) (h : ∀ y : Y, ∃ x : X, f(x) = y) : (∃ g : Y → X, f ∘ g = id) := begin cases classical.axiom_of_choice h with g H, dsimp at *, fsplit, --{ exact g }, work_on_goal 1 { ext1, dsimp at *, apply_assumption } end

#### Patrick Massot (Oct 02 2018 at 20:46):

interesting

#### Patrick Massot (Oct 02 2018 at 20:48):

Even better:

example (X Y : Type) (f : X → Y) (h : ∀ y : Y, ∃ x : X, f(x) = y) : (∃ g : Y → X, f ∘ g = id) := begin cases classical.axiom_of_choice h with g H, dsimp at *, fsplit, { exact g }, work_on_goal 0 { ext1, dsimp at *, apply_assumption } end

works!

#### Patrick Massot (Oct 02 2018 at 20:50):

but actually this is getting far away from what tidy suggested

#### Bryan Gin-ge Chen (Oct 02 2018 at 20:53):

Here's `work_on_goal`

. If I had to guess, there's something wrong in here, possibly in handling what happens if a goal gets solved.

#### Bryan Gin-ge Chen (Oct 02 2018 at 21:29):

I think the problem is that when `apply_assumption`

kills off a goal, it does not return properly to `work_on_goal`

. Then lean thinks it has finished, but in reality there are more goals that `work_on_goal`

just temporarily deleted. There are no issues when `exact g`

finishes a goal inside `work_on_goal`

, so there's something going on with this particular interaction.

#### Bryan Gin-ge Chen (Oct 02 2018 at 21:31):

`apply_assumption`

is here, but it's too monad-y for me to make sense of at the moment.

#### Simon Hudon (Oct 02 2018 at 21:42):

What problem are you looking for?

#### Bryan Gin-ge Chen (Oct 02 2018 at 22:07):

Patrick started this thread with an example where `tidy`

leaves the tactic state with `no goals`

but there is a strange error.

I'm proposing that the root cause of this is due to `apply_assumption`

not returning properly to `work_on_goal`

.

#### Scott Morrison (Oct 02 2018 at 22:08):

Thanks for these bug reports. I probably won't have a chance to work on it until the weekend.

#### Kenny Lau (Oct 02 2018 at 22:36):

import tactic.interactive example (X Y : Type) (f : X → Y) (g : Y → X) (h : ∀ z, (f ∘ g) z = id z) (y : Y): f (g y) = y := by tauto

#### Kenny Lau (Oct 02 2018 at 22:36):

@Patrick Massot

#### Patrick Massot (Oct 03 2018 at 07:14):

Thanks Kenny, but this is the version I don't want, because `h`

is stated un-mathematically

#### Yaël Dillies (Aug 15 2022 at 08:22):

Looks like `tidy`

used the same variable name twice:

```
import logic.relation
variables {α β γ δ ε κ : Type*}
example (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → κ) :
relation.map (relation.map r f₁ g₁) f₂ g₂ = relation.map r (f₂ ∘ f₁) (g₂ ∘ g₁) :=
by tidy
/-
type mismatch at application
r ᾰ_h_h_left_w
term
ᾰ_h_h_left_w
has type
α_1
but is expected to have type
α
types contain aliased name(s): α
remark: the tactic `dedup` can be used to rename aliases
-/
```

#### Bhavik Mehta (Aug 16 2022 at 15:21):

Is this a bug in `tidy`

or in one of the things `tidy`

uses? If I remember correctly, `tidy`

doesn't have the ability to choose variable names whatsoever, just to call other tactics

#### Kevin Buzzard (Aug 16 2022 at 21:28):

```
example (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → κ) :
relation.map (relation.map r f₁ g₁) f₂ g₂ = relation.map r (f₂ ∘ f₁) (g₂ ∘ g₁) :=
begin
ext1,
ext1,
simp at *,
fsplit,
work_on_goal 1
{ intros ᾰ,
cases ᾰ,
cases ᾰ_h, cases ᾰ_h_h, cases ᾰ_h_h_right, cases ᾰ_h_h_left, cases ᾰ_h_h_left_h,
induction ᾰ_h_h_right_right, induction ᾰ_h_h_right_left, cases ᾰ_h_h_left_h_h,
cases ᾰ_h_h_left_h_h_right, induction ᾰ_h_h_left_h_h_right_right,
induction ᾰ_h_h_left_h_h_right_left,
fsplit,
work_on_goal 2
{ dsimp at *,
fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 1
{ assumption },
simp at * } } },
intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_h, cases ᾰ_h_h_right,
induction ᾰ_h_h_right_right, induction ᾰ_h_h_right_left,
dsimp at *, fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 1 {
fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 1
{ assumption },
fsplit,
work_on_goal 1
{ refl },
refl } } },
simp at *, } },
end
/-
type mismatch at application
r ᾰ_h_h_left_w
term
ᾰ_h_h_left_w
has type
α_1
but is expected to have type
α
types contain aliased name(s): α
remark: the tactic `dedup` can be used to rename aliases
-/
```

(error at first line of example statement)

#### Kevin Buzzard (Aug 16 2022 at 21:46):

```
import logic.relation
variables {α β γ δ ε κ : Type*}
example (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → κ) :
relation.map (relation.map r f₁ g₁) f₂ g₂ = relation.map r (f₂ ∘ f₁) (g₂ ∘ g₁) :=
begin
ext1,
ext1,
simp at *,
fsplit,
work_on_goal 1
{ rintros ⟨ᾰ_w, ᾰ_h_w, ⟨ᾰ_h_h_left_w, ᾰ_h_h_left_h_w, ᾰ_h_h_left_h_h_left, rfl, rfl⟩,
rfl, rfl⟩,
refine ⟨_, _⟩,
work_on_goal 2
{ dsimp at *, -- this line breaks it; comment out to fix proof
fsplit,
work_on_goal 2 {
fsplit,
work_on_goal 1
{ assumption },
simp at * } } },
rintro ⟨ᾰ_w, ᾰ_h_w, ᾰ_h_h_left, rfl, rfl⟩,
dsimp at *,
refine ⟨_, _, ⟨_, _, ᾰ_h_h_left, rfl, rfl⟩, rfl, rfl⟩,
end
/-
type mismatch at application
r ᾰ_h_h_left_w
term
ᾰ_h_h_left_w
has type
α_1
but is expected to have type
α
types contain aliased name(s): α
remark: the tactic `dedup` can be used to rename aliases
-/
```

#### Kevin Buzzard (Aug 16 2022 at 21:46):

`tidy`

is running `dsimp`

on a goal with metavariables and on some hypotheses all at the same time

#### Kevin Buzzard (Aug 16 2022 at 21:58):

This is as compact as I can get it:

```
import logic.relation
variables {α β γ δ ε κ : Type*}
example (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → κ) :
relation.map (relation.map r f₁ g₁) f₂ g₂ = relation.map r (f₂ ∘ f₁) (g₂ ∘ g₁) :=
begin
ext1,
ext1,
simp only [eq_iff_iff],
refine ⟨_, _⟩,
{ rintros ⟨_, _, ⟨_, _, foo, rfl, rfl⟩, rfl, rfl⟩,
refine ⟨_, _⟩,
swap, -- new first goal now depends on metavariable in new second goal
{ dsimp at *, -- this line breaks it; comment out to fix proof
exact ⟨_, foo, by simp⟩, } },
{ rintro ⟨_, _, bar, rfl, rfl⟩,
exact ⟨_, _, ⟨_, _, bar, rfl, rfl⟩, rfl, rfl⟩, },
end
/-
type mismatch at application
r ᾰ_h_h_left_w
term
ᾰ_h_h_left_w
has type
α_1
but is expected to have type
α
types contain aliased name(s): α
remark: the tactic `dedup` can be used to rename aliases
-/
```

Last updated: Dec 20 2023 at 11:08 UTC