## Stream: general

### Topic: propext, quot.sound and eq.rec

#### Chris Hughes (Oct 09 2018 at 11:44):

Is every nat defined using propext, quot.sound and eq.rec but without choice guaranteed to reduce to succ $succ$ succ ... zero?

#### Gabriel Ebner (Oct 09 2018 at 16:19):

You don't even need quot.sound:

lemma not_refl : true = (true ∨ false) :=
propext (by simp)

def does_not_reduce_to_zero : ℕ :=

#### Kenny Lau (Oct 13 2018 at 07:54):

but this error I found, it doesn't affect canonicity?

#### Mario Carneiro (Oct 13 2018 at 07:55):

no because nothing there is an axiomatic constant

#### Mario Carneiro (Oct 13 2018 at 07:55):

it's all a layer over the real inductive type

#### Mario Carneiro (Oct 13 2018 at 07:55):

That theorem has to be proven by cases or induction or something internally so it's not defeq

#### Kevin Buzzard (Oct 13 2018 at 08:02):

(warning: amateur alert). So this is exactly the situation where you can't prove your example by rfl (even though to naive eyes it looks like it should be rfl) so you prove it by hand (possibly using some weird theorems with weird names with _ at the beginning), give it a good name, mark it as a simp lemma, and move on.

yes

#### Mario Carneiro (Oct 13 2018 at 08:02):

except in this case lean did it all for you and slapped a nice API over the whole thing

#### Mario Carneiro (Oct 13 2018 at 08:03):

In this case you can write by rw bad.to_list and it will use the equation lemmas for bad.to_list, which in this case are actually nontrivial theorems

#### Kenny Lau (Oct 13 2018 at 08:07):

inductive bad : Type

/-
-/


#### Mario Carneiro (Oct 13 2018 at 08:10):

this is just a funny way of writing bad.to_list.equations._eqn_1 L of course

#### Gabriel Ebner (Oct 13 2018 at 09:33):

@Mario Carneiro Thanks for the explanation, I'm looking forward to the canonicity result. Tiny nitpick:

it is not the case that i.e. propext iff.rfl reduces to rfl, which can spoil the inductive recursor case later.

In this particular case it actually works out since propext iff.rfl has type a = a for some a, and then eq.rec reduces by axiom K.

Last updated: May 13 2021 at 22:15 UTC