text:
From stdpp Require Import namespaces.
From iris.base_logic.lib Require Import na_invariants.
From iris.algebra Require Import auth excl agree csum.
From iris_time.heap_lang Require Import proofmode notation.
From iris_time Require Import TimeCredits Auth_max_nat.

(*
  This file contains a formalization of thunks. Compared with ThunksSimple.v,
  it specifies the same HeapLang code, but the representation predicate is more
  involved, so that we can also:

    - prove that a thunk always return the same value (the user of the library
      could already do that, but it comes for free as a by-product of our
      internal ghost state),
    - prove the consequence rule (see below),
    - and pass additional (non-persistent) assertions to the suspended code.

  Postconditions of thunks are necessarily persistent.

  The consequence rule is roughly the following: if we have a thunk with debt n
  and postcondition φ, and we can update φ to ψ by also spending m time credits
  (that is, TC m ∗ φ ==∗ ψ) where both φ and ψ are persistent, then we can see
  the thunk as having debt (n+m) and postcondition ψ.

      Thunk t  n    φ        TC m ∗ φ ==∗ ψ
      =====================================∗   CONSEQUENCE
      Thunk t (n+m) ψ

  The idea is that, when forcing the thunk, not only we consume n time credits
  to run the suspended code once and get its postcondition φ, we also consume
  m time credits to “run” the ghost update once and get ψ from φ.

  It is the combination of two desirable rules:

      Thunk t  n     φ
      ==============================∗   BORROWING
      Thunk t (n+m) (φ ∗ TC m)          (* nonsensical, postcond must be persistent *)

      Thunk t n φ            φ ==∗ ψ
      ==============================∗   CONSEQUENCE'
      Thunk t n ψ

  The consequence rule allows to reason about chained thunks. Combined with the
  pay rule applied to the inner thunk, it allows to derive the following:

      Thunk t1  n1    (λ t2, Thunk t2  n2    φ)
      =========================================∗    FORWARDING OF DEBT
      Thunk t1 (n1+m) (λ t2, Thunk t2 (n2-m) φ)

  To rule out reentrency, we still have one token per thunk, which is required
  to force the thunk. To be able to force a thunk that forces a thunk, we need
  to pass the token of the inner thunk to the code suspended by the outer thunk.
  We do so by allowing to pass an arbitrary assertion R during forcing (R is
  recovered after forcing).

  Variables:

    - p: thread pool name (technical detail)
    - t: physical location of the thunk
    - γv: ghost name given to the thunk (technical detail)
    - n: apparent remaining debt (might be over-estimated)
    - R: assertion to pass to the suspended code when forcing (recovered afterwards)
    - φ: persistent predicate about the value computed by forcing
    - v: the computed value of the thunk

  Provided assertions:

    - Thunk p t γv n R φ : persistent representation predicate
    - ThunkVal γv v      : persistent assertion saying that thunk t/γv has been
                           forced and that its value is v
    - ThunkToken p t     : unique token required to force thunk t

  The representation predicate Thunk is defined inductively.

    - The “base” thunk predicate represents the bare thunk: it stores the
      physical location of the thunk.
    - A “consequence” thunk predicate is the pair of (1) a parent thunk predicate
      about the same thunk, and (2) a consequence rule to apply to this parent.

  Using the CONSEQUENCE rule, as defined earlier, simply consists in logically
  building a consequence thunk predicate on top of the provided thunk predicate.

  Thus, thunk predicates about a given thunk are the “nodes” of a tree.
  Each node stores either an operation to be performed once (when forcing),
  or the result of this operation (if already forced).

    - The base node corresponds to the physical execution of the suspended code.
      It stores either the triple for this code, or its postcondition.
    - A consequence node corresponds to the logical execution of a ghost update.
      It stores either this ghost update, or its conclusion.

  All of these operations have their own cost in time credits. The cumulated
  cost of all operations, from the base node up to the considered descendent, is
  the debt of this descendent. The user can logically reduce the debt by paying,
  i.e. storing time credits in the thunk. Each node has its own deposit, storing
  only the time credits needed for its own operation.

  Only when the debt of a node is zero, the user can physically “force” the
  thunk, i.e. evaluate it.

  Note that, when forcing a node, only this node and its ancestors, down until
  the base node, are forced. Siblings or descendents are not. So even if we know
  that we have forced some node about a thunk t already, we cannot use that
  knowledge when considering some other node about t. In fact, it is possible
  that the other node still has a non-zero debt because we haven’t paid for the
  additional consequences yet. The only thing we know is that the base node has
  indeed been forced.
 *)

Notation UNEVALUATED f := (InjL f%V) (only parsing).
Notation EVALUATED v := (InjR v%V) (only parsing).
Notation UNEVALUATEDV f := (InjLV f%V) (only parsing).
Notation EVALUATEDV v := (InjRV v%V) (only parsing).
Notation "'match:' e0 'with' 'UNEVALUATED' x1 => e1 | 'EVALUATED' x2 => e2 'end'" :=
  (Match e0 x1%bind e1 x2%bind e2)
  (e0, e1, x2, e2 at level 200, only parsing) : expr_scope.

Definition create : val :=
  λ: "f",
    ref (UNEVALUATED "f").

Definition force : val :=
  λ: "t",
    match: ! "t" with
      UNEVALUATED "f" =>
        let: "v" := "f" #() in
        "t" <- (EVALUATED "v") ;;
        "v"
    | EVALUATED "v" =>
        "v"
    end.

Section ThunkProofs.

  Notation valO := (valO heap_lang).
  Context `{timeCreditHeapG Σ}.
  Context `{inG Σ (csumR (exclR unitO) (agreeR valO))}. (* γv *)
  Context `{inG Σ (authR $ optionUR $ exclR boolO)}.    (* γforced *)
  Context `{inG Σ (authR max_natUR)}.                   (* γpaid *)
  Context `{na_invG Σ}.

  Implicit Type t : loc.
  Implicit Type f v : val.
  Implicit Type γv γforced γpaid : gname.
  Implicit Type forced : bool.
  Implicit Type n m paid k : nat.
  Implicit Type R : iProp Σ.
  Implicit Type φ ψ : val → iProp Σ.
  Implicit Type d : nat.
  Implicit Type p : na_inv_pool_name.
  Implicit Type E F : coPset.

  Definition thunkN t : namespace :=
    nroot .@ "thunk" .@ t.
  Definition thunkPaidN t : namespace :=
    thunkN t .@ "paid".
  Definition thunkAtDepthN t d : namespace :=
    thunkN t .@ "depth" .@ d.

  Notation ThunkToken p t := (na_own p (↑thunkN t)).

  Notation ThunkVal γv v := (own γv (Cinr $ to_agree v)).

  Definition ThunkBaseInv t γv γforced n R φ : iProp Σ := (
    ∃ forced,
        own γforced (● Excl' forced)
      ∗ if forced then
          ∃ v,
              t ↦ EVALUATEDV « v »
            ∗ own γv (Cinr $ to_agree v)
            ∗ □ φ v
        else
          ∃ f,
              t ↦ UNEVALUATEDV « f »
            ∗ own γv (Cinl $ Excl ())
            ∗ (TC n -∗ R -∗ ∀ ψ, (∀ v, R -∗ □ φ v -∗ ψ «v»%V) -∗ WP «f #()» {{ ψ }})
  )%I.
  Definition ThunkCsqInv t γv γforced n φ ψ : iProp Σ := (
    ∃ forced,
        own γforced (● Excl' forced)
      ∗ if forced then
          ∃ v, own γv (Cinr $ to_agree v) ∗ □ ψ v
        else
          ∀ v, TC n -∗ φ v ={⊤}=∗ □ ψ v
  )%I.
  Definition ThunkPaidInv t γforced γpaid : iProp Σ := (
    ∃ forced paid,
        own γforced (◯ Excl' forced)
      ∗ own γpaid (● MaxNat paid)
      ∗ if forced then True else TC paid
  )%I.
  Fixpoint Thunk' p t γv n R φ d : iProp Σ := (
    ∃ γforced γpaid paid m,
        ⌜paid ≤ m ≤ n+paid⌝
      ∗ own γpaid (◯ MaxNat paid)
      ∗ inv (thunkPaidN t) (ThunkPaidInv t γforced γpaid)
      ∗ match d with
        | 0 =>
            na_inv p (thunkAtDepthN t 0) (ThunkBaseInv t γv γforced m R φ)
        | S d' =>
            ∃ φ',
                Thunk' p t γv (n+paid-m) R φ' d'
              ∗ na_inv p (thunkAtDepthN t d) (ThunkCsqInv t γv γforced m φ' φ)
        end
  )%I.
  Definition Thunk p t γv n R φ : iProp Σ := (
    ∃ d, Thunk' p t γv n R φ d
  )%I.

  Lemma ThunkToken_exclusive p t1 t2 :
    ThunkToken p t1 -∗ ThunkToken p t2 -∗ ⌜t1 ≠ t2⌝.
  Proof.
    iIntros "H1 H2" (<-). iDestruct (na_own_disjoint with "H1 H2") as %Hdisj.
    exfalso. apply (nclose_infinite (thunkN t1)).
    rewrite (_ : ↑thunkN t1 = ∅) ; last set_solver. apply empty_finite.
  Qed.

  Lemma ThunkVal_persistent γv v :
    Persistent (ThunkVal γv v).
  Proof. exact _. Qed.

  Lemma ThunkVal_agree γv v1 v2 :
    ThunkVal γv v1 -∗ ThunkVal γv v2 -∗ ⌜v1 = v2⌝.
  Proof.
    iIntros "H1 H2". iDestruct (own_valid_2 with "H1 H2") as %Hag. iPureIntro.
    eapply to_agree_op_valid_L, (proj1 (Cinr_valid (A:=unitR) _)). by rewrite Cinr_op.
  Qed.

  Instance Thunk'_persistent p t γv n R φ d :
    Persistent (Thunk' p t γv n R φ d).
  Proof.
    revert n φ. induction d ; exact _.
  Qed.

  Lemma Thunk_persistent p t γv n R φ :
    Persistent (Thunk p t γv n R φ).
  Proof. exact _. Qed.

  Lemma Thunk_weaken p t γv n₁ n₂ R φ :
    (n₁ ≤ n₂)%nat →
    Thunk p t γv n₁ R φ -∗
    Thunk p t γv n₂ R φ.
  Proof.
    iIntros (I) "H". iDestruct "H" as (d) "H". iExists d.
    iInduction (d) as [|d'] "IH" forall (n₁ n₂ I φ).
    { iDestruct "H" as (γforced γpaid paid m) "(%&H)".
      iExists γforced, γpaid, paid, m. iFrame "H". iPureIntro. lia. }
    { iDestruct "H" as (γforced γpaid paid m) "(%&?&?&H)"; fold Thunk'.
      iDestruct "H" as (φ') "[??]".
      iExists γforced, γpaid, paid, m; fold Thunk'. iFrame. iSplit ; first (iPureIntro;lia).
      iExists φ'. iFrame. iApply ("IH" with "[] [$]"). iPureIntro. lia. }
  Qed.

  Lemma Thunk_consequence p t γv n m R φ ψ :
    (∀ v, TC m -∗ φ v ={⊤}=∗ □ ψ v) -∗
    Thunk p t γv  n    R φ  ={∅}=∗
    Thunk p t γv (n+m) R ψ.
  Proof.
    iIntros "Hφψ Ht".
    iDestruct "Ht" as (d) "Ht".
    iMod (own_alloc (● MaxNat 0 ⋅ ◯MaxNat 0)) as (γpaid) "[Hγpaid● Hγpaid◯]".
    { by apply auth_both_valid_2. }
    iMod (own_alloc (● Excl' false ⋅ ◯ Excl' false)) as (γforced) "[Hγforced● Hγforced◯]".
    { by apply auth_both_valid_2. }
    iExists (S d), γforced, γpaid, 0, m; fold Thunk'. iFrame "Hγpaid◯".
    iSplitR ; last iSplitR "Ht Hγforced● Hφψ".
    { iPureIntro;lia. }
    { iMod zero_TC. iApply inv_alloc. iExists false. iFrame. iExists 0. by iFrame. }
    { iExists φ. rewrite (_ : n+m+0-m = n) ; last lia. iFrame "Ht".
      iApply na_inv_alloc. iExists false. by iFrame. }
  Qed.

  Lemma Thunk_pay_ind_aux E t γforced γpaid paid k m n :
    ↑thunkPaidN t ⊆ E →
        ⌜paid ≤ m ≤ n+paid⌝
      ∗ inv (thunkPaidN t) (ThunkPaidInv t γforced γpaid)
      ∗ own γpaid (◯ MaxNat paid)
      ∗ TC k
    ={E}=∗
      let paying := k `min` (m - paid) in
      let paid2 := paid + paying in
        ⌜paid2 ≤ m ≤ (n-k)+paid2⌝
      ∗ own γpaid (◯ MaxNat paid2)
      ∗ TC (k-paying).
  Proof.
      set paying := k `min` (m - paid).
      iIntros (?) "(% & HpaidInv & Hγpaid◯ & Htc)".
      iSplitR ; first (iPureIntro;lia).
      rewrite [in TC k](_ : k = (k-paying) + paying) ; last lia. iDestruct "Htc" as "[$ Htc]".
      iMod (inv_acc with "HpaidInv") as "[HpaidInv HpaidInvClose]" ; first done.
      iDestruct "HpaidInv" as (forced paid') "(Hγforced◯ & >Hγpaid● & Hpaid)".
      iMod (auth_max_nat_update_incr' _ _ _ paying with "Hγpaid● Hγpaid◯")
        as "[Hγpaid● $]" ; simpl.
      iApply "HpaidInvClose". iExists forced, (paid' + paying). iFrame. destruct forced.
      - done.
      - by iSplitR "Htc".
  Qed.

  Lemma Thunk_pay_ind E p t γv n k R φ d :
    ↑thunkPaidN t ⊆ E →
    TC k -∗ Thunk' p t γv n R φ d ={E}=∗ Thunk' p t γv (n-k) R φ d.
  Proof.
    (* proof by induction on the depth d of the predicate: *)
    iIntros (?) "Htc Ht". iInduction (d) as [|d'] "IH" forall (n k φ).
    (* (1) base case: the “node” at hand actually stores the thunk. *)
    {
      (* store as much credit as possible in the base node: *)
      iDestruct "Ht" as (γforced γpaid paid m) "(? & ? & #? & ?)".
      set paying := k `min` (m - paid).
      iExists γforced, γpaid, (paid + paying), m. iFrame "#∗".
      by iDestruct (Thunk_pay_ind_aux with "[$]") as ">($ & $ & _)".
      (* nothing else to do *)
    }
    (* (2) consequence case: the “node” at hand stores a consequence to apply. *)
    {
      (* store as much credit as possible in the current node: *)
      iDestruct "Ht" as (γforced γpaid paid m) "(? & ? & #? & H)" ; fold Thunk'.
      set paying := k `min` (m - paid).
      iExists γforced, γpaid, (paid + paying), m ; fold Thunk'. iFrame "#".
      iDestruct (Thunk_pay_ind_aux with "[$]") as ">(% & $ & Htc)" ; first done.
      fold paying. iSplitR ; first (iPureIntro;lia).
      (* pay recursively with the remainder, by applying the induction hypothesis: *)
      iDestruct "H" as (φ') "[Ht ?]". iExists φ'. iFrame.
      rewrite (_ : n-k+(paid+paying)-m = (n+paid-m) - (k-paying)) ; last lia.
      by iApply ("IH" with "Htc Ht").
    }
  Qed.

  Lemma Thunk_pay E p t γv n k R φ :
    ↑thunkPaidN t ⊆ E →
    TC k -∗ Thunk p t γv n R φ ={E}=∗ Thunk p t γv (n-k) R φ.
  Proof.
    iIntros (?) "Htc Ht". iDestruct "Ht" as (d) "Ht". iExists d.
    by iApply (Thunk_pay_ind with "Htc Ht").
  Qed.

  Lemma create_spec p n R φ f :
    TC_invariant -∗
    {{{ TC 3 ∗ ( TC n -∗ R -∗ ∀ ψ, (∀ v, R -∗ □ φ v -∗ ψ «v»%V) -∗ WP «f #()» {{ ψ }} ) }}}
    « create f »
    {{{ t γv, RET #t ; Thunk p t γv n R φ }}}.
  Proof.
    iIntros "#HtickInv" (Φ) "!# [? Hf] Post".
    iMod (own_alloc (Cinl $ Excl ())) as (γv) "?" ; first done.
    iMod (own_alloc (● MaxNat 0 ⋅ ◯MaxNat 0)) as (γpaid) "[Hγpaid● Hγpaid◯]".
    { by apply auth_both_valid_2. }
    iMod (own_alloc (● Excl' false ⋅ ◯ Excl' false)) as (γforced) "[Hγforced● Hγforced◯]".
    { by apply auth_both_valid_2. }
    iApply wp_fupd. wp_tick_lam. wp_tick_inj. wp_tick_alloc t. iApply "Post".
    iExists 0, γforced, γpaid, 0, n. iFrame. iSplitR ; first (iPureIntro;lia).
    iSplitL "Hγpaid● Hγforced◯".
    { iMod zero_TC. iApply inv_alloc. iExists false. iFrame. iExists 0. by iFrame. }
    { iApply na_inv_alloc. iExists false. auto with iFrame. }
  Qed.

  Lemma take_paid_from_ThunkPaidInv E t γforced γpaid m :
    ↑thunkPaidN t ⊆ E →
    inv (thunkPaidN t) (ThunkPaidInv t γforced γpaid) -∗
    own γforced (● Excl' false) -∗
    own γpaid (◯ MaxNat m) -∗
    |={E}=>
      own γforced (● Excl' true)
    ∗ TC m.
  Proof.
    iIntros (?) "HpaidInv Hγforced● Hγpaid◯".
    (* get the m accumulated time credits, by opening the “paid” invariant: *)
    iMod (inv_acc with "HpaidInv") as "[HpaidInv HpaidInvClose]" ; first done.
    iDestruct "HpaidInv" as (forced paid) "(>Hγforced◯ & >Hγpaid● & Hpaid)".
    iAssert ⌜forced = false⌝%I as %->.
    { by iDestruct (own_valid_2 with "Hγforced● Hγforced◯")
        as %[[=]%Excl_included ]%auth_both_valid_discrete. }
    iDestruct (own_auth_max_nat_le with "Hγpaid● Hγpaid◯") as %Hle; cbn in Hle.
    iDestruct (TC_weaken _ _ Hle with "Hpaid") as ">Hm".
    (* update the ghost state to b = true, so as to switch both invariants
     * to the other side: *)
    iMod (own_update_2 with "Hγforced● Hγforced◯") as "Hγforced".
    { by apply auth_update, option_local_update, (exclusive_local_update _ (Excl true)). }
    iDestruct "Hγforced" as "[Hγforced● Hγforced◯]".
    (* close the “paid” invariant: *)
    iMod ("HpaidInvClose" with "[Hγforced◯ Hγpaid●]"). { iExists true, paid. by iFrame. }
    by iFrame.
  Qed.

  Lemma force_spec_ind p F t γv R φ d :
    (∀ d', d' ≤ d  →  ↑thunkAtDepthN t d' ⊆ F) →
    TC_invariant -∗
    {{{ TC 11
      ∗ Thunk' p t γv 0 R φ d
      ∗ na_own p F
      ∗ R
    }}}
    « force #t »
    {{{ v, RET «v» ;
        own γv (Cinr $ to_agree v)
      ∗ □ φ v
      ∗ na_own p F
      ∗ R
    }}}.
  Proof.
    iIntros (HF) "#HtickInv".
    iIntros (Φ) "!> (Htc & Ht & Hp & HR) Post".
    (* proof by induction on the depth d of the predicate: *)
    iInduction (d) as [|d' IH] "IH" forall (F HF φ Φ).
    (* (1) base case: the “node” at hand actually stores the thunk. *)
    {
      iDestruct "Ht" as (γforced γpaid paid m) "(% & Hγpaid◯ & HpaidInv & #HtInv)"; fold Thunk'.
      (* open the “base” invariant: *)
      wp_tick_lam.
      iDestruct (na_inv_acc with "HtInv Hp") as ">(Ht & Hp & HtInvClose)" ;
        [done|auto|].
      (* add a fupd so that we can close it at the end: *)
      iApply wp_fupd.
      (* case analysis on whether the thunk has been forced already: *)
      iDestruct "Ht" as ([|]) "[Hγforced● H]".
      (* (1a) if forced = true: *)
      {
        (* get the memoized value and the already computed postcondition: *)
        iDestruct "H" as (v) "(Ht & #Hγv & #Hφ)".
        wp_tick_load. wp_tick_match.
        iApply "Post". iFrame "#∗".
        (* close the “base” invariant: *)
        iApply "HtInvClose". iFrame. iExists true. iFrame. iExists v. by iFrame "#∗".
      }
      (* (1b) if forced = false: *)
      {
        wp_tick.
        (* get the m accumulated time credits, by opening the “paid” invariant: *)
        assert (paid = m) as -> by lia.
        iDestruct (take_paid_from_ThunkPaidInv with "[$][$][$]") as ">[Hγforced● Hm]" ; first done.
        (* perform the forcing, obtain the value and the postcondition: *)
        iDestruct "H" as (f) "(Ht & Hγv & Hf)".
        wp_load. wp_tick_match.
        wp_apply ("Hf" with "Hm HR"). iIntros (v) "HR #Hφ".
        wp_tick_let. wp_tick_inj. wp_tick_store. wp_tick_seq.
        iApply "Post". iFrame "#∗".
        (* update the ghost state to remember that the value has been computed: *)
        iDestruct (own_update _ _ (Cinr $ to_agree v) with "Hγv") as ">#$".
        { by apply cmra_update_exclusive. }
        (* close the “base” invariant: *)
        iApply "HtInvClose". iFrame. iExists true. iFrame. iExists v. by iFrame "#∗".
      }
    }
    (* (2) consequence case: the “node” at hand stores a consequence to apply. *)
    {
      iDestruct "Ht" as (γforced γpaid paid m) "(% & Hγpaid◯ & HpaidInv & H)"; fold Thunk'.
      iDestruct "H" as (φ') "[Ht HcsqInv]".
      rewrite (_ : 0+paid-m = 0) ; last lia.
      set d := S d' in HF |- *.
      (* open the “consequence” invariant: *)
      rewrite (_ : F = ↑thunkAtDepthN t d ∪ (F ∖ ↑thunkAtDepthN t d)) ;
        first setoid_rewrite na_own_union ;
        [ | set_solver | set_solver | apply union_difference_L ; by auto ].
      iDestruct "Hp" as "[Hpd Hp]".
      iDestruct (na_inv_acc with "HcsqInv Hpd") as ">(HcsqInv & Hp' & HcsqInvClose)" ;
        [done|done|].
      (* add a fupd so that we can close it at the end: *)
      iApply wp_fupd.
      (* apply the induction hypothesis, get the value and the postcondition: *)
      iApply ("IH" with "[] Htc Ht Hp HR") ; iClear "HtickInv IH".
      { iPureIntro ; intros d1 ?.
        assert (d1 ≤ d  ∧  d1 ≠ d) as [??] by lia. solve_ndisj. }
      iIntros (v) "!>(#Hγv & Hφ' & Hp & HR)". iApply "Post". iFrame "#∗".
      (* case analysis on whether this node has been forced already: *)
      iDestruct "HcsqInv" as ([|]) "[Hγforced● Hcsq]".
      (* (2a) if forced = true: *)
      {
        (* get the result of the already computed consequence: *)
        iDestruct "Hcsq" as (v') "[Hγv' #Hφ]".
        iDestruct (ThunkVal_agree with "Hγv Hγv'") as %<-.
        iFrame "#".
        (* close the “consequence” invariant: *)
        iApply "HcsqInvClose". iFrame. iExists true. iFrame. iExists v. by iFrame "#".
      }
      (* (2b) if forced = false: *)
      {
        (* get the m accumulated time credits, by opening the “pay” invariant: *)
        assert (paid = m) as -> by lia.
        iDestruct (take_paid_from_ThunkPaidInv with "[$][$][$]") as ">[Hγforced● Hm]" ; first done.
        (* compute the consequence: *)
        iDestruct ("Hcsq" $! v with "Hm Hφ'") as ">#$".
        (* close the “consequence” invariant: *)
        iApply "HcsqInvClose". iFrame. iExists true. iFrame. iExists v. by iFrame "#".
      }
    }
  Qed.

  Lemma force_spec p t γv R φ :
    TC_invariant -∗
    {{{ TC 11 ∗ Thunk p t γv 0 R φ ∗ ThunkToken p t ∗ R }}}
    « force #t »
    {{{ v, RET «v» ; ThunkVal γv v ∗ □ φ v ∗ ThunkToken p t ∗ R }}}.
  Proof.
    iIntros "#HtickInv" (Φ) "!>(Htc & Ht & Hp & HR) Post".
    iDestruct "Ht" as (d) "Ht".
    wp_apply (force_spec_ind with "HtickInv [-Post] Post") ; first solve_ndisj.
    by iFrame.
  Qed.

  (* The following is provable. It amounts to forcing logically the thunk,
     knowing that the base node has already been forced and has value v.
     However the proof would largely replicate that of force_spec, and this
     reasoning rule does not seem useful in practice. *)
  Lemma ThunkVal_force p t γv R φ v :
    Thunk p t γv 0 R φ -∗
    ThunkVal γv v -∗
    ThunkToken p t -∗
    |={⊤}=>
      ▷ □ φ v ∗ ThunkToken p t.
  Abort.

  (* Example: forwarding of debt for a thunk that creates a thunk: *)
  Goal ∀ p t1 γv1 n1 n2 m R φ,
    Thunk p t1 γv1 n1 R (λ v2, ∃ t2 γv2, ⌜v2 = #t2⌝ ∗
      Thunk p t2 γv2 n2 R φ
    )
    ={∅}=∗
    Thunk p t1 γv1 (n1+m) R (λ v2, ∃ t2 γv2, ⌜v2 = #t2⌝ ∗
      Thunk p t2 γv2 (n2-m) R φ
    ).
  Proof.
    iIntros. iApply Thunk_consequence=>//.
    iIntros (v2) "Htc Ht2" ; iDestruct "Ht2" as (t2 γv2) "[#? Ht2]".
    iExists t2, γv2. iFrame "#". by iMod (Thunk_pay with "Htc Ht2") as "#$".
  Qed.

  (* Example: creating a thunk that forces a thunk: *)
  Goal ∀ p t2 γv2 n2 R φ,
    TC_invariant -∗
    {{{ TC 3 ∗ Thunk p t2 γv2 n2 R φ }}}
    « create (λ: <>, force #t2)%V »
    {{{ t1 γv1, RET #t1 ;
      Thunk p t1 γv1 (12+n2) (ThunkToken p t2 ∗ R) (λ v,
          (*ThunkVal γv1 v (* note: we cannot speak about t1 here, because it is not known before create *)
        ∗*) ThunkVal γv2 v
        ∗ □ φ v
      )
    }}}.
  Proof.
    intros ; iIntros "#HtickInv" (?) "!> [Htc Ht2] Post".
    wp_apply (create_spec with "HtickInv [$Htc Ht2] Post").
    iIntros "[Htc1 Htc2] [Htok2 HR]" (Ψ) "Post".
    iMod (Thunk_pay with "Htc2 Ht2") as "Ht2" ; first done. rewrite Nat.sub_diag.
    wp_tick_lam. wp_apply (force_spec with "HtickInv [$]").
    iIntros (v) "(#Htv2 & #Hφ & Htok2 & HR)". by iApply ("Post" with "[$] [$]").
  Qed.

End ThunkProofs.

author: Ricagraca

repo: i-splay-tree

save_path: github-repos/coq/Ricagraca-i-splay-tree


text:
Require Export Arith.
Require Export Peano_dec.
Require Import util.
Require Import EqdepFacts.
Require Import stability.
Require Import tactics.

Set Implicit Arguments.

Local Open Scope nat_scope.

Scheme le_ind_dep := Induction for le Sort Prop.

Lemma le_unique : forall n m (h1 h2 : n <= m), h1 = h2.
Proof.
intro n.
assert (forall m : nat, forall h1 : n <= m, forall p : nat, forall h2 : le n p,
  m=p -> eq_dep nat (le n) m h1 p h2).
 intros m h1; elim h1 using le_ind_dep.
  intros p h2; case h2; intros.
   auto.
   subst n. absurd (S m0 <= m0); auto with arith.
 intros m0 l Hrec p h2.
  case h2; intros.
   subst n; absurd (S m0 <= m0); auto with arith.
   assert (m0=m1); auto ; subst m0.
   replace l0 with l; auto.
set (w := eq_dep_eq).

   apply (@eq_dep_eq _ eq_nat_dec (le n) m1); auto.
 intros; apply (@eq_dep_eq _ eq_nat_dec (le n) m); auto.
Qed.

Lemma lt_unique : forall n m (h1 h2 : lt n m), h1 = h2.

Proof.
intros n m. unfold lt. intros. apply le_unique.
Qed.

(** Bounded natural numbers *)
(*
Section dom_lt.

  Variable n : nat.

  Local Open Scope nat_scope.

   (* A number smaller than n *)
  Definition dom_lt := { i : nat | i < n }.
  Definition dom_build i (ip : i < n) : dom_lt :=
    @exist _ _ i ip.
  Definition dom_lt_val (ip : dom_lt) : nat :=
    proj1_sig ip.
  Definition dom_lt_proof (ip : dom_lt) : dom_lt_val ip < n :=
    proj2_sig ip.

End dom_lt.
*)

(** Vcheck *)

Section Check_n.

  Variables
    (n : nat)
    (P Q : forall i, i < n -> Prop).

  Obligation Tactic := crunch.

  Program Fixpoint check_n_aux (p : nat) (H : p < n) : Prop :=
    let this := @P p H in
    let rest :=
      match p with
      | 0 => True
      | S p' => @check_n_aux p' _
      end
    in
    this /\ rest.

  Program Definition check_n :=
    match n with
    | 0 => True
    | _ => @check_n_aux (pred n) _
    end.

  Variable P_holds : forall i (ip: i < n), P ip.

  Lemma check_n_holds_aux :
    forall i (ip : i < n), check_n_aux ip.
  Proof.
    induction i; crunch.
  Qed.

  Variable P_stable : forall i (ip: i < n), Stable (P ip).

  Lemma check_n_Stable_aux :
    forall i (ip : i < n), Stable (check_n_aux ip).
  Proof.
    induction i; crunch.
  Qed.

End Check_n.

Lemma check_n_holds n (P : forall i, i < n -> Prop) :
  (forall i (ip: i < n), P i ip) -> check_n P.
Proof.
  destruct n; crunch.
  apply check_n_holds_aux; crunch.
Qed.

Lemma check_n_Stable n (P : forall i, i < n -> Prop) :
  (forall i (ip: i < n), Stable (P i ip)) -> Stable (check_n P).
Proof.
  destruct n; crunch.
  apply check_n_Stable_aux; crunch.
Qed.

Section Check_n_equiv.

  Variables
    (n : nat)
    (P Q : forall i, i < n -> Prop)
    (P_eq_Q : forall i (ip : i < n), P ip <-> Q ip).

  Lemma check_n_equiv_aux :
    forall i (ip : i < n),
      check_n_aux P ip <-> check_n_aux Q ip.
  Proof.
     (* FIXME, there must be a better way to state this proof, without
        those asserts (which essentially break iff into two implications *)
    pose (fun i (ip : i < n) => proj1 (P_eq_Q ip)).
    pose (fun i (ip : i < n) => proj2 (P_eq_Q ip)).
    induction i.
    crunch.
    pose (fun ip : i < n => proj1 (IHi ip)).
    pose (fun ip : i < n => proj2 (IHi ip)).
    crunch.
  Qed.

End Check_n_equiv.

Lemma check_n_equiv n
  (P Q : forall i, i < n -> Prop)
  (P_eq_Q : forall i (ip : i < n), P i ip <-> Q i ip) :
  check_n P <-> check_n Q.
Proof.
  destruct n; intros.
  crunch.
  unfold check_n.
  match goal with
    | |- check_n_aux _ ?ip <-> check_n_aux _ ?jp =>
      rewrite (lt_unique ip jp)
  end.
  apply check_n_equiv_aux. trivial.
Qed.

author: Eelis

repo: hybrid

save_path: github-repos/coq/Eelis-hybrid


text:
Require Import List.
Require Import Arith.
Require Import Logic.
Require Import Nat.
Import ListNotations.

Lemma cons_app:
  forall {X} (x : X) (A : list X),
  x :: A = [x] ++ A.
Proof. reflexivity. Qed.

(* ====================================== *)
(* 9.1 Terms, Substitutions, and Unifiers *)
(* ====================================== *)

Definition var := nat.

Inductive ter : Type :=
  | V : var -> ter
  | T : ter -> ter -> ter.

Definition eqn := prod ter ter.

Implicit Types x y z : var.
Implicit Types s t u v : ter.
Implicit Type e : eqn.
Implicit Types A B C : list eqn.
Implicit Types sigma tau : ter -> ter.
Implicit Types m n k : nat.

Definition subst sigma : Prop :=
  forall s t, sigma (T s t) = T (sigma s) (sigma t).

Definition unif sigma A : Prop :=
  subst sigma /\ forall s t, In (s,t) A -> sigma s = sigma t.

Definition unifiable A : Prop :=
  exists sigma, unif sigma A.

Definition principal_unifier sigma A : Prop :=
  unif sigma A /\ forall tau, unif tau A -> forall s, tau (sigma s) = tau s.

(* Exercise 9.1.1 Show that two substitutions agree on all
   terms if they agree on all variables. *)

Theorem sub_agree:
  forall sigma tau, subst sigma /\ subst tau ->
  (forall x, sigma (V x) = tau (V x)) ->
  forall t, sigma t = tau t.
Proof.
  intros sigma tau [Hsig Htau] Hvar t.
  induction t.
  - apply Hvar.
  - unfold subst in *. rewrite Hsig, Htau, IHt1, IHt2. reflexivity.
Qed.

(* Exercise 9.1.2 A function f : X → X is idempotent if f (fx) = fx for every x
  in X. Show that every principal unifier is idempotent. *)

Theorem principal_unif_idempotent:
  forall sigma A, principal_unifier sigma A -> forall t, sigma (sigma t) = sigma t.
(*   forall sigma A, principal_unifier sigma A -> forall e, In e A -> sigma (sigma e) = sigma A. *)
Proof.
  intros. unfold principal_unifier in H. destruct H. apply H0. apply H.
Qed.

(* Exercise 9.1.3 Prove the following facts about unification:
    a) unif σ (y ≐ s :: A) ↔ σs = σt ∧ unif σ A      TYPO???
    b) unif σ (A++B) ↔ unif σ A ∧ unif σ B *)

Theorem unif_cons:
  forall sigma s t A,
  unif sigma ((s,t)::A) <-> sigma s = sigma t /\ unif sigma A.
Proof.
  unfold unif. intros. split.
  - intros []. split.
    + apply H0. simpl. left. reflexivity.
    + split.
      * apply H.
      * intros s0 t0 H1. apply H0. simpl. right. apply H1.
  - intros [H [H0 H1]]. split.
    + apply H0.
    + intros s0 t0 H2. simpl in H2. destruct H2.
      * inversion H2. rewrite H4, H5 in H. apply H.
      * apply H1. apply H2.
Qed.

Theorem unif_app:
  forall sigma A B,
  unif sigma (A++B) <-> unif sigma A /\ unif sigma B.
Proof.
  unfold unif. intros. split.
  - intros []. split; split.
    + apply H.
    + intros s t H1. apply H0. apply in_or_app. left. apply H1.
    + apply H.
    + intros s t H1. apply H0. apply in_or_app. right. apply H1.
  - intros [[] []]. split.
    + apply H.
    + intros s t H3. apply in_app_or in H3. destruct H3.
      * apply H0. apply H3.
      * apply H2. apply H3.
Qed.

Lemma unif_nil:
  forall sigma, subst sigma -> unif sigma [].
Proof.
  intros sigma. unfold unif. split.
  - apply H.
  - intros. inversion H0.
Qed.

(* Exercise 9.1.4 Prove that an equation list is
   non-unifiable if some sublist is nonunifiable. *)
Theorem non_unif_sublist:
  forall A B,
  incl A B ->
  ~ unifiable A ->
  ~ unifiable B.
Proof.
  unfold unifiable, not, incl, unif. intros. apply H0.
  destruct H1 as [sigma]. exists sigma. split.
  - apply H1.
  - destruct H1. intros s t H3. apply H2. apply H. apply H3.
Qed.

Lemma in_incl:
  forall {X} (x:X) (A:list X),
  In x A -> incl [x] A.
Proof.
  intros X x A H. unfold incl. intros a [].
  - rewrite <- H0. apply H.
  - contradiction.
Qed.

Theorem non_unif_element:
  forall A e,
  In e A ->
  ~ unifiable [e] ->
  ~ unifiable A.
Proof.
  intros A e H H0. apply non_unif_sublist with (A:=[e]) (B:=A).
  - apply in_incl. apply H.
  - apply H0.
Qed.

(* ========================= *)
(* 9.2 Solved Equation Lists *)
(* ========================= *)

Fixpoint vars_term t : list var :=
  match t with
  | V x => [x]
  | T s t => (vars_term s) ++ (vars_term t)
  end.

Fixpoint vars_list A : list var :=
  match A with
  | nil => []
  | e::A' => (vars_term (fst e)) ++ (vars_term (snd e)) ++ (vars_list A')
  end.

Fixpoint domain A : list var :=
  match A with
  | [] => []
  | (V x,_)::A' => x :: (domain A')
  | _::A' => domain A'  (* TYPO??? *)
  end.

Definition disjoint {X} (A B : list X) : Prop :=
  ~ (exists x:X, In x A /\ In x B).

Inductive solved : list eqn -> Prop :=
  | solved_nil : solved nil
  | solved_cons : forall x s A, ~ In x (vars_term s) -> ~ In x (domain A) ->
                  disjoint (vars_term s) (domain A) -> solved A -> solved ((V x,s)::A).

Fixpoint replace_term s x t : ter :=
  match s with
  | V y => if (beq_nat x y) then t else V y
  | T u v => T (replace_term u x t) (replace_term v x t)
  end.

Fixpoint replace_list A x t : list eqn :=
  match A with
  | [] => []
  | e::A' => ((replace_term (fst e) x t),(replace_term (snd e) x t))::(replace_list A' x t)
  end.

Fixpoint phi A s : ter :=
  match A with
  | [] => s
  | (V x, t)::A' => replace_term (phi A' s) x t
  | (u, v)::A' => s
  end.

Lemma domain_vars:
  forall x A,
  In x (domain A) ->
  In x (vars_list A).
Proof.
  intros x A H. induction A.
  - contradiction.
  - destruct a, t.
    + simpl in *. destruct H.
      * left. apply H.
      * right. apply in_or_app. right. apply IHA. apply H.
    + simpl in *. apply in_or_app. right. apply in_or_app.
      right. apply IHA. apply H.
Qed.

(* Exercise 9.2.3 Prove the following facts about variable replacement. *)
(* 9.2.3a) If x ∉ Vs, then sxt = s. *)
Fact vars_term_no_replace:
  forall x s t,
  ~ In x (vars_term s) ->
  (replace_term s x t) = s.
Proof.
  unfold not. intros x s t H. induction s.
  - simpl. simpl in H. destruct (beq_nat x v) eqn:H0.
    + apply beq_nat_true in H0. exfalso. apply H. left. symmetry. apply H0.
    + reflexivity.
  - simpl. simpl in H. apply f_equal2.
    + apply IHs1. intros H0. apply H. apply in_or_app. left. apply H0.
    + apply IHs2. intros H0. apply H. apply in_or_app. right. apply H0.
Qed.

(* 9.2.3b) If x ∉ VA, then Axt= A. *)
Fact vars_list_no_replace:
  forall x A t,
  ~ In x (vars_list A) ->
  (replace_list A x t) = A.
Proof.
  unfold not. intros x A t H. induction A.
  - reflexivity.
  - simpl. apply f_equal2.
    + destruct a. simpl. apply f_equal2.
      * apply vars_term_no_replace. simpl in H. intros H0.
        apply H. apply in_or_app. left. apply H0.
      * apply vars_term_no_replace. simpl in H. intros H0.
        apply H. apply in_or_app. right. apply in_or_app. left. apply H0.
    + apply IHA. intros H0. apply H. simpl. apply in_or_app. right.
      apply in_or_app. right. apply H0.
Qed.

(* 9.2.3c) If x ∉ DA, then D(Axt) = DA. *)
Fact term_list_domain:
  forall x A t,
  ~ In x (domain A) ->
  (domain (replace_list A x t)) = (domain A).
Proof.
  unfold not. intros x A t H. induction A.
  - reflexivity.
  - destruct a. destruct t0.
    + destruct (beq_nat x v) eqn:H0.
      * exfalso. apply H. simpl. left. apply beq_nat_true_iff in H0. rewrite H0. reflexivity.
      * simpl. rewrite H0. apply f_equal2.
        { reflexivity. }
        { apply IHA. intros H1. apply H. simpl. right. apply H1. }
    + simpl. apply IHA. intros H0. apply H. simpl. apply H0.
Qed.

(* 9.2.3d) If σ is a substitution such that σx = σt, then σ(sxt) = σs. *)
Fact subst_replace:
  forall sigma s x t,
  subst sigma ->
  sigma (V x) = sigma t ->
  sigma (replace_term s x t) = sigma s.
Proof.
  intros sigma s x t H H0. induction s.
  - simpl. destruct (beq_nat x v) eqn:H1.
    + rewrite <- H0. apply beq_nat_true_iff in H1. rewrite H1. reflexivity.
    + reflexivity.
  - simpl. unfold subst in H. rewrite H. rewrite H. apply f_equal2.
    + apply IHs1.
    + apply IHs2.
Qed.

(* 9.2.3e) λs. sxt is a substitution. *)
Fact replace_subst:
  forall x t,
  subst (fun s => replace_term s x t).
Proof.
  intros x t. unfold subst. intros s0 t0. simpl. reflexivity.
Qed.

(* Exercise 9.2.4 Prove the following facts about ϕ: *)
(* 9.2.4a) ϕA is a substitution. *)
Fact phi_subst:
  forall A,
  subst (phi A).
Proof.
  intros A. unfold subst. intros s t. induction A.
  - simpl. reflexivity.
  - destruct a as [s0 t0]. destruct s0.
    + simpl. rewrite IHA. simpl. reflexivity.
    + simpl. reflexivity.
Qed.

(* 9.2.4b) If DA k Vs, then ϕAs = s. *)
Fact disjoint_phi:
  forall A s,
  disjoint (domain A) (vars_term s) ->
  phi A s = s.
Proof.
  unfold disjoint, not. intros A s H. induction A.
  - simpl. reflexivity.
  - destruct a as [s0 t0]. destruct s0.
    + simpl. replace (phi A s) with s.
      * apply vars_term_no_replace. intro. apply H. exists v. split.
        { simpl. left. reflexivity. }
        { apply H0. }
      * symmetry. apply IHA. intros []. apply H. exists x. split.
        { simpl. destruct H0. right. apply H0. }
        { destruct H0. apply H1. }
    + simpl. reflexivity.
Qed.

(* 9.2.4c) If A is solved, then ϕA is a unifier of A. *)
Fact solved_phi_unif:
  forall A,
  solved A -> unif (phi A) A.
Proof.
  intros A H. unfold unif. split.
  - apply phi_subst.
  - intros s t H0. induction A.
    + contradiction.
    + destruct a as [s0 t0]. destruct s0.
      * Search phi. simpl.
Admitted.

 (* induction A.
    + contradiction.
    + destruct a as [s0 t0], s0 eqn:Hs0.
      * simpl. rewrite vars_term_no_replace. rewrite vars_term_no_replace.
        -- apply IHA.
           ++ inversion H. apply H7.
           ++ simpl in H0. destruct H0.
              ** admit.
              ** apply H0.
        -- intro. inversion H. simpl in H0. destruct H0.
           ++ apply H5. inversion H0. replace (phi A t) with t in H1.
              ** apply H1.
              ** symmetry. apply disjoint_phi. unfold disjoint in *. intro. unfold not in *.
                 destruct H9 as [x0 []]. apply H7. exists x0. split.
                 --- rewrite H11. apply H12.
                 --- apply H9.
           ++ unfold disjoint in *. unfold not in *. apply H5. admit.
        -- intro. inversion H. simpl in H0. destruct H0.
           ++ apply H5. inversion H0. replace (phi A s) with t in H1.
              ** apply H1.
              ** symmetry. Admitted. *)
(*

 rewrite disjoint_phi with (s:=t).
        { simpl. rewrite IHA.
          { rewrite vars_term_no_replace with (s:=(phi A t)).
            { intro. simpl in *. destruct H0.
          { inversion H. apply H5. inversion H0. apply H1. }
          { inversion H. admit. } }
        { inversion H. apply H7. }
        { simpl in H0. destruct H0.
          { inversion H. admit. }
          { apply H0. } } }
      { simpl. simpl in *.
    + unfold disjoint, not. intros [x []]. induction H.
      * contradiction.
      * simpl in H1, H0. destruct H1, H0.
        { unfold disjoint in H4. unfold not in H4. apply H4. exists x0. split.
          { Admitted.  *)

(* apply H.

      destruct H.
      * contradiction.
      *

    + unfold disjoint. unfold not. intros [x []]. induction H.
      * contradiction.
      * unfold not in *. inversion H5. apply

apply IHsolved.
        { simpl in H1. simpl in H0. destruct H0.
          { rewrite <- H0.
        unfold disjoint. intros [x0 []]. unfold not in *. apply H1.
        simpl in H4. destruct H4.
        {
 *)
(* 9.2.4d) If σ is a unifier of A, then σ (ϕAs) = σs. *)
Fact sigma_phi:
  forall sigma A s,
  unif sigma A -> sigma (phi A s) = sigma s.
Proof.
  intros sigma A s H. Admitted.

(* 9.2.4e) If A is solved, then ϕA is a principal unifier of A. *)
Fact phi_principal:
  forall A,
  solved A -> principal_unifier (phi A) A.
Proof.
  intros A H. Admitted.

(* Exercise 9.2.5 Prove the bad equation lemma 9.2.2. Hint: Define a function
   size : ter → N such that size s < size (s · t) and proceed by proving the following
   facts:
   a) If x ∈ Vs and σ is a substitution, then size (σx) ≤ size (σs).
   b) No bad equation is unifiable. *)
Fixpoint size t : nat :=
  match t with
  | V _ => 1
  | T u v => (size u) + (size v)
  end.

Lemma size_sigma:
  forall x s sigma,
  In x (vars_term (V x)) ->
  subst sigma ->
  size (sigma (V x)) <= size (sigma s).
Proof.
  intros x s sigma H H0. Admitted.

Definition bad_eq e : Prop :=
  exists x s, e = (V x,s) /\ (V x) <> s /\ In x (vars_term s).

Fact bad_ununifiable:
  forall e,
  bad_eq e ->
  ~ unifiable [e].
Proof.
  unfold bad_eq, unifiable. intros e H H0. Admitted.

(* Exercise 9.2.6 Prove the following facts about variables: *)
(* 9.2.6a) DA ⊆ A *)
Fact domain_subset:
  forall A,
  incl (domain A) (vars_list A).
Proof.
  intros A. unfold incl. intros a H. induction A.
  - contradiction.
  - destruct a0 as [s t], s.
    + simpl in *. destruct H.
      * left. apply H.
      * right. apply in_or_app. right. apply IHA. apply H.
    + simpl in *. apply in_or_app. right. apply in_or_app.
      right. apply IHA. apply H.
Qed.

(* 9.2.6b) V(A++B) = VA++VB *)
Fact vars_app:
  forall A B,
  vars_list (A++B) = vars_list A ++ vars_list B.
Proof.
  intros A B. induction A, B.
  - reflexivity.
  - reflexivity.
  - rewrite app_nil_r. simpl. rewrite app_nil_r. reflexivity.
  - simpl. rewrite IHA. simpl. rewrite <- app_assoc. rewrite <- app_assoc. reflexivity.
Qed.

(* 9.2.6c) s ≐ t ∈ A → Vs ⊆ VA ∧Vt ⊆ VA *)
Fact vars_subset:
  forall s t A,
  In (s,t) A ->
  incl (vars_term s) (vars_list A) /\ incl (vars_term t) (vars_list A).
Proof.
  unfold incl. intros s t A H. split.
  - intros a H0. induction A.
    + contradiction.
    + simpl in *. destruct H.
      * rewrite H. simpl. apply in_or_app. left. apply H0.
      * apply in_or_app. right. apply in_or_app. right. apply IHA. apply H.
  - intros a H0. induction A.
    + contradiction.
    + simpl in *. destruct H.
      * rewrite H. simpl. apply in_or_app. right. apply in_or_app. left. apply H0.
      * apply in_or_app. right. apply in_or_app. right. apply IHA. apply H.
Qed.

(* 9.2.6d) A ⊆ B → VA ⊆ VB *)
Lemma incl_cons_iff:
  forall (A : Type) (a : A) (l m : list A),
  (In a m /\ incl l m) <-> incl (a :: l) m.
Proof.
  intros A a l m. split.
  - intros []. apply incl_cons.
    + apply H.
    + apply H0.
  - intros H. split.
    + unfold incl in H. apply H. simpl. left. reflexivity.
    + unfold incl in *. intros a0 H0. apply H. simpl. right. apply H0.
Qed.

Lemma in_nil_try2:
  forall {X} (x : X),
  In x [] -> False.
Proof.
  intros. inversion H.
Qed.

Fact subset_vars:
  forall A B,
  incl A B ->
  incl (vars_list A) (vars_list B).
Proof.
  intros A B H a H0. generalize dependent a. induction B.
  - admit.
  - intros a0 H0. simpl. apply in_app_iff. right. apply in_app_iff. right. apply IHB. Admitted.

(* Exercise 9.2.7 Write a function gen : N → ter for which you can prove that genm
   and gen n are non-unifiable if m and n are different. *)
Definition gen x : ter :=
  V x.

Lemma gen_different:
  forall n m, n <> m <-> gen n <> gen m.
Proof.
  unfold not. split.
  - intros H H0. apply H. inversion H0. reflexivity.
  - intros H H0. apply H. rewrite H0. reflexivity.
Qed.

Lemma gen_same:
  forall n m, gen n = gen m <-> n = m.
Proof.
  intros n m. split.
  - intros H. inversion H. reflexivity.
  - intros H. rewrite H. reflexivity.
Qed.

Lemma gen_nonunifiable:
  forall n m, n <> m -> ~ unifiable [(gen n, gen m)].
Proof.
  unfold not, unifiable. intros n m H H0. destruct H0 as [sigma].
  apply unif_cons in H0. destruct H0. unfold unif in H1. destruct H1. Admitted.

(* Exercise 9.2.8 Prove that the concatenation A++B of two solved lists A and B is
   solved if VA and DB are disjoint. *)
Lemma app_solved:
  forall A B,
  solved A ->
  solved B ->
  disjoint (vars_list A) (vars_list B) ->
  solved (A ++ B).
Proof.
  intros A B H H0 H1. induction H.
  - simpl. apply H0.
  - simpl. induction H0.
    + apply solved_cons.
      * apply H.
      * rewrite app_nil_r. apply H2.
      * rewrite app_nil_r. apply H3.
      * rewrite app_nil_r. apply H4.
    + apply solved_cons.
      * apply H.
      * Admitted.

(* ===================== *)
(* 9.3 Unification Rules *)
(* ===================== *)

Definition unif_equiv A B : Prop :=
  forall sigma, unif sigma A <-> unif sigma B.

Definition refinement A B : Prop :=
  incl (vars_list B) (vars_list A) /\ unif_equiv A B.

(* Lemma 9.3.1 Refinement of equation lists is a preorder compatible with cons,
   concatenation, and unification. *)
(* 9.3.3a. A ⊲ A. *)
Lemma unif_equiv_refl:
  forall A, unif_equiv A A.
Proof.
  intros A. unfold unif_equiv. intros sigma. split; intros HA; apply HA.
Qed.

Lemma refinement_refl:
  forall A, refinement A A.
Proof.
  intros A. unfold refinement. split.
  - apply incl_refl.
  - apply unif_equiv_refl.
Qed.

(* 9.3.3b. If A ⊲ B and B ⊲ C, then A ⊲ C. *)
Lemma unif_equiv_trans:
  forall A B C,
  unif_equiv A B ->
  unif_equiv B C ->
  unif_equiv A C.
Proof.
  intros A B C. unfold unif_equiv. intros H H0 sigma. split.
  - intros HA. apply H0. apply H. apply HA.
  - intros HC. apply H. apply H0. apply HC.
Qed.

Lemma refinement_trans:
  forall A B C,
  refinement A B ->
  refinement B C ->
  refinement A C.
Proof.
  unfold refinement. intros A B C [] []. split.
  - apply incl_tran with (vars_list B).
    + apply H1.
    + apply H.
  - apply unif_equiv_trans with B.
    + apply H0.
    + apply H2.
Qed.

(* 9.3.3c. If A ⊲ A′, then x :: A ⊲ x :: A′. *)
Lemma unif_equiv_cons:
  forall e A A',
  unif_equiv A A' ->
  unif_equiv (e :: A) (e :: A').
Proof.
  intros e A A' H. unfold unif_equiv in *. intros sigma. split.
  - intros H1. destruct e. apply unif_cons. apply unif_cons in H1 as []. split.
    + apply H0.
    + apply H. apply H1.
  - intros H1. destruct e. apply unif_cons. apply unif_cons in H1 as []. split.
    + apply H0.
    + apply H. apply H1.
Qed.

Lemma refinement_cons:
  forall e A A',
  refinement A A' ->
  refinement (e :: A) (e :: A').
Proof.
  unfold refinement. intros e A A' []. split.
  - simpl. apply incl_app.
    + unfold incl. intros a H1. apply in_or_app. left. apply H1.
    + apply incl_app.
      * unfold incl. intros a H1. apply in_or_app. right. apply in_or_app. left. apply H1.
      * unfold incl. intros a H1. apply in_or_app. right. apply in_or_app. right.
        unfold incl in H. apply H. apply H1.
  - apply unif_equiv_cons. apply H0.
Qed.

(* 9.3.3d. If A ⊲ A′ and B ⊲ B′, then A++B ⊲ A′ ++B′. *)
Lemma unif_equiv_app:
  forall A A' B B',
  unif_equiv A A' ->
  unif_equiv B B' ->
  unif_equiv (A++B) (A'++B').
Proof.
  unfold unif_equiv. intros A A' B B' H H0. split; intros H1; apply unif_app;
  apply unif_app in H1 as []; split.
    + apply H. apply H1.
    + apply H0. apply H2.
    + apply H. apply H1.
    + apply H0. apply H2.
Qed.

Lemma refinement_app:
  forall A A' B B',
  refinement A A' ->
  refinement B B' ->
  refinement (A++B) (A'++B').
Proof.
  unfold refinement. intros A A' B B' [] []. split.
  - rewrite vars_app. rewrite vars_app. apply incl_app.
    + apply incl_appl. apply H.
    + apply incl_appr. apply H1.
  - apply unif_equiv_app.
    + apply H0.
    + apply H2.
Qed.

(* 9.3.3e. If A ⊲ B, then unif σ A ↔ unif σ B. *)
Lemma refinement_sigma:
  forall A B sigma,
  refinement A B ->
  unif sigma A <-> unif sigma B.
Proof.
  unfold refinement. intros A B sigma []. unfold unif_equiv in H0. split; intros H1.
  - apply H0. apply H1.
  - apply H0. apply H1.
Qed.

(* Lemma 9.3.2 (Unification Rules) *)
(* 9.3.4a. Deletion [s ≐ s] ⊲ nil. *)
Fact deletion_unif_rule:
  forall s,
  refinement [(s,s)] nil.
Proof.
  intros s. unfold refinement. split.
  - simpl. unfold incl. intros a H. contradiction.
  - unfold unif_equiv, unif. intros sigma. split.
    + intros []. split.
      * apply H.
      * intros s0 t0 H1. contradiction.
    + intros []. split.
      * apply H.
      * intros s0 t0 H1. simpl in H1. destruct H1.
        { inversion H1. reflexivity. }
        { inversion H1. }
Qed.

(* 9.3.4b. Swap [s ≐ t] ⊲ [t ≐ s]. *)
Fact swap_unif_rule:
  forall s t,
  refinement [(s,t)] [(t,s)].
Proof.
  intros s t. unfold refinement. split.
  - simpl. rewrite app_nil_r. rewrite app_nil_r. apply incl_app.
    + apply incl_appr. apply incl_refl.
    + apply incl_appl. apply incl_refl.
  - unfold unif_equiv. intros sigma. split.
    + intros H. apply unif_cons. apply unif_cons in H as []. split.
      * symmetry. apply H.
      * apply H0.
    + intros H. apply unif_cons. apply unif_cons in H as []. split.
      * symmetry. apply H.
      * apply H0.
Qed.

(* 9.3.4c. Decomposition [s1 · s2 ≐ t1 · t2] ⊲ [s1 ≐ t1; s2 ≐ t2]. *)
Fact decomposition_unif_rule:
  forall s1 s2 t1 t2,
  refinement [(T s1 s2, T t1 t2)] [(s1, t1);(s2, t2)].
Proof.
  intros s1 s2 t1 t2. unfold refinement. split.
  - simpl. repeat rewrite app_nil_r. repeat apply incl_app.
    + apply incl_appl. apply incl_appl. apply incl_refl.
    + apply incl_appr. apply incl_appl. apply incl_refl.
    + apply incl_appl. apply incl_appr. apply incl_refl.
    + apply incl_appr. apply incl_appr. apply incl_refl.
  - unfold unif_equiv. intros sigma. split.
    + intros H. apply unif_cons in H as H0. destruct H0. inversion H1. unfold subst in H2.
      repeat rewrite H2 in H0. repeat (apply unif_cons; split).
      * inversion H0. reflexivity.
      * inversion H0. reflexivity.
      * apply H1.
    + intros H. apply unif_cons. inversion H. unfold subst in H0. split.
      * repeat rewrite H0. f_equal.
        { apply H1. simpl. left. reflexivity. }
        { apply H1. simpl. right. left. reflexivity. }
      * apply unif_nil. unfold subst. apply H0.
Qed.

(* 9.3.5. Replacement x ≐ t :: A ⊲ x ≐ t :: Axt
   Proceed by proving the following facts in the order stated. *)
(* 9.3.5a. If σ is a substitution such that σx = σt, then σ(sxt) = σs. *)
Lemma replace_term_eq:
  forall sigma s x t,
  subst sigma ->
  sigma (V x) = sigma t ->
  sigma (replace_term s x t) = sigma s.
Proof.
  apply subst_replace.
Qed.

(* 9.3.5b. If σx = σt, then unif σ A ↔ unif σ (Axt). *)
Lemma replace_list_eq:
  forall sigma x t A,
  sigma (V x) = sigma t ->
  unif sigma A <-> unif sigma (replace_list A x t).
Proof.
  intros sigma x t A H. split.
  - intros H0. induction A.
    + simpl. apply H0.
    + simpl. destruct a. apply unif_cons in H0 as []. apply unif_cons. split.
      * simpl in *. repeat rewrite replace_term_eq; destruct H1; trivial.
(*         { apply H0. }
        { destruct H1. apply H1. }
        { apply H. }
        { destruct H1. apply H1. }
        { apply H. } *)
      * apply IHA. apply H1.
  - intros H0. induction A.
    + simpl in H0. apply H0.
    + simpl in H0. destruct a. apply unif_cons. apply unif_cons in H0 as []. split.
      * simpl in H0. rewrite replace_term_eq in H0. rewrite replace_term_eq in H0.
        { apply H0. }
        { destruct H1. apply H1. }
        { apply H. }
        { destruct H1. apply H1. }
        { apply H. }
      * apply IHA. apply H1.
Qed.

(* 9.3.5c. x ≐ t :: A ≈ x ≐ t :: Axt *)
Lemma unif_equiv_replace:
  forall x t A,
  unif_equiv ((V x,t)::A) ((V x,t)::(replace_list A x t)).
Proof.
  intros x t a. unfold unif_equiv. intros sigma. split.
  - intros H. apply unif_cons in H as []. apply unif_cons. split.
    + apply H.
    + apply replace_list_eq.
      * apply H.
      * apply H0.
  - intros H. apply unif_cons. apply unif_cons in H as []. split.
    + apply H.
    + apply replace_list_eq in H0.
      * apply H0.
      * apply H.
Qed.

(* 9.3.5d. V(s xt ) ⊆ Vs ++Vt *)
Lemma incl_app_comm:
  forall {X} (A B C : list X),
  incl A (B ++ C) <-> incl A (C ++ B).
Proof.
  intros X A B C. split.
  - intros H. unfold incl in *. intros a H0. apply (in_app_or B C a) in H.
    + destruct H.
      * apply in_app_iff. right. apply H.
      * apply in_app_iff. left. apply H.
    + apply H0.
  - intros H. unfold incl in *. intros a H0. apply (in_app_or C B a) in H.
    + destruct H.
      * apply in_app_iff. right. apply H.
      * apply in_app_iff. left. apply H.
    + apply H0.
Qed.

Lemma incl_replace_vars:
  forall s x t,
  incl (vars_term (replace_term s x t)) ((vars_term s)++(vars_term t)).
Proof.
  intros s x t. induction s.
  - simpl. rewrite cons_app. destruct (beq_nat x v) eqn:H.
    + apply incl_appr. apply incl_refl.
    + apply incl_appl. apply incl_refl.
  - simpl. apply incl_app.
    + rewrite (incl_app_comm (vars_term (replace_term s1 x t)) (vars_term s1 ++ vars_term s2) (vars_term t)).
      rewrite incl_app_comm in IHs1. rewrite app_assoc. apply incl_appl. apply IHs1.
    + rewrite <- app_assoc. apply incl_appr. apply IHs2.
Qed.

(* 9.3.5e. V(Axt) ⊆ VA++Vt *)
Lemma incl_replace_list:
  forall A x t,
  incl (vars_list (replace_list A x t)) ((vars_list A)++(vars_term t)).
Proof.
  intros A x t. induction A.
  - simpl. unfold incl. contradiction.
  - destruct a as [s0 t0]. simpl. repeat rewrite <- app_assoc. repeat apply incl_app.
    + apply incl_app_comm. repeat rewrite <- app_assoc.
      apply incl_appr. apply incl_appr. apply incl_app_comm. apply incl_replace_vars.
    + apply incl_appr. apply incl_app_comm. rewrite <- app_assoc.
      apply incl_appr. apply incl_app_comm. apply (incl_replace_vars t0 x t).
    + apply incl_appr. apply incl_appr. apply IHA.
Qed.

(* 9.3.5f. x ≐ t :: A ⊲ x ≐ t :: Axt *)
Fact replacement_unif_rule:
  forall x t A,
  refinement ((V x,t)::A) ((V x,t)::(replace_list A x t)).
Proof.
  intros x t A. unfold refinement. split.
  - simpl. apply incl_cons.
    + simpl. left. reflexivity.
    + rewrite cons_app. apply incl_appr. apply incl_app_comm. apply incl_app.
      * apply incl_appr. apply incl_refl.
      * apply incl_replace_list.
  - apply unif_equiv_replace.
Qed.

(* Exercise 9.3.6 Prove the following fact about principal unifiers: If A ≈ B and σ
   is a principal unifier of A, then σ is a principal unifier of B. *)
Fact principal_unif_equiv:
  forall A B sigma,
  unif_equiv A B ->
  principal_unifier sigma A ->
  principal_unifier sigma B.
Proof.
  unfold principal_unifier. intros A B sigma H []. split.
  - unfold unif_equiv in H. apply H. apply H0.
  - intros tau H2 s. apply H1. unfold unif_equiv in H. apply H. apply H2.
Qed.

(* Exercise 9.3.7 Give a solved equation list that has more than one principal unifier. *)

(* Exercise 9.3.8 (Confrontation Rule)
   Prove [x ≐ s1 · s2; x ≐ t1 · t2] ⊲ [x ≐ s1 · s2; s1 ≐ t1; s2 ≐ t2]. The operational
   reading of this fact yields the so-called confrontation rule. The confrontation
   rule can often be used in place of the replacement rule when an equation list is
   transformed to solved form. In contrast to the replacement rule it has the virtue
   that it introduces only terms that are subterms of the original terms. This fact
   matters for efficient unification algorithms. *)
Fact confrontation_unif_rule:
  forall x s1 s2 t1 t2,
  refinement [(V x,T s1 s2);(V x,T t1 t2)] [(V x,T s1 s2);(s1,t1);(s2,t2)].
Proof.
  intros x s1 s2 t1 t2. unfold refinement. split.
  - simpl. apply incl_cons.
    + simpl. left. reflexivity.
    + repeat rewrite app_nil_r. rewrite cons_app. apply incl_appr.
      repeat apply incl_app; intuition. (* trivial, don't feel like writing apply incl_appr 15 times *)
  - unfold unif_equiv. intros sigma. split.
    + intros H. apply unif_cons in H as H1. destruct H1. unfold unif in H. destruct H.
      unfold subst in H. repeat (apply unif_cons; split).
      * apply H0.
      * rewrite H in H0. apply unif_cons in H1 as []. rewrite H in H1. rewrite H1 in H0.
        inversion H0. reflexivity.
      * rewrite H in H0. apply unif_cons in H1 as []. rewrite H in H1. rewrite H1 in H0.
        inversion H0. reflexivity.
      * apply unif_nil. apply H1.
    + intros H. apply unif_cons in H as H1. destruct H1. unfold unif in H. destruct H.
      unfold subst in H. repeat (apply unif_cons; split).
      * apply H0.
      * rewrite H0. repeat rewrite H. f_equal.
        { apply H2. simpl. right. left. reflexivity. }
        { apply H2. simpl. right. right. left. reflexivity. }
      * apply unif_nil. apply H1.
Qed.

(* ============================ *)
(* 9.4 Presolved Equation Lists *)
(* ============================ *)

Inductive presolved : list eqn -> Prop :=
  | presolved_nil   : presolved []
  | presolved_cons  : forall x t A, (V x <> t) -> presolved A -> presolved (((V x),t)::A).

Fixpoint presolve_term s t : list eqn :=
  match (s,t) with
  | (V x, V y) => if (x =? y) then [] else [(s,t)]
  | (V x, _) => [(s,t)]
  | (_, V x) => [(t,s)]
  | (T s1 s2, T t1 t2) => (presolve_term s1 t1) ++ (presolve_term s2 t2)
  end.

Fixpoint presolve A : list eqn :=
  match A with
  | nil => nil
  | (s,t)::A' => (presolve_term s t)++(presolve A')
  end.

Lemma presolved_app:
  forall A B,
  presolved A -> presolved B -> presolved (A++B).
Proof.
  intros A B H H0. induction A.
  - simpl. apply H0.
  - simpl. destruct a as [s t]. destruct s.
    + apply presolved_cons.
      * inversion H. apply H3.
      * apply IHA. inversion H. apply H5.
    + inversion H.
Qed.

(* Exercise 9.4.2 Prove Lemma 9.4.1. *)
(* 9.4.2a. [s ≐ t] ⊲ pre′ s t and pre′ s t is presolved. *)
Lemma presolve_term_refinement:
  forall s t,
  refinement [(s,t)] (presolve_term s t).
Proof.
  induction s; induction t.
  - simpl. destruct (v =? v0) eqn:H.
    + apply beq_nat_true_iff in H. rewrite H. apply deletion_unif_rule.
    + apply refinement_refl.
  - simpl. apply refinement_refl.
  - simpl. apply swap_unif_rule.
  - simpl. apply (refinement_trans [(T s1 s2, T t1 t2)] [(s1,t1);(s2,t2)] (presolve_term s1 t1 ++ presolve_term s2 t2)).
    + apply decomposition_unif_rule.
    + apply (refinement_app [(s1,t1)] (presolve_term s1 t1) [(s2,t2)] (presolve_term s2 t2)).
      * apply IHs1.
      * apply IHs2.
Qed.

Lemma presolve_term_presolved:
  forall s t,
  presolved (presolve_term s t).
Proof.
  intros s. induction s.
  - intros. destruct t.
    + simpl. destruct (v =? v0) eqn:H.
      * apply presolved_nil.
      * apply presolved_cons. apply beq_nat_false_iff in H. congruence. apply presolved_nil.
    + simpl. apply presolved_cons.
      * congruence.
      * apply presolved_nil.
  - induction t.
    + simpl. apply presolved_cons.
      * congruence.
      * apply presolved_nil.
    + simpl. apply presolved_app.
      * apply IHs1.
      * apply IHs2.
Qed.

(* 9.4.2b. A ⊲ pre A and pre A is presolved. *)
Lemma presolve_list_refinement:
  forall A,
  refinement A (presolve A).
Proof.
  intros A. induction A.
  - simpl. apply refinement_refl.
  - destruct a. simpl. apply (refinement_app [(t, t0)] (presolve_term t t0) A (presolve A)).
    + apply presolve_term_refinement.
    + apply IHA.
Qed.

Lemma presolve_list_presolve:
  forall A,
  presolved (presolve A).
Proof.
  intros A. induction A.
  - simpl. apply presolved_nil.
  - destruct a. simpl. apply presolved_app.
    + apply presolve_term_presolved.
    + apply IHA.
Qed.

(* ===================== *)
(* Unification Algorithm *)
(* ===================== *)

Fixpoint solveN n A B : option (list eqn) :=
  match n, presolve B with
  | O, _ => None
  | S n', (V x,t) :: C => if [In x (vars_term t)] then None else solveN n' ((V x,t) :: A) (replace_list C x t)
  | S n', _ => Some A
end.

Definition solveE A B := solveN (1 + length(vars_list B)) A B.

Definition solve C := solveE nil C.

(* The proof of solveN_correct is pleasant and leads to subgoals expressing
   proof obligations one would expect from an informal correctness argument for
   solve. One first reverts A and B and then continues by induction on n. The base
   case is trivial. For the inductive case one simulates the case analysis of the function
   solveN. For the recursion step one applies the inductive hypothesis, which
   produces subgoals for the preconditions. *)
Lemma solveN_correct A B C n :
  refinement C (A ++ B) ->
  solved A ->
  disjoint (domain A) (vars_list B) ->
  length (vars_list B) < n ->
  match solveN n A B with
  | Some D => refinement C D /\ solved D
  | None => ~ unifiable C
  end.
Proof.
  revert A B.
  induction n.
  - intros A B H H0 H1 H2. simpl. intro. admit.
  - intros A B H H0 H1 H2. induction B.
    + simpl. split.
      * rewrite app_nil_r in H. apply H.
      * apply H0.
    + destruct a as [s t]. destruct s.
      * simpl. Admitted.

Lemma solveE_correct A B C :
  refinement C (A ++ B) ->
  solved A ->
  disjoint (domain A) (vars_list B) ->
  match solveE A B with
  | Some D => refinement C D /\ solved D
  | None => ~ unifiable C
  end.
Proof.
  intros H H0 H1.
  apply solveN_correct.
  - apply H.
  - apply H0.
  - apply H1.
  - unfold lt. simpl. apply le_n.
Qed.

Theorem solve_correct C :
  match solve C with
  | Some A => refinement C A /\ solved A
  | None => ~ unifiable C
  end.
Proof.
  apply solveE_correct.
  - simpl. apply refinement_refl.
  - apply solved_nil.
  - unfold disjoint. intros [x []]. inversion H.
Qed.

author: dandougherty


text:
(** * Definition of ε, the CFG accepting only "" *)
Require Import Coq.Strings.String Coq.Lists.List.
Require Import ParsingParses.Parsers.ContextFreeGrammar.

Set Implicit Arguments.

Section generic.
  Variable CharType : Type.
  Variable String : string_like CharType.

  Definition trivial_grammar : grammar CharType :=
    {| Start_symbol := "";
       Lookup := fun _ => nil::nil;
       Valid_nonterminals := ""%string::nil |}.

  Definition trivial_grammar_parses_empty_string : parse_of_grammar _ (Empty String) trivial_grammar.
  Proof.
    hnf; simpl.
    apply ParseHead.
    constructor.
  Defined.

  Lemma trivial_grammar_parses_only_empty_string s : parse_of_grammar _ s trivial_grammar -> s = Empty String.
  Proof.
    intro H; hnf in H; simpl in H.
    repeat match goal with
             | _ => reflexivity
             | [ H : parse_of _ _ _ _ |- _ ] => inversion_clear H
             | [ H : parse_of_production _ _ _ _ |- _ ] => inversion_clear H
           end.
  Qed.
End generic.

author: JasonGross

repo: parsing-parses


text:
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Instantiation of the Ring tactic for the binary natural numbers *)

Require Import Bool.
Require Export LegacyRing.
Require Export ZArith_base.
Require Import NArith.
Require Import Eqdep_dec.

Definition Neq (n m:N) :=
  match (n ?= m)%N with
  | Datatypes.Eq => true
  | _ => false
  end.

Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
  intros n m H; unfold Neq in H.
  apply N.compare_eq.
  destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
Qed.

Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
  split.
    apply N.add_comm.
    apply N.add_assoc.
    apply N.mul_comm.
    apply N.mul_assoc.
    apply N.add_0_l.
    apply N.mul_1_l.
    apply N.mul_0_l.
    apply N.mul_add_distr_r.
    apply Neq_prop.
Qed.

Add Legacy Semi Ring
  N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].

author: coq-contribs

repo: legacy-ring