Library zoo.program_logic.prophet_typed

Require Import zoo.prelude.
Require Import zoo.base.
Require Import zoo.options.

Record prophet_typed :=
  { prophet_typed ۰ type : Type
  ; prophet_typed ۰ of_val : val → val → option $ option prophet_typed ۰ type
  }.

Section prophet_typed.
  Context (prophet : prophet_typed).
  Context `{zoo ۰ G : !ZooG Σ}.

  Implicit Type uproph : val × val.
  Implicit Type uprophs : list (val × val).
  Implicit Type oproph : option prophet.(prophet_typed ۰ type).
  Implicit Type proph : prophet.(prophet_typed ۰ type).
  Implicit Type prophs : list prophet.(prophet_typed ۰ type).

  #[local] Fixpoint prophet_typed ۰ process uprophs :=
    match uprophs with
    | [] ⇒
        []
    | (w, v) :: uprophs ⇒
        match prophet.(prophet_typed ۰ of_val) w v with
        | None ⇒
            []
        | Some None ⇒
            prophet_typed ۰ process uprophs
        | Some (Some proph) ⇒
            proph :: prophet_typed ۰ process uprophs
        end
    end.

  Definition prophet_typed ۰ model pid prophs : iProp Σ :=
    ∃ uprophs ,
    ⌜prophs = prophet_typed ۰ process uprophs ⌝ ∗
    prophet ۰ model pid uprophs.
  #[local] Instance : CustomIpat "model" :=
    " ( %uprophs & %Hprophs & Hpid ) ".

  #[global] Instance prophet_typed ۰ model ｰ timeless pid prophs :
    Timeless (prophet_typed ۰ model pid prophs).

  Lemma prophet_typed ۰ model ｰ exclusive pid prophs1 prophs2 :
    prophet_typed ۰ model pid prophs1 -∗
    prophet_typed ۰ model pid prophs2 -∗
    False.

  Lemma prophet_typed ｰ wp ｰ proph E :
    {{{
      True
    }}}
      Proph @ E
    {{{
      pid prophs
    , RET #pid ;
      prophet_typed ۰ model pid prophs
    }}}.

  Lemma prophet_typed ｰ wp ｰ resolve e pid v prophs E Φ :
    Atomic e →
    to_val e = None →
    prophet_typed ۰ model pid prophs -∗
    WP e @ E {{ w ,
      ∃ oproph ,
      ⌜prophet.(prophet_typed ۰ of_val) w v = Some oproph ⌝ ∗
      match oproph with
      | None ⇒
          prophet_typed ۰ model pid prophs -∗
          Φ w
      | Some proph ⇒
          ∀ prophs',
          ⌜prophs = proph :: prophs'⌝ -∗
          prophet_typed ۰ model pid prophs' -∗
          Φ w
      end
    }} -∗
    WP Resolve e #pid v @ E {{ Φ }}.
End prophet_typed.

#[global] Opaque prophet_typed ۰ model.

Record prophet_typed₁ :=
  { prophet_typed₁ ۰ type : Type
  ; prophet_typed₁ ۰ of_val : val → val → option $ option prophet_typed₁ ۰ type

  ; #[global] prophet_typed₁ ۰ type ｰ inhabited ::
      Inhabited prophet_typed₁ ۰ type
  }.

Section prophet_typed₁.
  Context (prophet : prophet_typed₁).
  Context `{zoo ۰ G : !ZooG Σ}.

  Implicit Type oproph : option prophet.(prophet_typed₁ ۰ type).
  Implicit Type proph : prophet.(prophet_typed₁ ۰ type).
  Implicit Type prophs : list prophet.(prophet_typed₁ ۰ type).

  Definition prophet_typed₁ ۰ to_prophet :=
    {|prophet_typed ۰ type :=
        prophet.(prophet_typed₁ ۰ type)
    ; prophet_typed ۰ of_val :=
        prophet.(prophet_typed₁ ۰ of_val)
    |}.

  Definition prophet_typed₁ ۰ model pid proph : iProp Σ :=
    ∃ prophs ,
    prophet_typed ۰ model prophet_typed₁ ۰ to_prophet pid prophs ∗
    ⌜if prophs is proph' :: _ then proph' = proph else True ⌝.
  #[local] Instance : CustomIpat "model" :=
    " ( %prophs{} & Hmodel{} & % ) ".

  #[global] Instance prophet_typed₁ ۰ model ｰ timeless pid proph :
    Timeless (prophet_typed₁ ۰ model pid proph).

  Lemma prophet_typed₁ ۰ model ｰ exclusive pid proph1 proph2 :
    prophet_typed₁ ۰ model pid proph1 -∗
    prophet_typed₁ ۰ model pid proph2 -∗
    False.

  Lemma prophet_typed₁ ｰ wp ｰ proph E :
    {{{
      True
    }}}
      Proph @ E
    {{{
      pid proph
    , RET #pid ;
      prophet_typed₁ ۰ model pid proph
    }}}.

  Lemma prophet_typed₁ ｰ wp ｰ resolve e pid v proph E Φ :
    Atomic e →
    to_val e = None →
    prophet_typed₁ ۰ model pid proph -∗
    WP e @ E {{ w ,
      ∃ oproph ,
      ⌜prophet.(prophet_typed₁ ۰ of_val) w v = Some oproph ⌝ ∗
      match oproph with
      | None ⇒
          Φ w
      | Some proph' ⇒
          ⌜proph = proph'⌝ -∗
          Φ w
      end
    }} -∗
    WP Resolve e #pid v @ E {{ Φ }}.
End prophet_typed₁.

#[global] Opaque prophet_typed₁ ۰ model.

Coercion prophet_typed₁ ۰ to_prophet : prophet_typed₁ >-> prophet_typed.