Stream: math-comp users

Topic: "unpacking" Choice.sort


view this post on Zulip Andreas Wachs (May 21 2022 at 14:20):

Hi! I'm working with the infotheo and math-comp packages to encode a probabilistic hoare logic. I'm doing this to create a lemma of a coin flip of two coins with their sides having one or two dots. My goal is to create a lemma that states that there is a 1/2 probability that the sum of dots across the two coins will sum to 3 dots. This is done with a sampling operator $={1, 2, 3, .. , n} that randomly samples an element from a sample set.

My problem is that the distribution of states in the post condition is of type Choice.sort {dist state}, see below:

Lemma two_coins : forall x y,
  {{ fun _ => true }}
  x $={ANum 1; ANum 2} ; y $= {ANum 1; ANum 2}
  {{ fun dst => dst }}.

I'm a beginner in Coq, but just slightly less of a beginner in Haskell and I interpret this as the distribution is wrapped in a monad. I'm interested in aceessing these distributions but I am coming up empty with ideas on how to do that. Any help with this is appreciated, even telling me that I'm completely off in my thinking :)

view this post on Zulip Notification Bot (May 21 2022 at 14:24):

This topic was moved here from #Coq users > "unpacking" Choice.sort by Karl Palmskog.

view this post on Zulip Karl Palmskog (May 21 2022 at 14:25):

@Andreas Wachs I moved to the MathComp stream since this is at its core related to MathComp idioms.

view this post on Zulip Karl Palmskog (May 21 2022 at 14:30):

@Andreas Wachs have you looked at Polaris? It also uses MathComp and does a probabilistic Hoare logic via Iris, but does not use InfoTheo: https://github.com/jtassarotti/polaris

Work on Polaris eventually resulted in the coq-proba library: https://github.com/jtassarotti/coq-proba

view this post on Zulip Karl Palmskog (May 21 2022 at 14:32):

you might also find applications of Infotheo useful, such as https://github.com/affeldt-aist/monae and https://github.com/certichain/ceramist

view this post on Zulip Reynald Affeldt (May 22 2022 at 05:34):

What about accessing the distribution using Pr?

view this post on Zulip Reynald Affeldt (May 22 2022 at 05:40):

(as for Choice.sort, sort is a field of a record from the Choice module in the choice.v file of MathComp; {dist _} indeed forms a monad, see the file fsdist.v in infotheo)

view this post on Zulip Reynald Affeldt (May 22 2022 at 05:41):

(but I suspect you already noticed that)

view this post on Zulip Reynald Affeldt (May 22 2022 at 05:46):

Pr uses the type {fdist _} of distributions over a finType, most of infotheo uses {fdist _}; {dist _} was introduced later and there are some functions to go between both types

view this post on Zulip Reynald Affeldt (May 22 2022 at 05:48):

Does this help?

view this post on Zulip Andreas Wachs (May 22 2022 at 09:27):

Thank you to both of you. I have gotten out of being a little stuck, but I am unsure if my understanding of using Pr is solid, since I am very much a Coq novice.

I am having a hard time working with these events. I want to be very specific with expressing the events that I want to prove the probability of. At the moment I am unable to express that I want to consider an event where x + y = 3. I see that events are defined as sets but I'm unable to find materials online detailing how I go about this. Do you have any pointers?

view this post on Zulip Reynald Affeldt (May 22 2022 at 11:33):

Maybe you could share your source file?

view this post on Zulip Reynald Affeldt (May 22 2022 at 11:36):

(Should this turn into a post-condition using an expression such as Pr d [set xy | xy.1 + xy.2 == 3] where d is a distribution of pairs of outcomes?)

view this post on Zulip Andreas Wachs (May 22 2022 at 12:00):

For sure, I can attach it right below. Thanks a lot!

Reboot.v

What you've proposed looks like what I'm trying to express, but Coq aren't convinced about this notation it seems.

view this post on Zulip Andreas Wachs (May 22 2022 at 12:01):

I am working in the very bottom of the file, around line 310. The above code is to encode an Imp language, the Hoare triplet and some axioms on the Hoare triplet.

view this post on Zulip Andreas Wachs (May 22 2022 at 12:23):

Here is the problem area in the file that I'm struggling with

Definition validate_postcond (dst: {dist state}) : bool :=
  let dst' := fdist_of_Dist dst in Pr dst' [set st | st.x + st.y == 3].

  (*
      What is left to do in the function is to verify that the probability
      is equal to 1/2
  *)

Lemma two_coins : forall x y,
  {{ fun _ => true }}
  x $= {ANum 1; ANum 2} ; y $= {ANum 1; ANum 2}
  {{ validate_postcond }}.
Proof.
Admitted.

My Coq installation complains that The reference st.x was not found in the current environment.. I'm unsure what to do about this.

view this post on Zulip Reynald Affeldt (May 22 2022 at 13:02):

it is not obvious at first sight that st has fields x or y (the error message seems to suggest it doesn’t), there should be a way to access the contents of the x or y variables in a state st (a kind of generic “get” function that retrieves the value associated with a variable given a state and a variable)

view this post on Zulip Reynald Affeldt (May 22 2022 at 13:03):

(and I would expect validate_postcond to be parameterized by x and y here)

view this post on Zulip Andreas Wachs (May 22 2022 at 14:08):

My bad! I've been blindly writing code based on our starting point with lines of psuedocode. Indeed state doesn't have fields x and y.

What I've come to understand is that somehow I can get these xand y values from the state with these constructs:

Definition var := ordinal 4.
Definition state := {ffun var -> nat}.

Definition X: var := inord 0.
Definition Y: var := inord 1.
Definition Z: var := inord 2.
Definition W: var := inord 3.

I've attempted to rewrite the function to

Definition validate_postcond (dst: {dist state}) : bool :=
  let dst' := fdist_of_Dist dst in Pr dst' [set st | (st X) + (st Y) == 3].

But I get the error message

Illegal application (Non-functional construction):
The expression "st" of type "Finite.sort ?T"
cannot be applied to the term
 "X" : "var"

view this post on Zulip Reynald Affeldt (May 22 2022 at 14:40):

maybe state’d better be with range say ordinal 8 for the type to be finite otherwise [set …] cannot be used

view this post on Zulip Reynald Affeldt (May 22 2022 at 14:42):

(that should not prevent you from using the addition of natural numbers)

view this post on Zulip Reynald Affeldt (May 22 2022 at 14:44):

also validate_postcond cannot be bool since Pr isn’t

view this post on Zulip Andreas Wachs (May 24 2022 at 13:24):

Reynald and Karl, thank you so much for your time. Your comments were very helpful. With the additional aid of our project counsellors we progressed.


Last updated: Jan 29 2023 at 19:02 UTC