Julin S (Jan 07 2022 at 13:29): 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)?
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
Julin S (Jan 07 2022 at 13:33):Oh sorry. Let me correct it.
Julin S (Jan 07 2022 at 13:34):Wait. why is it wrong?
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.
Guillaume Melquiond (Jan 07 2022 at 13:35):Otherwise, intuitionistic logic makes it unprovable.
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).
Kenji Maillard (Jan 07 2022 at 13:43):yes
Kenji Maillard (Jan 07 2022 at 13:44):And that statement forall (p q : Prop), ((p->q) -> (~q->~p)). is also an intuitionistic tautology
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 |
+-----+--------+---------------+
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.
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?
Pierre-Marie Pédrot (Jan 07 2022 at 14:05):depends, what kind of proof do you want? explicit? automatic? computational?
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).
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
Julin S (Jan 07 2022 at 14:11):Thanks. doing apply followed by exact did it.
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.
I suppose this is the 'explicit' way?
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?
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.
Guillaume Melquiond (Jan 07 2022 at 14:20):You can type Print pq. to see what the function looks like.
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?
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)
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
Pierre-Marie Pédrot (Jan 07 2022 at 16:02):forget about "the λ-calculus", just look at Gallina terms
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).
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?
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.
Guillaume Melquiond (Jan 07 2022 at 16:16):In other words, do_match is just the identity.
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...
Guillaume Melquiond (Jan 07 2022 at 16:21):As far as I remember, yes.
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:
x : (variable)t t : (application)λx. t : (abstraction) 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
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
Pierre-Marie Pédrot (Jan 07 2022 at 16:24):basically you replace an inductive term by the match tree it produces
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)
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.
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)?
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)...
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.
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.
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.
Paolo Giarrusso (Jan 07 2022 at 22:27):Which suggests the relevant definition is definition 26.
Paolo Giarrusso (Jan 07 2022 at 22:30):Furthermore, examples 19 and 20 look more like Church encoding than primitive recursion.
Paolo Giarrusso (Jan 07 2022 at 22:37):ditto example 21, tho they unhelpfully omit the representation of constructors in both naturals and lists.
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?
Paolo Giarrusso (Jan 07 2022 at 22:47):say, they’d have to use their (encoding of) pairs.
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.
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.
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.
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.
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).
Paolo Giarrusso (Jan 08 2022 at 13:11):see slide 32 in that link.
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 …)
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).
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.
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?
Li-yao (Jan 09 2022 at 15:10):The term you get when you print the lemma is the neater way.
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)
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.
Li-yao (Jan 10 2022 at 04:45):https://en.wikipedia.org/wiki/Natural_deduction
https://incredible.pm/
Julin S (Jan 10 2022 at 05:23):Thanks for the link. A nice way to visualize small proofs.
Last updated: Sep 30 2023 at 05:01 UTC