First, I'd like to apologize in advance if the question is vague.

I have a game. There are two players: jury and participant. First, the jury generates a random binary string of length 1000000000 with popcount set bits. popcount must be even. The participant can ask the jury how many set bits are in the range [left, right] at most 29 times. Then, the participant wins if they can provide a range [left, right] of length 500000000 and has popcount / 2 set bits. Now, I want to prove the participant always wins if they play optimally.

I know the proof already, and I want to formalize it! And first I need to know how to formalize the statement. Currently I have no idea :( Could anyone help me?

Just a guess, list functions would help a lot.

Yeah. I know I need inductive predicates and lists. Where can I learn about list functions in Coq? Stuff like map, reduce, etc.

I know I also need a function to extract a range from a list. What is that function?

I guess the hard part is I don't know how to model the interactions between the participant and the jury. And also I have to keep track of the number of times the participant asks the jury.

You can represent a strategy as a tree.

something like

```
Fixpoint strategy (questions_allowed:nat) : Type :=
match questions_allowed with
| 0 => range
| S n => range * (bool -> strategy n)
end.
Fixpoint run_strategy the_string n (s:strategy n) : range :=
match n, s with
| 0, r => r
| S k, (r, s') => run_strategy the_string k (s' (count_set_bits_in the_string r))
end.
Definition is_winning_answer the_string r := count_set_bits_in the_string r = count_set_bits_in the_string full_range / 2.
Theorem has_winning_strat : exists s : strategy 29, forall the_string, is_winning_answer the_string (run_strategy the_string _ s).
```

maybe use

```
Inductive strategy : nat -> Type :=
| Done : range -> strategy 0
| Step n : range -> (bool -> strategy n) -> strategy (S n).
```

instead of the fixpoint (they are equivalent, the inductive is a bit more annoying to work with as destruct might not be great with it but the fixpoint needs you to be careful when reducing if it's applied to a concrete nat like 29)

we don't have "random" instead we have "arbitrary" (`forall`

)

the player not knowing about the string which is chosen is expressed by writing `exists s, forall string`

instead of `forall string, exists s`

What you want to do here (counting the number of queries to an oracle) is essentially the same as this question I asked recently, so the replies there may also be useful for you: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.E2.9C.94.20Counting.20operations.20used.20by.20a.20function

It seems that the technique of choice here is to use a monad to keep track of how many queries you've made. (This makes sense, since incrementing the query count is a side effect, and monads are the usual way to model side effects in a pure functional language.)

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Sep 28 2023 at 11:01 UTC