I was trying to prove `p → q`

is same as `~p ∨ q`

in Coq.

How would we do it?

Is the correct way of stating it?

```
Lemma foo : forall (p q : Prop), (p -> q) -> (~p \/ q).
Proof.
intros.
(* not sure what should be next *)
```

Or should the statement be `forall (p q : Prop), ((p->q) -> (~q->~p)).`

(found here)?

I was trying to prove p → q is same as ~p ∨ q in Coq.

It isn't so you won't succeed

Oh sorry. Let me correct it.

Wait. why is it wrong?

If you have the excluded middle on `p`

, then the first step is to destruct `p \/ ~p`

.

Otherwise, intuitionistic logic makes it unprovable.

Could making the statement

```
Lemma pq : forall (p q : Prop), (p \/ ~p) -> (p -> q) -> (~p \/ q).
Proof.
intros p q H H0.
destruct H.
```

make it provable? (I'm not that familiar with logic yet).

yes

And that statement `forall (p q : Prop), ((p->q) -> (~q->~p)).`

is also an intuitionistic tautology

I guess the proof for this lemma could be something like

```
| 1 | p ∨ ~p | Premise |
| 2 | p → q | Premise |
|---+--------+------------|
| 3 | p | Assumption |
| 4 | q | →i 3,2 |
|---+--------+------------|
| 5 | q | Assumption |
|---+--------+------------|
| 6 | q | →i 3-6 |
| 7 | ¬p ∨ q | ∨i₂ 6 |
```

I think I reached step 3 with the `destruct`

. How can I reach step 4 in coq?

Edit:

Just realized the above proof is wrong. I guess the correct one is:

```
+-----+--------+---------------+
| 1 | p → q | Premise |
| 2 | p ∨ ¬p | Premise (LEM) |
|-----+--------+---------------|
| +---+--------+-------------+ |
| | 3 | p | Assumption | |
| | 4 | q | →e 1,3 | |
| | 5 | ¬p ∨ q | ∨i₂ 4 | |
| +---+--------+-------------+ |
| +---+--------+-------------+ |
| | 6 | ¬p | Assumption | |
| | 7 | ¬p ∨ q | ∨i₁ 6 | |
| +---+--------+-------------+ |
| 8 | ¬p ∨ q | ∨e 2,3-5,6-7 |
+-----+--------+---------------+
```

Goal is:

```
1 subgoal
(1 unfocused at this level)
p, q : Prop
H : p
H0 : p -> q
========================= (1 / 1)
~ p \/ q
```

Tactics `left`

and `right`

allow you to select the side of a disjunction in the goal. So, here `right`

.

After doing `right`

, goal became

```
1 subgoal
(1 unfocused at this level)
p, q : Prop
H : p
H0 : p -> q
========================= (1 / 1)
q
```

How can we use `H`

and `H0`

to satisfy the goal?

depends, what kind of proof do you want? explicit? automatic? computational?

it can be any of (a much larger set containing) `tauto.`

, `apply H0; exact H.`

or `refine (H0 H).`

I'd recommend playing with explicit λ-term if you have trouble with the base logic, the table representation is a terrible linearization of the underlying tree that hides the actual stucture of the proof

Thanks. doing `apply`

followed by `exact`

did it.

```
Lemma pq : forall (p q : Prop), (p \/ ~p) -> (p -> q) -> (~p \/ q).
Proof.
intros p q H H0.
destruct H.
- right.
apply H0.
exact H.
- left.
exact H.
Qed.
```

I suppose this is the 'explicit' way?

Could you tell me what the explicit lambda term mean? Is it related lambda calculus or more with coq?

Both. You can see `pq`

as a function (from the lambda calculus) that takes two arguments `p`

and `q`

of type `Prop`

and two arguments of respective types `p \/ ~p`

and `p -> q`

(i.e., proofs) and returns a value of type `~p \/ q`

(i.e., a proof again). And that is exactly what Coq builds internally from your proof script. But you could also have written this lambda term directly.

You can type `Print pq.`

to see what the function looks like.

Printing the lemma gave

```
pq =
fun (p q : Prop) (H : p \/ ~ p) (H0 : p -> q) =>
match H with
| or_introl H1 => or_intror (H0 H1)
| or_intror H1 => or_introl H1
end
: forall p q : Prop, p \/ ~ p -> (p -> q) -> ~ p \/ q
Arguments pq (_ _)%type_scope _ _%function_scope
```

Was wondering, how are pattern matches implemented in simply typed lambda calculus?

... as pattern-matchings? (assuming your simply-typed λ-calculus has inductive types, like e.g. nat in System T)

but I think you're following the wrong cue. I am just saying that Coq proofs are just programs in (a somewhat rich variant of) the λ-calculus, so that you can actually look at the term to understand what the proof does

forget about "the λ-calculus", just look at Gallina terms

And if your lambda-calculus does not have pattern matching, you can simply see it as a predefined function (one per inductive type) that gets instantiated as follows: `do_match H (fun H1 => or_intror (H0 H1)) (fun H1 => or_introl H1)`

.

for the record, what's the intuition behind pattern matching when inductive types are not in the logic (but encoded using "tricks" as in CoC)? Will that also be the `do_match`

?

I am not sure which trick you are referring to, but as far as I know, the inductive value itself is the `do_match`

function then.

In other words, `do_match`

is just the identity.

I meant the approach in the Paulin-Pfenning paper if that makes sense or rings any bells...

As far as I remember, yes.

I guess I better stick to reading the Gallina terms instead of trying to convert that to lambda calculus terms.

But just to sate some curiosity...

I had been reading TAPL book by Benjamin Pierce and got only through the first 6 or so chapters. And I was wondering how pattern matching could be implemented using the bare minimum lambda calculus (don't sure if that's the right way to put it). ie, with just:

`x`

: (variable)`t t`

: (application)`λx. t`

: (abstraction)

In untyped λ-calculus, a typical way to encode inductive types is to use an "impredicative" encoding

that's the FP equivalent of the visitor pattern, aka write everything as a CPS

basically you replace an inductive term by the match tree it produces

(there are many variants of such encodings, depending on the properties you want to enforce)

After rereading the Pfenning-Paulin paper, I confirm what I wrote above: Inductive values are the matching functions themselves.

so then I guess the overall picture is clearer, if you have a typed λ-calculus *without* built-in inductive types equivalent in power to CoC, then do Pfenning-Paulin, and if untyped do an impredicative one as suggested by PMP. In between, I think there are a bunch of approaches, like what they use for HOL (natural bounded functors)?

I'm now wondering which of these encodings are Church encoding (and/or Böhm-Berarducci ones)...

From https://www.cs.cmu.edu/~fp/papers/mfps89.pdf it seems we're talking indeed about Church encodings.

It looks like Church encoding, but it is a bit different. If you look at the end of Definition 31, you should notice the difference. There you have `pair x (f z1 ... zm x)`

, while for Church encoding you would only have `f z1 ... zn x`

. That is, when recursing, you not only have access to the output of the recursor, but also its input.

I'm not sure but Definition 31 doesn't seem to be the scheme; they're talking about deriving primitive recursion from iteration, and earlier they claim (page 9) that elements are represented by their iteration function.

Which suggests the relevant definition is definition 26.

Furthermore, examples 19 and 20 look more like Church encoding than primitive recursion.

ditto example 21, tho they unhelpfully omit the representation of constructors in both naturals and lists.

their paper does suggest before definition 31 using primitive recursion as primitive, for performance (citing Parigot), but I’d expect different type signatures?

say, they’d have to use their (encoding of) pairs.

but to be clear, I haven’t studied this paper for the time the writing would demand; I’ve learned about Church encodings in the Calculus of Construction from https://homepage.cs.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf, which seems far more respectful of readers’ time.

Paolo Giarrusso said:

their paper does suggest before definition 31 using primitive recursion as primitive, for performance (citing Parigot), but I’d expect different type signatures?

No, the type signatures are mostly the same. (It depends on the kind of polymorphism you have.) Look at Definitions 1 and 2 in the paper you cited, which compare the Church and Parigot encoding of natural numbers. In one case, you have ∀, and in the other you have Π.

And it is not just a matter of performances. It is a matter of sanity. Sure, addition and multiplication of numbers are easy with Church encoding, but as soon as you try to define something as simple as the predecessor, you are in a world of pain.

If you just wanted the programmability, you could just derive primitive recursion. Making it primitive makes sense for performance, but I'm not sure how they could manage in pure CoC, at least in pure F you can't.

Also, good that we are talking of Parigot encodings, I've studied those (years ago). "mostly the same" = different; the successor takes one extra argument (of type Nat), which is completely absent in a non-dependent Church encoding.

The challenge for using this encoding as primitive is exactly this extra argument: since the type of the “successor callback” uses `Nat`

, and must be used when defining `Nat`

, you suddenly need some recursion (luckily, positive recursion: https://homepage.divms.uiowa.edu/~astump/talks/colloq-10-24-2014.pdf).

see slide 32 in that link.

@Julin S some of our replies might be unhelpful, but you can look up “Church encoding” and find tons of good tutorials (from https://en.wikipedia.org/wiki/Church_encoding to https://matt.might.net/articles/js-church/ to …)

@Julin S in any case, TAPL also shows how to extend simply-typed lambda calculus with the ingredients for datatypes (sums, products and (iso)recursive types, you can skip equirecursion); Coq also adds a (more complex) primitive for datatypes (inductive datatypes).

@Paolo Giarrusso :smiley: I couldn't understand much of the discussion but I think I could pick up on some of the terms used.

But I had read about Church encoding in TAPL itself.

Pierre-Marie Pédrot said:

the table representation is a terrible linearization of the underlying tree that hides the actual stucture of the proof

Is there a neater way of representing proof on paper?

The term you get when you print the lemma is the neater way.

That's one way but on *paper*, people (logicians) use natural deduction more often (in logic courses)

Yeah, I meant on paper. Is there any way which can make the proof more readable when compared to the table representation? I found the table representation in the book 'Logic in computer science' by Huth and Ryan.

https://en.wikipedia.org/wiki/Natural_deduction

https://incredible.pm/

Thanks for the link. A nice way to visualize small proofs.

Last updated: Sep 30 2023 at 05:01 UTC