Zulip Chat Archive

Stream: general

Topic: tidy issue


Kevin Buzzard (Sep 24 2020 at 17:27):

This works

import tactic

variables (X Y : Type)


example :  (T : Type) (f : T  X) (g : T  Y),
∃! h : T  X × Y, prod.fst  h = f  prod.snd  h = g :=
begin
  intros,
  use [λ t, (f t, g t)],
  tidy, -- works fine
end

but if you bump the tidy above the use the tactic reports that it's solved the goal but the kernel doesn't buy it. The error if you just prove the example by tidy is

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

Is this a known issue?

Bhavik Mehta (Sep 24 2020 at 17:40):

Curiously enough, the issue disappears if you use

example (T : Type) (f : T  X) (g : T  Y) :
∃! h : T  X × Y, prod.fst  h = f  prod.snd  h = g :=
begin
  tidy,
end

Bhavik Mehta (Sep 24 2020 at 17:51):

Here's a more minimal example, showing that it's not an issue with tidy (but maybe an issue with dsimp?)

example :  (T : Type) (f : T  X) (g : T  Y),
∃! h : T  X × Y, prod.fst  h = f  prod.snd  h = g :=
begin
  intros,
  refine λ t, _, _⟩, _, _⟩,
  work_on_goal 2 { dsimp at *, refine rfl, rfl },
  rintros _ rfl, rfl⟩,
  dsimp at *,
  simp at *,
end

fails, but if you remove the dsimp inside the work_on_goal, it's fine

Kevin Buzzard (Sep 24 2020 at 18:19):

Nice! I only put the foralls in explicitly because I was imagining explaining it to a class.

Bhavik Mehta (Sep 24 2020 at 18:24):

This reminds me of: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20and.20dedup


Last updated: Dec 20 2023 at 11:08 UTC