Stream: Coq users

Topic: ✔ Formalize a game


view this post on Zulip Huỳnh Trần Khanh (Sep 10 2022 at 13:14):

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?

view this post on Zulip abab9579 (Sep 10 2022 at 13:20):

Just a guess, list functions would help a lot.

view this post on Zulip Huỳnh Trần Khanh (Sep 10 2022 at 13:22):

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

view this post on Zulip Huỳnh Trần Khanh (Sep 10 2022 at 13:23):

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

view this post on Zulip Huỳnh Trần Khanh (Sep 10 2022 at 13:28):

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.

view this post on Zulip Li-yao (Sep 10 2022 at 13:33):

You can represent a strategy as a tree.

view this post on Zulip Gaëtan Gilbert (Sep 10 2022 at 14:42):

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)

view this post on Zulip Gaëtan Gilbert (Sep 10 2022 at 14:44):

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

view this post on Zulip Malcolm Sharpe (Sep 10 2022 at 17:21):

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

view this post on Zulip Notification Bot (Sep 11 2022 at 06:01):

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


Last updated: Oct 13 2024 at 01:02 UTC