Julin S (Jun 02 2022 at 16:46): 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?
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.
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.
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.
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.
this seems a classic application of "invariants": the thesis follows because the number of black balls does not change, modulo 2.
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".
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)
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…
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
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)
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?
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 ofproccauses an error of pattern matching.
It is fixed if you definewhiteandblackas notations (which are expanded into the constructorstrueandfalse).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 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.
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.
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…
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.
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
Julin S said:
A very basic doubt, but what does the
1ininduction 1mean? in the proof forgame_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)
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
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?
Julin S (Jun 07 2022 at 09:04):I mean is there another way of saying induction 1 in this case?
Meven Lennon-Bertrand (Jun 07 2022 at 09:05):You can do intros x. induction x.
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: Oct 13 2024 at 01:02 UTC