Curry-Howard Correspondence

Stream: general

[Phiroc]

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]

is there a Data.Product data type in Lean?

it's called prod, or A \times B

[Eric Wieser]

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

[Mario Carneiro]

docs#and.symm is the version with /\

[Phiroc]

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]

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

[Mario Carneiro]

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]

@Phiroc that's because /\ is similar to x

[Kenny Lau]

To give a proof of p /\ q is to give a proof of p and a proof of q

[Kenny Lau]

to give an element of A x B is to give an element of A and an element of B

[Kenny Lau]

in jargon, they are both sigma types

[Phiroc]

@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]

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

[Kenny Lau]

I don't understand the syntax { }0

[Kevin Buzzard]

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]

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

[Kenny Lau]

why are you asking about Agda in a Lean chat

[Phiroc]

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

[Phiroc]

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

[Kevin Buzzard]

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]

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]

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]

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]

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