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

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

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

@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

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

What about accessing the distribution using `Pr`

?

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

(but I suspect you already noticed that)

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

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?

Maybe you could share your source file?

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

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.

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.

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.

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)

(and I would expect `validate_postcond`

to be parameterized by `x`

and `y`

here)

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

maybe `state`

’d better be with range say `ordinal 8`

for the type to be finite otherwise `[set …]`

cannot be used

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

also `validate_postcond`

cannot be `bool`

since `Pr`

isn’t

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