Stream: Coq users

Topic: Proof of p -> q


view this post on Zulip Julin S (Jan 07 2022 at 13:29):

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

view this post on Zulip Gaëtan Gilbert (Jan 07 2022 at 13:32):

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

It isn't so you won't succeed

view this post on Zulip Julin S (Jan 07 2022 at 13:33):

Oh sorry. Let me correct it.

view this post on Zulip Julin S (Jan 07 2022 at 13:34):

Wait. why is it wrong?

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 13:34):

If you have the excluded middle on p, then the first step is to destruct p \/ ~p.

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 13:35):

Otherwise, intuitionistic logic makes it unprovable.

view this post on Zulip Julin S (Jan 07 2022 at 13:43):

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

view this post on Zulip Kenji Maillard (Jan 07 2022 at 13:43):

yes

view this post on Zulip Kenji Maillard (Jan 07 2022 at 13:44):

And that statement forall (p q : Prop), ((p->q) -> (~q->~p)). is also an intuitionistic tautology

view this post on Zulip Julin S (Jan 07 2022 at 14:00):

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

view this post on Zulip Julin S (Jan 07 2022 at 14:00):

Goal is:

1 subgoal
(1 unfocused at this level)

p, q : Prop
H : p
H0 : p -> q

========================= (1 / 1)

~ p \/ q

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 14:01):

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

view this post on Zulip Julin S (Jan 07 2022 at 14:04):

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?

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 14:05):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 14:06):

it can be any of (a much larger set containing) tauto., apply H0; exact H. or refine (H0 H).

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 14:07):

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

view this post on Zulip Julin S (Jan 07 2022 at 14:11):

Thanks. doing apply followed by exact did it.

view this post on Zulip Julin S (Jan 07 2022 at 14:11):

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.

view this post on Zulip Julin S (Jan 07 2022 at 14:11):

I suppose this is the 'explicit' way?

view this post on Zulip Julin S (Jan 07 2022 at 14:12):

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

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 14:17):

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.

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 14:20):

You can type Print pq. to see what the function looks like.

view this post on Zulip Julin S (Jan 07 2022 at 16:00):

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?

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:01):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:02):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:02):

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

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 16:06):

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

view this post on Zulip Karl Palmskog (Jan 07 2022 at 16:11):

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?

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 16:15):

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.

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 16:16):

In other words, do_match is just the identity.

view this post on Zulip Karl Palmskog (Jan 07 2022 at 16:17):

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

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 16:21):

As far as I remember, yes.

view this post on Zulip Julin S (Jan 07 2022 at 16:23):

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:

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:24):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:24):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:24):

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

view this post on Zulip Pierre-Marie Pédrot (Jan 07 2022 at 16:25):

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

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 16:31):

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

view this post on Zulip Karl Palmskog (Jan 07 2022 at 16:34):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 19:54):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 19:59):

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

view this post on Zulip Guillaume Melquiond (Jan 07 2022 at 20:47):

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.

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:26):

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.

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:27):

Which suggests the relevant definition is definition 26.

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:30):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:37):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:40):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:47):

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

view this post on Zulip Paolo Giarrusso (Jan 07 2022 at 22:48):

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.

view this post on Zulip Guillaume Melquiond (Jan 08 2022 at 10:01):

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.

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:06):

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.

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:07):

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.

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:10):

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

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:11):

see slide 32 in that link.

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:15):

@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 …)

view this post on Zulip Paolo Giarrusso (Jan 08 2022 at 13:20):

@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).

view this post on Zulip Julin S (Jan 08 2022 at 15:30):

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

view this post on Zulip Julin S (Jan 09 2022 at 07:18):

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?

view this post on Zulip Li-yao (Jan 09 2022 at 15:10):

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

view this post on Zulip Paolo Giarrusso (Jan 10 2022 at 00:03):

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

view this post on Zulip Julin S (Jan 10 2022 at 04:24):

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.

view this post on Zulip Li-yao (Jan 10 2022 at 04:45):

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

view this post on Zulip Julin S (Jan 10 2022 at 05:23):

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


Last updated: Mar 28 2024 at 16:02 UTC