Zulip Chat Archive

Stream: new members

Topic: Using functions as proofs


view this post on Zulip Thomas Scholz (Mar 10 2019 at 22:23):

I have defined the following function swap:

def swap {A B : Type} : A × B  B × A :=
fun x, (x.2, x.1)

Because of propositions-as-types, I thought this would, at the same time, be a proof of ABBAA\land B\implies B\land A.
But apparently I can't use the function swap as a proof:

constants C D : Prop
def swap_thm : C  D  D  C :=
fun y, swap y

So how can I make this work?
Or do I have to define proofs and functions separately, even if they are essentially the same?

view this post on Zulip Mario Carneiro (Mar 10 2019 at 22:30):

You should use Sort instead of Type if you want it to apply in both contexts. But this still won't work, because prod is not the same constant as and, although they have parallel definitions.

view this post on Zulip Mario Carneiro (Mar 10 2019 at 22:32):

In lean they are separate because if prod had the type Sort u -> Sort v -> Sort (max u v) (so that it could also work on proofs) then the generated recursor would be weaker. (Actually maybe not in this case, I'm not positive; and is a subsingleton eliminator which complicates things.)

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 22:34):

You can copy your definition of the swap function and get a proof of the theorem :-)

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 22:34):

Actually maybe even that won't work

view this post on Zulip Mario Carneiro (Mar 10 2019 at 22:35):

you would have to use the angle brackets, but then I think it would work

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 22:35):

You need \< pointy brackets

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 22:35):

The constructor for prod has a different notation

view this post on Zulip Kevin Buzzard (Mar 10 2019 at 22:36):

However maybe pointy brackets work for the swap proof?

view this post on Zulip Thomas Scholz (Mar 11 2019 at 23:04):

Thank you all!


Last updated: May 12 2021 at 04:19 UTC