Zulip Chat Archive

Stream: general

Topic: constructing proofs by hand


Scott Morrison (Apr 10 2018 at 03:25):

If I have X Y Z : expr, and a P : expr representing a proof that X = Y, how do I make the expression that says (X = Z) = (Y = Z)?

Scott Morrison (Apr 10 2018 at 03:26):

(deleted)

Simon Hudon (Apr 10 2018 at 03:30):

to_expr ``(congr_arg (λ x, x = %%Z) %%P)

Scott Morrison (Apr 10 2018 at 03:34):

woah, okay, that's much better than what I was doing.

Scott Morrison (Apr 10 2018 at 03:34):

I was trying things along the lines of

eq ← mk_const `eq,
prf' ← mk_congr_arg eq prf,
prf' ← mk_congr_fun prf' rhs,
 ````

Scott Morrison (Apr 10 2018 at 03:34):

but quotations are much nicer

Kenny Lau (Apr 10 2018 at 03:35):

so people are making programs that program

Scott Morrison (Apr 10 2018 at 03:35):

@Kenny Lau, this has been happening since the dawn of time :-)

Mario Carneiro (Apr 10 2018 at 03:35):

you might even call them... metaprograms

Simon Hudon (Apr 10 2018 at 03:53):

I guess now is a good time to bring up the Curry-Howard-Lambek correspondence and point out that, similarly, you can use a logical system to show that another logic is sound or complete. You can also use category theory to study the category of categories

Sean Leather (Apr 10 2018 at 06:36):

Whoa, slow down there, @Simon Hudon. Next thing you know, we'll be using English to describe... English. (Or choose your preferred self-describing language of choice.)

Kenny Lau (Apr 10 2018 at 06:36):

isn't that what dictionaries do?

Sean Leather (Apr 10 2018 at 06:36):

Also, hi, everyone. :wave: I've been away for a while.

Sean Leather (Apr 10 2018 at 06:37):

@Kenny Lau OMG! You mean it's already happening?!

Sean Leather (Apr 10 2018 at 06:37):

The end of the world is nigh!

Simon Hudon (Apr 10 2018 at 06:37):

Hi Sean! We missed you! I hope you still managed to get your daily recommended dose of math and nerdiness ;-)

Sean Leather (Apr 10 2018 at 06:38):

I tried here and there, but nothing came close to this. :wink:

Kenny Lau (Apr 10 2018 at 06:39):

i'm high rn

Kenny Lau (Apr 10 2018 at 06:39):

high on homological algebra / wedderburn's theorem


Last updated: Dec 20 2023 at 11:08 UTC