Using functions as proofs

Stream: new members

[Thomas Scholz]

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]

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]

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]

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

[Kevin Buzzard]

Actually maybe even that won't work

[Mario Carneiro]

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

[Kevin Buzzard]

You need \< pointy brackets

[Kevin Buzzard]

The constructor for prod has a different notation

[Kevin Buzzard]

However maybe pointy brackets work for the swap proof?

[Thomas Scholz]

Thank you all!