Unguarded iteration of a weak maybe monad

maybe_iter.v

Set Primitive Projections.

From Equations Require Import Equations.
Set Equations Transparent.

Record maybe (X : Type) := {
  dom : Prop ;
  val : dom -> X ;
}.
Arguments dom {X}.
Arguments val {X}.

Definition ret {X} (x : X) : maybe X := {| dom := True ; val _ := x |} .
Record sig (P : Prop) (Q : P -> Prop) : Prop := {
  fst : P ;
  snd : Q fst ;
}.
Arguments fst {P Q}.
Arguments snd {P Q}.
Notation "Σ[ p ∈ P ] Q" := (sig P (fun p => Q)) (at level 40).

Definition bnd {X Y} (u : maybe X) (f : X -> maybe Y) : maybe Y :=
  {| dom := Σ[ p ∈ u.(dom) ] (f (u.(val) p)).(dom) ;
     val p := (f _).(val) (snd p) |} .

Inductive sumP {X Y} (P : X -> Prop) (Q : Y -> Prop) : X + Y -> Prop :=
| Inl {x} : P x -> sumP P Q (inl x)
| Inr {y} : Q y -> sumP P Q (inr y) .
Arguments Inl {X Y P Q x}.
Arguments Inr {X Y P Q y}.

Equations sumP_inl {X Y P Q x} : @sumP X Y P Q (inl x) -> P x :=
  sumP_inl (Inl p) := p .

Equations sumP_inr {X Y P Q y} : @sumP X Y P Q (inr y) -> Q y :=
  sumP_inr (Inr q) := q .

Definition sumP_rect {X Y} {P : X -> Prop} {Q : Y -> Prop} (T : X + Y -> Type)
                (H1 : forall x, P x -> T (inl x))
                (H2 : forall y, Q y -> T (inr y))
                (s : X + Y) : sumP P Q s -> T s :=
  match s with
  | inl x => fun h => H1 _ (sumP_inl h)
  | inr y => fun h => H2 _ (sumP_inr h)
  end.

Inductive trace {X Y} (f : X -> maybe (Y + X)) (u : maybe (Y + X)) : Prop :=
| T (p : u.(dom)) : sumP (fun _ => True) (fun x => trace f (f x)) (u.(val) p) -> trace f u .
Arguments T {X Y f u}.

Definition trace_extr {X Y} (f : X -> maybe (Y + X)) : forall u, trace f u -> Y :=
  fix _trace_extr u t :=
    match t with
    | T p h => sumP_rect (fun _ => Y) (fun y _ => y) (fun _ t => _trace_extr _ t) _ h
    end .

Definition iter {X Y} (f : X -> maybe (Y + X)) (x : X) : maybe Y
  := {| dom := trace f (f x) ;
        val t := trace_extr f _ t |} .

Definition eqv {X} : maybe X -> maybe X -> Prop :=
  fun u v =>   (forall p : u.(dom), exists q : v.(dom), u.(val) p = v.(val) q)
          /\ (forall q : v.(dom), exists p : u.(dom), u.(val) p = v.(val) q) .

Lemma iter_unf {X Y} (f : X -> maybe (Y + X)) (x : X)
  : eqv (iter f x) (bnd (f x) (fun s => match s with inl y => ret y | inr x => iter f x end)) .
Proof.
  split.
  + intros [ p s ]; cbn.
    assert (exists q : dom match val (f x) p with
                      | inl y => ret y
                      | inr x0 => iter f x0
                      end,
    sumP_rect (fun _ : Y + X => Y) (fun (y : Y) (_ : True) => y)
      (fun (y : X) (t : trace f (f y)) => trace_extr f (f y) t) 
      (val (f x) p) s =
    val match val (f x) p with
        | inl y => ret y
        | inr x0 => iter f x0
        end q); [ | destruct H as [ q H ]; exists {| snd := q |}; exact H ].
    destruct (val (f x) p); cbn in *.
    - now exists I.
    - now exists (sumP_inr s).
  + intros [ q s ]; cbn.
    assert (exists p : sumP (fun _ => True) (fun x => trace f (f x)) ((f x).(val) q),
               trace_extr f (f x) (T _ p) = val match val (f x) q with
                                              | inl y => ret y
                                              | inr x => iter f x end s); [ | destruct H as [ p H ]; exists (T _ p); exact H ].
    cbn.
    destruct (val (f x) q); cbn.
    - now exists (Inl I).
    - now unshelve eexists (Inr _); [ exact s | ].
Qed.