using tactic.exact_dec_trivial implicitly

Stream: new members

[Yakov Pechersky]

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' :=
h.perm.nodup_iff

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 {
    ext,
    { 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]

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

[Mario Carneiro]

It should still trigger the tactic though

[Yakov Pechersky]

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

[Yakov Pechersky]

Yeah, doing _ triggers is fine

[Mario Carneiro]

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]

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]

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

[Yury G. Kudryashov]

. 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?