Zulip Chat Archive

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

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

Karl Palmskog (May 21 2022 at 14:32):

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

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

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

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

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

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

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

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.

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

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

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

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

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.

Stream: math-comp users

Topic: "unpacking" Choice.sort

Andreas Wachs (May 21 2022 at 14:20):