Zulip Chat Archive

Stream: general

Topic: Curry-Howard Correspondence


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 16 2021 at 08:21):

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

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:21):

docs#and.symm is the version with /\

view this post on Zulip 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 ?

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:27):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 16 2021 at 08:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 16 2021 at 08:32):

in jargon, they are both sigma types

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Mar 16 2021 at 08:37):

I don't understand the syntax { }0

view this post on Zulip 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.

view this post on Zulip Phiroc (Mar 16 2021 at 08:38):

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

view this post on Zulip Kenny Lau (Mar 16 2021 at 08:38):

why are you asking about Agda in a Lean chat

view this post on Zulip Phiroc (Mar 16 2021 at 08:39):

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

view this post on Zulip Phiroc (Mar 16 2021 at 08:41):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip 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".

view this post on Zulip 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