John P. Pratt logic puzzle in Coq · Coq users

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.

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)

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.

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

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.

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?

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

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.

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/

Soren (May 21 2020 at 00:14):

Cyril Cohen (Jun 02 2020 at 12:35):

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

Stream: Coq users

Topic: John P. Pratt logic puzzle in Coq

Soren (May 20 2020 at 23:16):