tidy variable bug

Stream: general

[Kevin Buzzard]

import tactic

example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  ( ∃ (U : set X) (H : U ∈ {V : set X | P V ∧ V ⊆ S}), x ∈ U ) ↔
    ∃ (U : set X) (hU : P U) (hUS : U ⊆ S), x ∈ U :=
begin
  tidy, -- goals accomplished but kernel complains
end

/-
type mismatch at application
  ᾰ_w ᾰ
term
  ᾰ
has type
  X_1
but is expected to have type
  X
types contain aliased name(s): X
remark: the tactic `dedup` can be used to rename aliases
-/

Shall I open an issue? I don't think this is my fault...(I changed the variable X to Y and got the same error but about Y_1)

[Arthur Paulino]

I don't think this is exactly a tidy bug. Replacing it by tidy?'s suggestion causes the same error:

import tactic

example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  ( ∃ (U : set X) (H : U ∈ {V : set X | P V ∧ V ⊆ S}), x ∈ U ) ↔
    ∃ (U : set X) (hU : P U) (hUS : U ⊆ S), x ∈ U :=
begin
  dsimp at *,
  simp at *,
  fsplit,
  work_on_goal 0
  { intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_left, fsplit,
    work_on_goal 0 { intros ᾰ },
    work_on_goal 1
    { dsimp at *, fsplit, work_on_goal 0 { assumption },
      dsimp at *, fsplit, work_on_goal 0 { assumption }, assumption } },
  intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_right, fsplit,
  work_on_goal 0 { intros ᾰ },
  work_on_goal 1
  { dsimp at *, fsplit,
    work_on_goal 0 { fsplit, work_on_goal 0 { assumption }, assumption },
    assumption },
end

[Kevin Buzzard]

I worked through this; there's a highly suspicious part of the proof where we have a goal contains metavariables and the bad kind of [] and it's solved with assumption; perhaps that's the issue.

ᾰ_h_left_left : P ᾰ_w
⊢ P (λ (ᾰ : X), ?m_1[X, S, P, x, ᾰ_w, ᾰ_h_right, ᾰ_h_left_left, ᾰ_h_left_right, ᾰ])

Could that be it?

[Kevin Buzzard]

I think goals of that nature are typically discouraged in normal play.

[Arthur Paulino]

So it's a bug in assumption?

[Arthur Paulino]

Okay I found something strange:

import tactic

example {X : Type}
  (S : set X)
  (P : set X → Prop)
  (x : X) :
  ( ∃ (U : set X) (H : U ∈ {V : set X | P V ∧ V ⊆ S}), x ∈ U ) ↔
    ∃ (U : set X) (hU : P U) (hUS : U ⊆ S), x ∈ U :=
begin
  simp at *,
  fsplit,
  work_on_goal 0
  { intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_left, fsplit,
    work_on_goal 0 { intros ᾰ },
    work_on_goal 1
    { fsplit, work_on_goal 0 { assumption },
      fsplit, work_on_goal 0 { assumption }, assumption } },
  intros ᾰ, cases ᾰ, cases ᾰ_h, cases ᾰ_h_right, fsplit,
  work_on_goal 0 { intros ᾰ },
  work_on_goal 1
  { dsimp at *, fsplit,
    { fsplit, assumption, assumption },
    assumption },
end

If you remove that last dsimp at * then the kernel accepts it