Support for the Prop Monad

[YaZko]

This PR describes the ongoing work to provide good library support to denote non-deterministic languages with [itree]s, such as is done in Vellvm.
The gist of it is to provide an (iterative) [Prop] monad transformer, roughly of type [fun M A -> (M A -> Prop)].

The main current draft is contained in the file [Basics/MonadPropClosed], that works more specifically over a sigma type in order to only consider sets of computations closed for the underlying equivalence.

From a technical standpoint, we are currently identifying two main difficulties.

Consider the definition of [bind]: judging the membership of a computation, it should accept it if it can be decomposed into a bind such that each component essentially belong to two sets. However, when it comes to the continuation, we have a subtlety: for the [bind_ret_l] law to hold true, we need to restrict the membership check over values that the first part of the monadic computation may return (see comment in commit 1de7443 for details).
This leads us to define the typeclass MayReturn whose study is in progress. The current definition has been instantiated for the [itree E] monad, but seems to raise issue in the case of the [StateT] monad transformer. A suggestion to be looked at in details might be that rather than relating monadic computations to values (m A -> A -> Prop), we might want to related monadic transformer applied to the [itree E] monad to ones applied to the [Id] monad (T (itree E) A -> T A -> Prop).

The second difficulty comes with proving the left associativity monadic law. The intuition behind the difficulty is that we have an hypothesis stating that forall a:A, mayret ma a -> exists mb kbc, ..., i.e. a propositional hypothesis positing for each value that may be returned by the part 1 of the computation a way to break down the remaining of the computation into two parts. From this, we need to craft a concrete continuation, i.e. a function, to feed to our concrete bind.
It feels like classical reasoning is necessary, but phrasing things right is not yet clear. The current feeling is that we may need to assume the underlying monad to be pointed (so that we have a default value to return, e.g. [spin], in the absurd branches of the continuation), and that we would use an oracle to decide [mayret] in the continuation.

Finally, additional resources are:

• the file [coq/PropT.v] from the Vellvm master branch, that notably contains an instance of [Proper_bind_strong] for the [itree E] monad.
• Li-yao has some stuff on predicate transformers here that may be related https://gitlab.com/lysxia/predicate-transformers
• Lucas' branch [dijkstra_monad]

[euisuny]

Interesting subtleties while defining the Iterative Instance for PropTM:

1. Indexed quantification of loop body (commit ac87b87)

Our original definition of the MonadIter Instance of PropTM was as follows:

 Global Instance MonadIter_PropTM : MonadIter PropTM.
   exact (fun R I step i =>
            exist (fun (r: m R) => exists (step': I -> m (I + R)%type),
                     (forall j, !(step j) (step' j)) /\
                     (eqm (m := m)(CategoryOps.iter step' i) r))
                  (monad_iter_closed R I step i)).

However, this approach is problematic because it applies the same step to every iteration of the loop, which is not desirable for cases when each iteration of the loop might choose a different nondeterministic action. For instance, consider the following example.

We can define a "tt and ff printing loop", where the body of the loop is defined as the nondeterministic set of actions as follows:

I = unit
body = fun _ => {print tt; ret (inl ()); print ff; ret (inl ())}

An iteration of this body, ideally, would be {(tt + ff)*}, the possibly infinite stream of alternating printing of tt and ff. However, the above (incorrect) definition of iterating through the nondeterministic set will output {tt*; ff*}, as the existential quantifier on the step' applies to the entire iteration of the loop ((CategoryOps.iter step i)`).

As a possible fix to this problem, we can modify the existential quantifier on each step of the iteration with a natural number which indexes the loop body.

  Global Instance MonadIter_PropTM' : MonadIter PropTM.
  refine (fun (R I : Type) (step : I -> PropTM (I + R)) (i : I) =>
            exist (fun r : m R =>
           exists step' : I * nat -> m (I + R),
             (forall (n : nat) (j : I), ! (step j) (step' (j, n))) /\
             eqm (m := m) (let body :=
                  fun '(x, k) =>
                    bind (step' (x, k))
                         (fun ir : I + R =>
                            match ir with
                            | inl i0 => ret (inl (i0, S k))
                            | inr r0 => ret (inr r0)
                            end) in
                           CategoryOps.iter body (i, 0)) r)
                  (monad_iter_closed' R I step i)).

So, each (x, k) : I * nat will describe the step of the loop body at its kth iteration, allowing for a different nondeterministic choice of the propositional monad for each iteration.

2. IterUnfold: Need for classical reasoning

 forall (a b : Type) (f : Kleisli PropTM a (a + b)),
  iter f ⩯ f >>> case_ (iter f) (id_ b)

This is the IterUnfold law that needs to be proved for PropTM. By the pointwise equality defined on the underlying Prop, this becomes:

 forall (a0 : a) (x y : m b),
  x ≈ y ->
  (! (iter f a0) x -> ! ((f >>> case_ (iter f) (id_ b)) a0) y) /\
  (! ((f >>> case_ (iter f) (id_ b)) a0) y -> ! (iter f a0) x)

However, notice that in order to reason about the second case, ( (! ((f >>> case_ (iter f) (id_ b)) a0) y -> ! (iter f a0) x)), we need to classically reason about the termination of the computation on ma. That is, forall a0: a+ b, mayret ma a0 is either True or False.

The hypothesis ! ((f >>> case_ (iter f) (id_ b)) a0) y is equivalent to the statement below, which demonstrates why we need this style of classical reasoning:

exists (ma : m (a + b)) (kb : a + b -> m b),
         ! (f a0) ma /\
         (forall a0 : a + b,
          mayret ma a0 -> ! (case_ (MonadIter_PropTM' b a f) (id_ b) a0) (kb a0)) /\
         y ≈ bind ma kb

Without classical reasoning, we cannot reason about a MonadIter_PropTM where the underlying computation, ma, diverges. (Additionally, we cannot arbitrarily derive from the context that mayret ma a0 would hold.)

[euisuny]

Some notes with the experiment on defining PropTM with a generalized notion of eqM (on definitions that didn't work, and why).

1. Initial eqmR PropTM definition

Our initial attempt at defining the eqmR instance for PropTM gave the following definition to eqm:

Definition closed_eqmR {A B} (REL : A -> B -> Prop) (PA : m A -> Prop) 
  (PB : m B -> Prop) :=
    forall ma mb, eqmR REL ma mb -> (PA ma <-> PB mb).

Definition eqm' : forall (A B : Type) (R : A -> B -> Prop), 
  PropTM A -> PropTM B -> Prop :=
    fun _ _ REL PA PB =>
      (forall x y r, eqmR r x y -> (PA x <-> PB y)) /\
      closed_eqmR PA PB REL.

Notice that (forall x y r, eqmR r x y -> (PA x <-> PB y)) is too strong for our purpose (the universal quantification on r makes a stronger claim than the closedness property stated by closed_eqmR). So we can fix this definition to this instead:

Definition closed_eqm {A} (P: m A -> Prop) := forall a a', eqm a a' -> (P a <-> P a').

Definition eqm' : forall (A B : Type) (R : A -> B -> Prop), 
  PropTM A -> PropTM B -> Prop :=
    fun _ _ REL PA PB =>
      (forall x y REL, eqmR REL x y -> (PA x <-> PB y)) /\
      closed_eqm PA /\ closed eqm PB.

However, as seen in [Awkward Proper Instance], this definition will require us to make strange claims about propositions that hold for a PropTM.

2. Awkward Proper Instance

In order to prove EqmR_OK or the monad laws with the above definition, we end up needing the following proper instance:

forall (r : A -> A -> Prop) (P : PropTM A), Proper (eqmR r ==> impl) P

Let's assume that (P : PropTM A) has an underlying monad of name m. The proper instance states that if two monads of type m A are equivalent under eqmR r, where we have the homogeneous relation r, then it implies implication under P. (For instance, eqmR r ma ma' holds for some ma and ma'of typem A, P maimpliesP ma'`.)

This is the same as the "too strong universal quantification" statement that we wanted to eliminate! We do not want this proper instance to hold true, because that would imply that our parameterized equivalence relation implies a more general notion of equivalence over more relations.

3. Current Experiment
Because of this unsound proper instance, we now trying out another way of defining eqm':

Definition eqm' : forall (A B : Type) (R: A -> B -> Prop), PropTM A -> PropTM B -> Prop :=
  (forall ma, PA ma -> exists mb, PB mb /\ eqmR R ma mb) /\
  (forall mb, PB mb -> exists ma, PA ma /\ eqmR R ma mb).

Right now, we're trying to see if proving an EqmR_OK and EqmRMonad instance for this definition makes sense in branch prop_eqmR.

[euisuny]

1. Why not "MayRet"?
MayRet doesn't seem like the appropriate formulation for stating the "continuing computation" condition on PropTM, because it is unclear how to give a StateT instance of MayRet.

2. Weaker closedness condition
Our original encoding of closedness was too strong (see last comment on this thread). But we would still like to state a notion of closure over our equivalence.

@YaZko 's proposal of a weaker closedness property:
forall ma mb, eqmR R ma mb -> PA ma -> PB mb -> (forall (ma': m A), eqmR R ma' mb -> PA ma') /\ (forall (mb': m B), eqmR R ma mb' -> PB mb').

3. Heterogeneous relations (See Basics/HeterogeneousRelations.v in prop_eqmR)---the Coq standard library only has support for homogeneous relations, so we state a heterogeneous equality definition with a notion of composition, inclusion (equivalent to "subrelations"), transpose, and define a category over relations, where the objects are types and morphisms are relations.

[euisuny]

Another note ---
Here's a paper that seems relevant to our "EqmRMonad" and "Monads with Typ" definition:
(Hughes 99, Restricted Data Types in Haskell)
https://www.researchgate.net/profile/John_Hughes13/publication/2507831_Restricted_Data_Types_in_Haskell/links/00b4952bf430de0182000000/Restricted-Data-Types-in-Haskell.pdf

Haskell's restricted data types allows the definition of monads on types with equality, which is similar to what we do (See : Section 3, Restricted Monads).