# Zulip Chat Archive

## Stream: general

### Topic: decidability of quotients

#### Yakov Pechersky (Sep 30 2021 at 17:16):

What is going on in elaboration here such that the first example fails but the other ones work?

```
import data.list.cycle
example : cycle.nodup (↑[1, 2]) := dec_trivial -- why do I get two errors here?
example : cycle.nodup (↑[1, 2] : cycle ℕ) := dec_trivial
example : @cycle.nodup ℕ (↑[1, 2]) := dec_trivial
example : cycle.nodup (↑[1, 2]) := cycle.nodup_coe_iff.mpr dec_trivial
```

#### Eric Wieser (Sep 30 2021 at 18:49):

Do they all work with `lemma`

?

#### Eric Wieser (Sep 30 2021 at 18:49):

Remember `example`

means `def`

#### Kevin Buzzard (Sep 30 2021 at 22:13):

Because the coercion could be to `zmod 1`

?

#### Yakov Pechersky (Sep 30 2021 at 22:40):

If that was the case, then why would the last example work, where the type of the elements is not specified?

#### Kevin Buzzard (Oct 01 2021 at 06:42):

#### Kevin Buzzard (Oct 01 2021 at 06:45):

Because for some reason lean decides you're talking about naturals in the last one? What is the type of the term produced?

#### Kevin Buzzard (Oct 01 2021 at 06:47):

For me this lemma looks ambiguous/false. It's not true that `(1 : R) ≠ 2`

in general so whether the lemma is provable or not depends on exactly what is going on when it's elaborated.

#### Reid Barton (Oct 01 2021 at 10:34):

This is just a guess really but maybe cycle.nodup_coe_iff eliminates the `↑`

, and then defaulting kicks in. It's not really surprising that in the others, an explicit `↑`

without fixed source or target type doesn't work well.

#### Kevin Buzzard (Oct 01 2021 at 10:49):

```
import data.list.cycle
example : cycle.nodup (↑[1, 2]) := dec_trivial -- infoview says this is about `cycle ⁇`
example : cycle.nodup (↑[1, 2]) := cycle.nodup_coe_iff.mpr dec_trivial -- infoview says this is about `cycle nat`
```

#### Kevin Buzzard (Oct 01 2021 at 10:50):

I think that `↑[1, 2]`

is just a highly ambiguous thing to say. Are you talking about nats or not? If nats then say so, if not then the result isn't true. `1`

doesn't mean `1 : nat`

, it means `has_one.one`

so it could mean anything without any further clues.

#### Eric Wieser (Oct 01 2021 at 10:51):

Eric Wieser said:

Do they all work with

`lemma`

?

Since no one replied to this, no, they don't:

```
import data.list.cycle
lemma foo1 : cycle.nodup (↑[1, 2]) := dec_trivial
-- fail: don't know how to synthesize placeholder `Type ?`
lemma foo2 : cycle.nodup (↑[1, 2] : cycle ℕ) := dec_trivial
-- ok
lemma foo3 : @cycle.nodup ℕ (↑[1, 2]) := dec_trivial
-- ok
lemma foo4 : cycle.nodup (↑[1, 2]) := cycle.nodup_coe_iff.mpr dec_trivial
-- fail: don't know how to synthesize placeholder `Type ?`
```

#### Eric Wieser (Oct 01 2021 at 10:52):

This is the "`example`

is `def`

and works out its type from the proof" thing again

#### Kevin Buzzard (Oct 01 2021 at 10:52):

Oh -- even `example : cycle.nodup (↑[(1 : ℕ), 2]) := dec_trivial`

fails :-(

#### Reid Barton (Oct 01 2021 at 10:53):

even if the literals `1`

and `2`

are determined to be `nat`

, which I think Lean will do, it doesn't mean the result is `cycle nat`

, because there is no `out_param`

in the class controlling `coe`

; Lean has to imagine that you could mean `cycle`

of anything

#### Eric Wieser (Oct 01 2021 at 11:04):

There's something broken with the `has_lift_t`

resolution that I found while looking at this... I'll make a new thread

#### Yakov Pechersky (Oct 01 2021 at 12:22):

I was relying on the thought that numerals are nat (to lean 3) until notated or inferred otherwise. Perhaps the coe arrow is too powerful, and apart from allowing the list to be interpetered as a cycle, it also fuzzed the type of the numeral.

#### Yakov Pechersky (Oct 01 2021 at 12:24):

This question is around an issue of how to encode a dec_trivial for the notation I define in #9470

#### Yakov Pechersky (Oct 01 2021 at 12:25):

Where the notation constructs a list over an arbitrary type, then lifts that into a quotient, and tries to prove its nodup by brute force

Last updated: Dec 20 2023 at 11:08 UTC