## Stream: general

#### Mario Carneiro (Apr 02 2018 at 10:19):

that's correct (modulo funny business regarding algorithmic equality not really being definitional equality)

#### Kenny Lau (Apr 02 2018 at 10:19):

could you expand on your parentheses

#### Mario Carneiro (Apr 02 2018 at 10:20):

Sometimes lean doesn't know when to eta expand stuff

#### Kenny Lau (Apr 02 2018 at 10:20):

could you provide an example

#### Mario Carneiro (Apr 02 2018 at 10:24):

def foo : true = true → plift true := @eq.rec Prop true (λ p, plift true) ⟨trivial⟩ true
def bar : true = true → plift true := @eq.rec Prop true (λ p, plift p) ⟨trivial⟩ true
example : foo = bar := funext \$ λ x, rfl
example : foo = bar := rfl


#### Kenny Lau (Apr 02 2018 at 10:25):

ah, that funny rec business

#### Patrick Massot (Apr 02 2018 at 10:25):

Mario, aren't you sleeping?

LOL

#### Kevin Buzzard (Apr 02 2018 at 11:40):

I found myself writing this yesterday:

#### Kevin Buzzard (Apr 02 2018 at 11:40):

Hid :=  λ U OU,funext (λ x,subtype.eq rfl),
Hcomp :=  λ U V W OU OV OW HUV HVW,funext (λ x, subtype.eq rfl)


#### Kevin Buzzard (Apr 02 2018 at 11:40):

and I couldn't move the rfl

#### Kenny Lau (Apr 02 2018 at 11:40):

subtype.eq rfl cannot be replaced by rfl

#### Kevin Buzzard (Apr 02 2018 at 11:40):

and I could understand why subtype.eq wasn't a simp lemma

#### Kenny Lau (Apr 02 2018 at 11:41):

well it's just congr

#### Kevin Buzzard (Apr 02 2018 at 11:41):

because it's  a1.val = a2.val → a1 = a2

#### Kevin Buzzard (Apr 02 2018 at 11:41):

which doesn't look great for simp

but then I found

#### Kevin Buzzard (Apr 02 2018 at 11:42):

subtype.mk_eq_mk

#### Kevin Buzzard (Apr 02 2018 at 11:42):

which is an iff and is marked as a simp lemma

#### Kevin Buzzard (Apr 02 2018 at 11:43):

so I was hopeful that by simp would work, but I couldn't get it to

Last updated: May 08 2021 at 19:11 UTC