I recently found a sort of puzzle which goes like this:

There is a bag of white and black balls.

At each step, 2 balls are taken out of the bag (they won't be returned to the bag).

- if both balls are of same colour, we keep a white ball into the bag
- otherwise, a black ball is placed into the bag

When this is repeated, we will end up having just one ball in the bag (provided we start with at least one ball in the bag).

The task is to find the color of the last ball in the bag.

The answer is black ball if we started off with odd number of black balls in the bag and white ball otherwise.

I wanted to try proving this in coq.

I made a function that does something like this:

```
Require Import List.
Import ListNotations.
Definition black := false.
Definition white := true.
Fixpoint proc (bag:list bool) : list bool :=
match bag with
| (a::b::ls) =>
match a, b with
| black, black => white::ls
| white, white => white::ls
| _, _ => black::ls
end
| _ => bag
end.
```

Then I tried to prove the case where we start off with odd number of black balls.

```
Require Import Coq.Arith.Even.
Definition booleqb (a b:bool):bool := negb (xorb a b).
Definition count (l:list bool) (val:bool) : nat :=
length (filter (fun elem => booleqb elem val) l).
Theorem proc_odd_b : forall bag:list bool,
(length bag) > 0 -> odd (count bag black) -> proc bag = [black].
Proof.
intros.
induction bag.
- simpl.
inversion H.
- induction a.
*
```

The goal became:

```
1 subgoal
a : bool
bag : list bool
H : length (a :: bag) > 0
H0 : odd (count (a :: bag) false)
IHbag : length bag > 0 -> odd (count bag false) -> proc bag = [false]
========================= (1 / 1)
proc (a :: bag) = [false]
```

I was thinking that we could use

`H`

and `IHbag`

to get

```
odd (count a::bag false) -> proc a::bag = [false]
```

and then use H0 to this to get

```
proc a::bag = [false]
```

But I couldn't figure how to do this.

How can I set this right?

Did I state the theorem in a bad way?

Or am I trying to prove using a wrong method?

As far as I can tell, your `proc`

function is not recursive. So, it does not give you the last state of the bag, but only the next one. For example, `proc [black;black;black]`

will be `[white;black]`

, which is not `[black]`

, and thus a counterexample to your theorem.

Ah.. now that I come to think of it, I see that it doesn't call itself.... Thanks. Let me try fixing that.

Remarking that what matters is only the numbers of white and black balls in the bag leads to a much simpler formalization of the situation.

Lists can be OK if they represent the order in which you remove the balls from the bag, and not the contents of the bag (which may be represented as a pair of natural numbers).

A few remarks:

Your definition of `proc`

causes an error of pattern matching.

It is fixed if you define `white`

and `black`

as notations (which are expanded into the constructors `true`

and `false`

).

```
Notation black := false (only parsing).
Notation white := true (only parsing).
```

In order to call recursively `proc`

, you may tell Coq that the length of the bag is strictly decreasing along the computation.

```
Require Import Recdef.
Function proc_rec (bag: list bool) {measure length bag} :=
match bag with nil| [_] => bag
| _::_::l => proc_rec (proc bag)
end.
Proof.
intros bag b l0 b0 l; case b; case b0; simpl; auto.
Defined.
```

this seems a classic application of "invariants": the thesis follows because the number of black balls does not change, modulo 2.

In an "informal maths" text, that line might essentially be the entire proof, because everything else is "follows your nose".

(That is close to what @Li-yao wrote, but forgetting about white balls makes things even simpler. I would still keep them in the formalization of course)

in Coq, proving that `proc`

preserves this metric should be easy by case-analysis on the inputs…

in addition, I’d prove by induction that `l <> [] -> length (proc_rec l) = 1`

, and then prove the top-level theorem `proc_rec_odd`

by nested case-analysis on `proc_rec l`

We may also formalize this puzzle as a transition system, by a binary relation over nat*nat and its transitive closure (proc makes the game quite deterministic)

Li-yao said:

Remarking that what matters is only the numbers of white and black balls in the bag leads to a much simpler formalization of the situation.

I didn't get that right. If we just use the number of black and white balls, we would be losing the order in which the balls show up, right?

Pierre Castéran said:

Lists can be OK if they represent the order in which you remove the balls from the bag, and not the contents of the bag (which may be represented as a pair of natural numbers).

A few remarks:

Your definition of`proc`

causes an error of pattern matching.

It is fixed if you define`white`

and`black`

as notations (which are expanded into the constructors`true`

and`false`

).`Notation black := false. Notation white := true.`

In order to call recursively

`proc`

, you may tell Coq that the length of the bag is strictly decreasing along the computation.`Require Import Recdef. Function proc_rec (bag: list bool) {measure length bag} := match bag with nil| [_] => bag | _::_::l => proc_rec (proc bag) end. Proof. intros bag b l0 b0 l; case b; case b0; simpl; auto. Defined.`

I couldn't complete this.

How would we define `proc`

for use with `proc_rec`

?

What do the things in `Recdef`

do? From what I could gather from here, is it a more 'capable' form of `Fixpoint`

?

Is doing `measure`

and having `struct`

do the same thing in Coq?

Could it be that we can't have function application in the case of `struct`

?

I had thought doing a simple `Definition`

and a simple notation would be effectively same.

Is it that the `Definition`

version would lead to the creation of a new type or something?

Never realized that we could sort of 'short' two pattern matches together like

```
match a with
| one | two => result
end.
```

I always did

```
match a with
| one => result
| two => result
end.
```

`proc_rec`

was written for your version of `proc`

(Btw, it would be better to represent colors with an inductive type with two constructors `black`

and `white`

instead of booleans).

Note that `proc`

makes implicit an hypothesis: the new ball you put in the bag will be taken first (as in a stack). Thus, we prove only properties of a given behaviour.

The following formalization doen't make such hypotheses. I represent a bag as a pair of numbers, but I consider all behaviours.

```
Require Import Relations Arith Lia.
Record bag := Bag{black_of : nat; white_of: nat}.
(* one turn *)
Inductive step : relation bag :=
bb: forall b w, step (Bag (S (S b)) w) (Bag b (S w))
| ww: forall b w, step (Bag b (S (S w))) (Bag b (S w))
| bw: forall b w, step (Bag (S b) (S w)) (Bag (S b) w) .
(* a game is a sequence of steps *)
Definition game := clos_refl_trans _ step.
(* Dynamic invariant *)
Definition inv (b b': bag) :Prop := Nat.odd (black_of b) = Nat.odd (black_of b').
Lemma step_invariant b b' : step b b' -> inv b b'.
inversion 1; unfold inv; cbn; auto.
Qed.
Lemma game_invariant b b' : game b b' -> inv b b'.
Proof.
induction 1.
- now apply step_invariant.
- reflexivity.
- unfold inv; now transitivity (Nat.odd (black_of y)).
Qed.
Lemma alive x y : (exists b', step (Bag x y) b') <->
(2 <= x + y).
Proof.
split.
- intros [b' H]; inversion H; try lia.
- destruct x, y.
+ inversion 1.
+ destruct y; [lia |].
* exists (Bag 0 (S y)); constructor.
+ destruct x; [lia |].
* exists (Bag x 1); constructor.
+ exists (Bag (S x) y); constructor.
Qed.
```

Julin S said:

I didn't get that right. If we just use the number of black and white balls, we would be losing the order in which the balls show up, right?

The order does not matter. Every time you take from a bag the result can be any two balls from the bag.

Or said otherwise: bags are not ordered (in programming, and the real world), so it’s the list that is weird…

Writing the list fixes (in advance) the order in which balls are going to be extracted — here one could prove that’s equivalent to what actually happens, but your original version skips that. Pierre Castéran’s formalization is instead more faithful to the process.

A very basic doubt, but what does the `1`

in `induction 1`

mean? in the proof for `game_invariant`

?

It changed the goal from

```
1 subgoal
bin, bout : bag
========================= (1 / 1)
process bin bout -> invariant bin bout
```

to

```
3 subgoals
x, y : bag
H : step x y
========================= (1 / 3)
invariant x y
========================= (2 / 3)
invariant x x
========================= (3 / 3)
invariant x z
```

Julin S said:

A very basic doubt, but what does the

`1`

in`induction 1`

mean? in the proof for`game_invariant`

?

Induction on the first universally quantifier variable in the goal (here, the one of type `process bin bout`

, which appears as an arrow type because the rest of the goal does not depend on it, but still is a universal quantification under the hood)

In general, `induction n`

(with `n`

a concrete integer, like `4`

) introduces `n-1`

variables, and performs induction on the `n`

-th one

Okay. Is there another way to do the same 'goal transformation' in this case?

I had blindly tried doing `induction bin`

and `induction process`

but neither worked.

Is using the `1`

in `induction 1`

the only way?

I mean is there another way of saying `induction 1`

in this case?

You can do `intros x. induction x.`

The point of `induction 1`

is mostly that you do not have to introduce a name when you do not need to.

Last updated: Jan 29 2023 at 03:28 UTC