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: Oct 13 2024 at 01:02 UTC