Stream: Coq users

Topic: John P. Pratt logic puzzle in Coq


view this post on Zulip Soren (May 20 2020 at 23:16):

A few beginner questions:
I'm attempting to solve a logic puzzle using Coq, and I'm following https://cdsmith.wordpress.com/2008/05/04/solving-a-logic-problem-with-coq/ for the most part, however my problem is a bit more complex.

Here's an image of the problem statement: https://elixi.re/i/i6w4.png

So far, I have

Section Pizza.
Variable Family : Set.
Variable Colliers : Family.
Variable Leonards : Family.
Variable Morgans : Family.
Variable Nelsons : Family.
Variable Walkers : Family.
Hypothesis FamiliesAreUnique :
  Colliers <> Leonards <> Morgans <> Nelsons <> Walkers.

Am I on the right track? I'm still in high school so my knowledge of proofs is minimal.

My worries are that

  1. I can't use Coq to find the solution for me
  2. I'll be unable to properly phrase the problem

but I'm guessing that #1 could be solved with trying to prove that "the size of the solution set is exactly 1" and #2 is solved by practice?

I have a lot of Scala+programming knowledge, and a tiny bit of knowledge on the Calculus of Constructions (the lambda calculus part and not the proofs part)

view this post on Zulip Soren (May 20 2020 at 23:25):

It seems that <> isn't repeatable, but I don't want to create a matrix of every single family making it unique to every single other family.

view this post on Zulip Yannick Zakowski (May 21 2020 at 00:01):

Hello. A first important idea is the one of a (finite) inductive datatype: you only want to consider four families as simply five distinct entities. So while your idea to represent a set of all families and considering that you have five distinct elements in it, it is much simpler to define:
Inductive Families := | Colliers | Leonards | Morgans | Nelsons | Walkers
By doing so you are _defining_ a certain type that contains exactly five values, one for each family, that are distinct by construction. You therefore do not need to add an hypothesis of uniqueness.
Note that inductive datatypes are much richer and allow you to define all sort of complex types and propositions, but in particular such "finite sets".

view this post on Zulip Yannick Zakowski (May 21 2020 at 00:03):

With respect to 1., it is a much more difficult question than 2.
You should first focus indeed on formalizing your problem. That is expressing each question as an assertion (i.e. in Coq something in "Prop" typically). Answering the question consists then in proving this assertion (or disproving it, i.e. proving its negation, depending on the case).
Wondering whether there is an algorithm allowing this proof to be found automatically is an interesting question but likely to be more complex.

view this post on Zulip Soren (May 21 2020 at 00:06):

Section Pizza.

Inductive Families :=
  | Colliers | Leonards | Morgans | Nelsons | Walkers.

Inductive Toppings :=
  | Anchovy | Cheese | Mushroom | Pepperoni | Sausage.

Goal Anchovy <> Cheese /\ Colliers <> Leonards.

split.
trivial.
trivial.
Qed.

Now that I've changed to Inductive, it seems that Anchovy <> Cheese isn't ("valid"? "true"? something else?) I.e. no step is taken on either trivial.

I'm also wondering how to represent the set of prices/sizes, since they're numbers. Do I just use 12 and 3.50?

view this post on Zulip Soren (May 21 2020 at 00:09):

I think I'll try to use Coq as an "assistant" like it's meant to be used to prove that there is exactly one solution manually, and in doing so discover what the solution is(?)

view this post on Zulip Yannick Zakowski (May 21 2020 at 00:09):

Anchovy <> Cheese is actually now not worth proving per se as it is always true.
To prove it to convince yourself of the fact, it works as follow:

Goal Anchovy <> Cheese.
intros abs. (* In Coq, the negation of a fact is intuitively the capacity to derive the absurd from this fact *)
inversion abs.
Qed.

view this post on Zulip Yannick Zakowski (May 21 2020 at 00:11):

Note that your questions are very welcome of course, but you may also be interested in following part of this introductory book to familiarize yourself with the concepts and the system: https://softwarefoundations.cis.upenn.edu/

view this post on Zulip Soren (May 21 2020 at 00:14):

Ah, will give it a look! Thank you :grinning_face_with_smiling_eyes:

view this post on Zulip Cyril Cohen (Jun 02 2020 at 12:35):

I renamed the topic using more specific keywords than "beginner questions", feel free to adjust.


Last updated: Jan 29 2023 at 01:02 UTC