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

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