Utilities for lifting camera properties to iProp, used in swap_later_impl.v and persistence.v.

From iris.algebra Require Import gmap.
From iris.base_logic Require Import iprop.

In practice, in this code P meant to abstract over type classes, but this is not supported by Coq.
Implicit Types (P : cmra Type) (F : rFunctor) (Σ : gFunctors).

Set Suggest Proof Using.
Set Default Proof Using "Type".

Notation LiftCPropToRFunctor P F :=
  ( A `(!Cofe A) B `(!Cofe B), P (rFunctor_car F A B)).
Notation LiftCPropToGFunctors P Σ :=
  ( i, LiftCPropToRFunctor P (gFunctors_lookup Σ i)).

All lemmas below are used to generate typeclass instances; the LiftCProp× lemmas are templates for instances, and LiftCProp×_type are helpers for declaring them. See swap_later_impl.v for the intended usage.

Lift to #[].

Notation LiftCPropToGFunctors_nil_type P := (LiftCPropToGFunctors P #[]).

Lemma LiftCPropToGFunctors_nil P : LiftCPropToGFunctors_nil_type P.
Proof. movei. apply fin_0_inv with (p := i). Qed.

Lift to gFunctors.app.

Notation LiftCPropToGFunctors_app_type P :=
  ( Σ Σ' ( : LiftCPropToGFunctors P Σ) (HΣ' : LiftCPropToGFunctors P Σ'),
    LiftCPropToGFunctors P (gFunctors.app Σ Σ')).

Lemma LiftCPropToGFunctors_app P : LiftCPropToGFunctors_app_type P.
  intros; apply fin_add_inv with (i := i); intros;
    [rewrite /= fin_add_inv_l|rewrite /= fin_add_inv_r]; auto.

Lift to gFunctors.singleton.

Notation LiftCPropToGFunctors_GFunctor_type F P :=
  ( (fp : LiftCPropToRFunctor P F),
  LiftCPropToGFunctors P (gFunctors.singleton (GFunctor F))).

(* We abstract over rFunctorContractive explicitly, to make it an implicit
parameter. *)

Lemma LiftCPropToGFunctors_GFunctor `{!rFunctorContractive F} P :
  LiftCPropToGFunctors_GFunctor_type F P.
  intros; apply fin_S_inv with (i := i); first exact: fp.
  apply fin_0_inv.

Show what's needed to lift camera properties to iResUR (the resources used by iProp). This could be generated by typeclass search, but
  • I prefer a way to see the actual code.
  • In fact, we don't want typeclass search unfolding iResUR to prove a proposition is persistent, so we make it Typeclasses Opaque.
Typeclasses Opaque iResUR.

Section lift_cprop_iResUR.
  Context {P : cmra Type}.
  Context {P_discrete_funUR : {A} (B : A ucmra) `( i, P (B i)), P (discrete_funUR B)}.
  Context {P_gmapUR : `{Countable A} `(HpT : P T), P (gmapUR A T)}.

  Lemma lift_cprop_iResUR `{fp : LiftCPropToGFunctors P Σ} : P (iResUR Σ).
  Proof using Type×.
    rewrite /iResUR. apply P_discrete_funURi; apply P_gmapUR, fp.
End lift_cprop_iResUR.