Zulip Chat Archive

Stream: new members

Topic: using tactic.exact_dec_trivial implicitly

Yakov Pechersky (Apr 14 2021 at 02:17):

I've defined a way to construct a cyclic permutation, and would like to automatically prove the nodup of my cycle via tactic.exact_dec_trivial. But the way I've defined cycle.perm below means that in usage, I need to include a _ for the auto_param. Is there a way to make it implicit?

import data.list.rotate
import data.list.erase_dup
import group_theory.perm.basic

variables {α : Type*}

namespace list

def is_rotated (l l' : list α) : Prop :=  n, l.rotate n = l'

infixr ` ~r `:1000 := is_rotated

def is_rotated.setoid : setoid (list α) :=
{ r := is_rotated, iseqv := sorry }

lemma is_rotated.perm {l l' : list α} (h : l ~r l') : l ~ l' :=
exists.elim h (λ _ hl, hl  (rotate_perm _ _).symm)

lemma is_rotated.nodup_iff {l l' : list α} (h : l ~r l') : nodup l  nodup l' :=

def form_perm [decidable_eq α] (l : list α) : equiv.perm α :=
(zip_with equiv.swap l (l.rotate 1)).tail.prod

lemma form_perm_eq_of_is_rotated [decidable_eq α] {l l' : list α} (hd : nodup l) (h : l ~r l') :
  form_perm l = form_perm l' := sorry

end list

open list

def cycle (α : Type*) : Type* := quotient (@is_rotated.setoid α)

namespace cycle

instance : has_coe (list α) (cycle α) := quot.mk _

def nodup (s : cycle α) : Prop :=
quot.lift_on s nodup (λ l₁ l₂ (e : l₁ ~r l₂), propext $ e.nodup_iff)

instance [decidable_eq α] {s : cycle α} : decidable (nodup s) :=
quot.rec_on_subsingleton s (λ (l : list α), list.nodup_decidable l)

def perm_aux [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.hrec_on s (λ l h, form_perm l)
  (λ l₁ l₂ (h : l₁ ~r l₂), by {
    { exact is_rotated.nodup_iff h },
    { intros h1 h2 he,
      refine heq_of_eq _,
      rw form_perm_eq_of_is_rotated _ h,
      exact h1 } })

def perm [decidable_eq α] (s : cycle α) (h : nodup s . tactic.exact_dec_trivial) : equiv.perm α :=
s.perm_aux h

end cycle

#reduce ([1, 4, 3, 2] : cycle ).perm _ 3

Mario Carneiro (Apr 14 2021 at 02:26):

Auto params have to be the last argument, so if you pass additional things after them you need the _

Mario Carneiro (Apr 14 2021 at 02:27):

It should still trigger the tactic though

Yakov Pechersky (Apr 14 2021 at 02:27):

So auto_param will never work cleanly with things that have a coe_fn

Yakov Pechersky (Apr 14 2021 at 02:28):

Yeah, doing _ triggers is fine

Mario Carneiro (Apr 14 2021 at 02:28):

You might be able to add coe_fn or a type ascription to split it into two applications, but that won't be shorter than what you have

Yakov Pechersky (Apr 14 2021 at 02:31):

And why does something like

def perm (s : cycle α) {h : nodup s . tactic.exact_dec_trivial} : equiv.perm α :=
s.perm_aux h

complain about ill-formed expressions? Is the . tactic syntax only allowed in explicit args?

Johan Commelin (Apr 14 2021 at 04:56):

@Yakov Pechersky yes, as far as I'm aware, h needs to be explicit

Yury G. Kudryashov (Apr 14 2021 at 05:21):

. tactic.* makes the argument pseudo-implicit. If it's already implicit, how should Lean know whether you want it to deduce the argument by looking at the types, or by applying the tactic?

Last updated: Dec 20 2023 at 11:08 UTC