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.
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).
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" (
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: Jan 29 2023 at 03:28 UTC