(* iris/base_logic/lib/iprop.v *)
From iris.algebra Require Import gmap
From iris.algebra Require cofe_solver
From iris.base_logic Require Export base_logic
From iris.prelude Require Import options

Structure gFunctor:= GFunctor {
  gFunctor_F :> rFunctor;
  gFunctor_map_contractive : rFunctorContractive gFunctor_F;
}.

Global ArgumentsGFunctor _ {_}.

Global ExistingInstance gFunctor_map_contractive.
Add Printing Constructor gFunctor.

Record gFunctors:= GFunctors {
  gFunctors_len : nat;
  gFunctors_lookup : fin gFunctors_len → gFunctor
}.

Definition gid(Σ : gFunctors) := fin (gFunctors_len Σ).

Definition gname:= positive.
Canonical Structure gnameO := leibnizO gname.

Definition iResF(Σ : gFunctors) : urFunctor :=
  discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).

Definition nil: gFunctors := GFunctors 0 (fin_0_inv _).

Definition singleton(F : gFunctor) : gFunctors :=
    GFunctors 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).

Definition app(Σ1 Σ2 : gFunctors) : gFunctors :=
    GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
              (fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).

Coercion gFunctors.singleton : gFunctor >-> gFunctors.

Class subG(Σ1 Σ2 : gFunctors) := in_subG i :
  { j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.

Global HintMode subG ! + : typeclass_instances.

Lemma subG_invΣ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
Proof.
  move=> H; split.
  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
Qed.

Global InstancesubG_refl Σ : subG Σ Σ.
Proof. move=> i; by exists i. Qed.

Global InstancesubG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
Qed.

Global InstancesubG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
Proof.
  move=> H i; move: H=> /(_ i) [j ?].
  exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
Qed.

Parameter iPrePropO: gFunctors → ofe.

Global DeclareInstance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).

Definition iResUR(Σ : gFunctors) : ucmra :=
    discrete_funUR (λ i,
      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).

Notation iPropΣ := (uPred (iResUR Σ)).

Notation iPropOΣ := (uPredO (iResUR Σ)).

Notation iPropIΣ := (uPredI (iResUR Σ)).

Parameter iProp_unfold: ∀ {Σ}, iPropO Σ -n> iPrePropO Σ.

Parameter iProp_fold: ∀ {Σ}, iPrePropO Σ -n> iPropO Σ.

Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
    iProp_fold (iProp_unfold P) ≡ P.

Parameter iProp_unfold_fold: ∀ {Σ} (P : iPrePropO Σ),
    iProp_unfold (iProp_fold P) ≡ P.

Definition iProp_result(Σ : gFunctors) :
    solution (uPredOF (iResF Σ)) := solver.result _.

Definition iPrePropO(Σ : gFunctors) : ofe := iProp_result Σ.

Global InstanceiPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.

Definition iResUR(Σ : gFunctors) : ucmra :=
    discrete_funUR (λ i,
      gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).

Notation iPropΣ := (uPred (iResUR Σ)).

Notation iPropOΣ := (uPredO (iResUR Σ)).

Definition iProp_unfold{Σ} : iPropO Σ -n> iPrePropO Σ :=
    ofe_iso_1 (iProp_result Σ).

Definition iProp_fold{Σ} : iPrePropO Σ -n> iPropO Σ :=
    ofe_iso_2 (iProp_result Σ).

Lemma iProp_fold_unfold{Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
  Proof. apply ofe_iso_21. Qed.

Lemma iProp_unfold_fold{Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
  Proof. apply ofe_iso_12. Qed.

Lemma iProp_unfold_equivI{Σ} (P Q : iProp Σ) :
  iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
Proof.
  rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). apply: f_equivI.
Qed.