Stream: Coq users

Topic: Proving a small puzzle


view this post on Zulip Julin S (Jun 02 2022 at 16:46):

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

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?

view this post on Zulip Guillaume Melquiond (Jun 02 2022 at 16:55):

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.

view this post on Zulip Julin S (Jun 02 2022 at 17:00):

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

view this post on Zulip Li-yao (Jun 02 2022 at 17:08):

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.

view this post on Zulip Pierre Castéran (Jun 02 2022 at 17:43):

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 proccauses an error of pattern matching.
It is fixed if you define whiteand blackas notations (which are expanded into the constructors trueand 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.

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 17:51):

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

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 17:53):

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

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 17:56):

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

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 18:06):

in Coq, proving that proc preserves this metric should be easy by case-analysis on the inputs…

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 18:08):

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

view this post on Zulip Pierre Castéran (Jun 02 2022 at 18:21):

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)

view this post on Zulip Julin S (Jun 05 2022 at 07:48):

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?

view this post on Zulip Julin S (Jun 05 2022 at 08:06):

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 proccauses an error of pattern matching.
It is fixed if you define whiteand blackas notations (which are expanded into the constructors trueand 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.

view this post on Zulip Pierre Castéran (Jun 05 2022 at 09:06):

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

view this post on Zulip Li-yao (Jun 05 2022 at 14:04):

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.

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 14:24):

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

view this post on Zulip Paolo Giarrusso (Jun 05 2022 at 14:30):

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.

view this post on Zulip Julin S (Jun 07 2022 at 08:54):

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

view this post on Zulip Meven Lennon-Bertrand (Jun 07 2022 at 08:58):

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)

view this post on Zulip Meven Lennon-Bertrand (Jun 07 2022 at 08:58):

In general, induction n(with n a concrete integer, like 4) introduces n-1 variables, and performs induction on the n-th one

view this post on Zulip Julin S (Jun 07 2022 at 09:01):

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?

view this post on Zulip Julin S (Jun 07 2022 at 09:04):

I mean is there another way of saying induction 1 in this case?

view this post on Zulip Meven Lennon-Bertrand (Jun 07 2022 at 09:05):

You can do intros x. induction x.

view this post on Zulip Meven Lennon-Bertrand (Jun 07 2022 at 09:05):

The point of induction 1 is mostly that you do not have to introduce a name when you do not need to.


Last updated: Mar 28 2024 at 16:02 UTC