tidy bug

Stream: general

[Patrick Massot]

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]

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]

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]

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]

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]

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]

Good idea Bryan!

[Bryan Gin-ge Chen]

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

[Patrick Massot]

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]

here I get exactly the same result as with tidy itself

[Patrick Massot]

google says Scott may be sleeping

[Bryan Gin-ge Chen]

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]

you erased too much

[Patrick Massot]

the choice idea is required

[Bryan Gin-ge Chen]

Oops!

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

Replacing solve_by_elim with apply_assumption gives the same strange behavior.

[Rob Lewis]

Higher order reasoning is hard!

[Patrick Massot]

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

[Patrick Massot]

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]

Of course rewriting h like this is the most un-mathematical thing you could see

[Kenny Lau]

finish and its friends

[Patrick Massot]

its friends are tauto and tidy

[Bryan Gin-ge Chen]

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]

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]

interesting

[Patrick Massot]

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]

but actually this is getting far away from what tidy suggested

[Bryan Gin-ge Chen]

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]

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]

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

[Simon Hudon]

What problem are you looking for?

[Bryan Gin-ge Chen]

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]

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

[Kenny Lau]

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]

@Patrick Massot

[Patrick Massot]

Thanks Kenny, but this is the version I don't want, because h is stated un-mathematically

[Yaël Dillies]

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]

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]

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]

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]

tidy is running dsimp on a goal with metavariables and on some hypotheses all at the same time

[Kevin Buzzard]

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
-/