Zulip Chat Archive

Stream: general

Topic: funext $ λ x, rfl


view this post on Zulip Kenny Lau (Apr 02 2018 at 10:16):

conjecture: everything that can be proven using funext $ λ x, rfl can be proven using rfl

view this post on Zulip Mario Carneiro (Apr 02 2018 at 10:19):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:19):

could you expand on your parentheses

view this post on Zulip Mario Carneiro (Apr 02 2018 at 10:20):

Sometimes lean doesn't know when to eta expand stuff

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:20):

could you provide an example

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:25):

ah, that funny rec business

view this post on Zulip Patrick Massot (Apr 02 2018 at 10:25):

Mario, aren't you sleeping?

view this post on Zulip Kenny Lau (Apr 02 2018 at 10:25):

LOL

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:40):

I found myself writing this yesterday:

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:40):

and I couldn't move the rfl

view this post on Zulip Kenny Lau (Apr 02 2018 at 11:40):

subtype.eq rfl cannot be replaced by rfl

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:40):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 11:41):

well it's just congr

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:41):

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

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:41):

which doesn't look great for simp

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:41):

but then I found

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:42):

subtype.mk_eq_mk

view this post on Zulip Kevin Buzzard (Apr 02 2018 at 11:42):

which is an iff and is marked as a simp lemma

view this post on Zulip 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