## 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