constructing proofs by hand

Stream: general

[Scott Morrison]

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]

(deleted)

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

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]

but quotations are much nicer

[Kenny Lau]

so people are making programs that program

[Scott Morrison]

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

[Mario Carneiro]

you might even call them... metaprograms

[Simon Hudon]

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]

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]

isn't that what dictionaries do?

[Sean Leather]

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

[Sean Leather]

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

[Sean Leather]

The end of the world is nigh!

[Simon Hudon]

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

[Sean Leather]

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

[Kenny Lau]

i'm high rn

[Kenny Lau]

high on homological algebra / wedderburn's theorem