Zulip Chat Archive

Stream: general

Topic: simpa hygiene issue


view this post on Zulip Yakov Pechersky (Apr 02 2021 at 05:54):

simpa substitutes in this over existing this. Expected?

import group_theory.perm.cycles

variables {α : Type*} [decidable_eq α] {x y : α}

open list equiv equiv.perm

def list.form_perm (l : list α) : equiv.perm α :=
(list.zip_with equiv.swap l l.tail).prod

example (h : x  y) : [x, y].erase_dup.form_perm.is_cycle :=
begin
  have : nodup [x, y] := by simpa,
  simpa [erase_dup_eq_self.mpr this, form_perm] using is_cycle.swap h
  -- what is the hyp used for ^^? it is the is_cycle.swap h, not what we want
end

view this post on Zulip Yakov Pechersky (Apr 02 2021 at 05:56):

Of course, I can prove it using

simpa [erase_dup_eq_self, h, form_perm] using is_cycle.swap h

but just wanted to flag


Last updated: May 13 2021 at 06:15 UTC