decidability of quotients

Stream: general

[Yakov Pechersky]

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]

Do they all work with lemma?

[Eric Wieser]

Remember example means def

[Kevin Buzzard]

Because the coercion could be to zmod 1?

[Yakov Pechersky]

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

[Kevin Buzzard]

docs#cycle.nodup_coe_iff

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

This is the "example is def and works out its type from the proof" thing again

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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]

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

[Yakov Pechersky]

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