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

- I can't use Coq to find the solution for me
- 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)

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.

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

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.

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

?

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

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

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/

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

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

Last updated: Jun 24 2024 at 01:01 UTC