Stream: new members

Topic: Using functions as proofs

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 $A\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?

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.

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.)

Kevin Buzzard (Mar 10 2019 at 22:34):

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

Kevin Buzzard (Mar 10 2019 at 22:34):

Actually maybe even that won't work

Mario Carneiro (Mar 10 2019 at 22:35):

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

Kevin Buzzard (Mar 10 2019 at 22:35):

You need \< pointy brackets

Kevin Buzzard (Mar 10 2019 at 22:35):

The constructor for prod has a different notation

Kevin Buzzard (Mar 10 2019 at 22:36):

However maybe pointy brackets work for the swap proof?

Thomas Scholz (Mar 11 2019 at 23:04):

Thank you all!

Last updated: May 12 2021 at 04:19 UTC