# Zulip Chat Archive

## Stream: general

### Topic: Curry-Howard Correspondence

#### Phiroc (Mar 16 2021 at 08:15):

Hello,

the Program Proof book (https://www.amazon.com/PROGRAM-PROOF-Samuel-Mimram/dp/B08C97TD9G/ref=sr_1_1?dchild=1&keywords=program+proof&qid=1615882109&sr=8-1) states the following on page 293:

```
As a first proof, let's show that the propositional formula
A /\ B => B /\ A
is valid. By the Curry-Howard correspondence, we want a program of the type
A x B -> B x A
showing that x is commutative.
```

Further down the page, the author provides the proof in Agda:

```
open import Data.Product
x-comm : (A B : Set) -> (A x B) -> (B x A)
x-comm A B (a , b) = (b , a)
```

A few pages later, he steps throught the proof, as follows:

```
x-comm = { }0 ---------------- (=>R) right rule or introduction rule in natural deduction
x-comm p = {}0 ---------------- (/\L) left-rule
etc.
```

I have a few questions:

- is there a
*Data.Product*data type in Lean? - let's say the multiplication sign is the Data Product sign in Lean

```
theorem x-comm {a b : Prop} (a x b) -> (b x a) := by ...
```

... how would you prove such a theorem?

Must you somewhat convert multiplication signs to /\s?

Many thanks.

Phiroc

#### Mario Carneiro (Mar 16 2021 at 08:20):

is there a Data.Product data type in Lean?

it's called `prod`

, or `A \times B`

#### Eric Wieser (Mar 16 2021 at 08:21):

I think docs#prod.swap is the "proof" you are looking for

#### Mario Carneiro (Mar 16 2021 at 08:21):

docs#and.symm is the version with /\

#### Phiroc (Mar 16 2021 at 08:27):

Thanks for the proofs. Now, can anyone explain why *A /\ B => B /\ A* is equivalent (for lack of a better term) to *A x B => B x A* ?

#### Mario Carneiro (Mar 16 2021 at 08:27):

They aren't equivalent in lean, but they are very similar looking

#### Mario Carneiro (Mar 16 2021 at 08:28):

```
def foo {A B} : A × B → B × A := λ ⟨x, y⟩, ⟨y, x⟩
def bar {A B} : A ∧ B → B ∧ A := λ ⟨x, y⟩, ⟨y, x⟩
```

#### Kenny Lau (Mar 16 2021 at 08:31):

@Phiroc that's because `/\`

is similar to `x`

#### Kenny Lau (Mar 16 2021 at 08:32):

To give a proof of `p /\ q`

is to give a proof of `p`

and a proof of `q`

#### Kenny Lau (Mar 16 2021 at 08:32):

to give an element of `A x B`

is to give an element of `A`

and an element of `B`

#### Kenny Lau (Mar 16 2021 at 08:32):

in jargon, they are both sigma types

#### Phiroc (Mar 16 2021 at 08:35):

@Kenny Lau On page 299 of the book, the author fills the proof's holes step by step, providing proofs in traditional logic syntax along the way. For instance,

```
x-comm = { }0 --------------> ? / |- A /\ B => B /\ A
```

#### Phiroc (Mar 16 2021 at 08:36):

Does it mean that he considers A x B pairs equivalent to A /\ B in this particular proof?

#### Kenny Lau (Mar 16 2021 at 08:37):

I don't understand the syntax `{ }0`

#### Kevin Buzzard (Mar 16 2021 at 08:37):

These things are not equivalent in Lean. What is going on in your resource is a question about your resource, not a question about Lean.

#### Phiroc (Mar 16 2021 at 08:38):

{ }0 is a "hole" which needs filling (C-c C-r)

#### Kenny Lau (Mar 16 2021 at 08:38):

why are you asking about Agda in a Lean chat

#### Phiroc (Mar 16 2021 at 08:39):

I'm not asking an Agda question. I am trying to understand the x-comm proof.

#### Phiroc (Mar 16 2021 at 08:41):

I'm satisfied with the answers you guys have provided.

#### Kevin Buzzard (Mar 16 2021 at 08:42):

In Lean we have a `Prop`

universe and a `Type`

universe, and there are analogies between them (e.g. prod vs and) but moving from `Prop`

to `Type`

can be tricky because `Prop`

is proof-irrelevant. So your agda thing might not port so well into Lean.

#### Phiroc (Mar 16 2021 at 08:45):

I think the explanation is as follows (in my understanding as a newbie): because Ands are Pairs, A /\ B is equivalent to A x B. So to prove A x B => B x A, you can prove A /\ B => B /\ A, or something of the sort. Case closed.

#### Eric Wieser (Mar 16 2021 at 08:47):

Is docs#pprod.swap the agda equivalent? Edit: that doesn't exist, but docs#pprod does, and is probably the analog to Agda's 'x'

#### Mario Carneiro (Mar 16 2021 at 08:48):

So to prove A x B => B x A, you can prove A /\ B => B /\ A, or something of the sort.

Well, the two proofs don't actually relate to each other - one doesn't imply the other in any nontrivial sense. Rather, they are just two proofs with the same "shape".

#### Mario Carneiro (Mar 16 2021 at 08:49):

You would be surprised how often completely different theorems can be proved with exactly the same proof text. `by simp`

and `rfl`

come up shockingly often as proof texts

Last updated: May 13 2021 at 17:42 UTC