Stream: math-comp users

Topic: "unpacking" Choice.sort

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

Notification Bot (May 21 2022 at 14:24):

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

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.

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

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

Reynald Affeldt (May 22 2022 at 05:34):

What about accessing the distribution using `Pr`?

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)

Reynald Affeldt (May 22 2022 at 05:41):

(but I suspect you already noticed that)

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

Does this help?

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?

Reynald Affeldt (May 22 2022 at 11:33):

Maybe you could share your source file?

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

Andreas Wachs (May 22 2022 at 12:00):

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

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

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.

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

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

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)

Reynald Affeldt (May 22 2022 at 13:03):

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

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 `x`and `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"
``````

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

Reynald Affeldt (May 22 2022 at 14:42):

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

Reynald Affeldt (May 22 2022 at 14:44):

also `validate_postcond` cannot be `bool` since `Pr` isn’t