# Zulip Chat Archive

## 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