# 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' :=
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 (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