exercises.gr_predicates

From iris.bi Require Export fixpoint.
From iris.heap_lang Require Import lang proofmode notation.

(* ################################ *)

Guarded Recursive Predicates

In the Linked List chapter, we defined a representation predicate for linked lists using Coq's Fixpoint mechanism. In this chapter, we present an alternative approach to defining representation predicates, which instead uses fixpoints of predicates. The high-level point to notice is that we can define fixpoints of monotone functions on Iris predicates, much in the same way as one can define fixpoints of monotone function on Coq predicates. Later on, we will discuss different kinds of fixpoints in more detail.

Section proofs.
Context `{!heapGS Σ}.

As we have already seen, we can define a predicate for linked lists representing a list of specific values, using Coq's notion of fixpoint for the inductive Coq type list val.
Fixpoint is_list_of (v : val) (xs : list val) : iProp Σ :=
  match xs with
  | [] => ⌜v = NONEV⌝
  | x :: xs => ∃ l : loc, ⌜v = SOMEV #l⌝ ∗ ∃ t, l ↦ (x, t) ∗ is_list_of t xs
  end.

However, sometimes we don't care about the exact list and instead, we only want to know that each value of the list satisfies some predicate. This can be captured by using a helper predicate all expressing that all elements of a Coq list satisfy a predicate.
Fixpoint all (xs : list val) (Φ : val → iProp Σ) : iProp Σ :=
  match xs with
  | [] => True
  | x :: xs => Φ x ∗ all xs Φ
  end.

Then, using all, we can express that a value represents some list whose elements satisfy a given predicate.
Definition is_list (v : val) (Φ : val → iProp Σ) : iProp Σ :=
  ∃ xs, is_list_of v xs ∗ all xs Φ.

However, this definition is rather annoying to work with, as it requires explicitly finding the list of values. Alternatively, we can define the is_list predicate as the solution to a recursive definition. This means defining a function:
F : (A → iProp Σ) → (A → iProp Σ)
A solution is then a function f satisfying f = F f. Solutions to such equations are called fixpoints as f doesn't change under F.
Definition is_list_pre (Φ : val → iProp Σ) (f : val → iProp Σ) (v : val) : iProp Σ :=
  ⌜v = NONEV⌝ ∨ ∃ l : loc, ⌜v = SOMEV #l⌝ ∗ ∃ x t, l ↦ (x, t) ∗ Φ x ∗ f t.

Recursive definitions can have multiple fixpoints. Of these, there are two special fixpoints: the least fixpoint and the greatest fixpoint. The least fixpoint corresponds to an inductively defined predicate, while the greatest corresponds to a coinductively defined predicate.
These solutions exist when F is monotone, as captured by the typeclass BiMonoPred.
Global Instance is_list_pre_mono Φ : BiMonoPred (is_list_pre Φ).
Proof.
  split.
  - intros Ψ1 Ψ2 H1 H2.
    iIntros "#HΨ %v [->|(%l & -> & %x & %t & Hl & Hx & Ht)]".
    + by iLeft.
    + iRight.
      iExists l.
      iSplitR; first done.
      iExists x, t.
      iFrame.
      iApply ("HΨ" with "Ht").
  -
In addition to monotonicity, we also need to prove that the resulting predicate is `time preserving' – NonExpansive. We will explain non-expansiveness in more detail later. In this case, it is trivial as values are discrete.
    apply _.
Qed.

Now that we have proved monotonicity, we can obtain the least fixed point along with associated lemmas for its unfolding and an induction principle.

Definition is_list_rec (v : val) (Φ : val → iProp Σ) :=
  bi_least_fixpoint (is_list_pre Φ) v.

Lemma is_list_rec_unfold (v : val) (Φ : val → iProp Σ) :
  is_list_rec v Φ ⊣⊢ is_list_pre Φ (λ v, is_list_rec v Φ) v.
Proof. apply least_fixpoint_unfold, _. Qed.

Lemma is_list_rec_ind (Φ Ψ : val → iProp Σ) :
  □ (∀ v, is_list_pre Φ Ψ v -∗ Ψ v ) -∗ ∀ v, is_list_rec v Φ -∗ Ψ v.
Proof. apply least_fixpoint_iter, _. Qed.

Of course, this new representation predicate, is_list_rec, should be equivalent to our original definition, is_list. We can indeed prove that this is the case.
Lemma is_list_rec_correct (v : val) (Φ : val → iProp Σ) :
  is_list v Φ ⊣⊢ is_list_rec v Φ.
Proof.
  iSplit.
  - iIntros "(%xs & Hv & HΦs)".
    iInduction xs as [|x xs] "IH" forall (v); simpl.
    + rewrite is_list_rec_unfold.
      by iLeft.
    + rewrite is_list_rec_unfold.
      iRight.
      iDestruct "Hv" as "(%l & -> & %t & Hl & Ht)".
      iDestruct "HΦs" as "[HΦ HΦs]".
      iExists l.
      iSplitR; first done.
      iExists x, t.
      iFrame.
      iApply ("IH" with "Ht HΦs").
  - iRevert (v).
    iApply is_list_rec_ind.
    iIntros "!> %v [->|(%l & -> & %x & %t & Hl & HΦ & %xs & Ht & Hxs)]".
    + by iExists [].
    + iExists (x :: xs); cbn.
      iFrame "HΦ Hxs".
      iExists l.
      iSplitR; first done.
      iExists t.
      iFrame.
Qed.

End proofs.