(* tests/heapprop_affine.v *)
From stdpp Require Import gmap
From iris.bi Require Import interface
From iris.proofmode Require Import proofmode
From iris.prelude Require Import options

Definition loc:= Z.

Definition val:= Z.

Record heapProp:= HeapProp {
  heapProp_holds :> gmap loc val → Prop;
  heapProp_closed σ1 σ2 : heapProp_holds σ1 → σ1 ⊆ σ2 → heapProp_holds σ2;
}.

Global ArgumentsheapProp_holds : simpl never.
Add Printing Constructor heapProp.

Inductive heapProp_equiv'(P Q : heapProp) : Prop :=
    { heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.

Local InstanceheapProp_equiv : Equiv heapProp := heapProp_equiv'.

Local InstanceheapProp_equivalence : Equivalence (≡@{heapProp}).
  Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
  Canonical Structure heapPropO := discreteO heapProp.

Inductive heapProp_entails(P Q : heapProp) : Prop :=
  { heapProp_in_entails : ∀ σ, P σ → Q σ }.

Local ProgramDefinition heapProp_pure_def (φ : Prop) : heapProp :=
  {| heapProp_holds _ := φ |}.
Solve Obligations with done.

Local DefinitionheapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.

Definition heapProp_pure:= unseal heapProp_pure_aux.

Local DefinitionheapProp_pure_unseal :
  @heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.

Definition heapProp_emp: heapProp := heapProp_pure True.

Local ProgramDefinition heapProp_and_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := P σ ∧ Q σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.

Local DefinitionheapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.

Definition heapProp_and:= unseal heapProp_and_aux.

Local DefinitionheapProp_and_unseal:
  @heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.

Local ProgramDefinition heapProp_or_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := P σ ∨ Q σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.

Local DefinitionheapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.

Definition heapProp_or:= unseal heapProp_or_aux.

Local DefinitionheapProp_or_unseal:
  @heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.

Local ProgramDefinition heapProp_impl_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∀ σ', σ ⊆ σ' → P σ' → Q σ' |}.
Next Obligation. intros P Q σ1 σ2 HPQ ? σ' ?; simpl in *. apply HPQ. by etrans. Qed.

Local DefinitionheapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.

Definition heapProp_impl:= unseal heapProp_impl_aux.

Local DefinitionheapProp_impl_unseal :
  @heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.

Local ProgramDefinition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
  {| heapProp_holds σ := ∀ a, Ψ a σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.

Local DefinitionheapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.

Definition heapProp_forall{A} := unseal heapProp_forall_aux A.

Local DefinitionheapProp_forall_unseal :
  @heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.

Local ProgramDefinition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
  {| heapProp_holds σ := ∃ a, Ψ a σ |}.
Solve Obligations with naive_solver eauto using heapProp_closed.

Local DefinitionheapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.

Definition heapProp_exist{A} := unseal heapProp_exist_aux A.

Local DefinitionheapProp_exist_unseal :
  @heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.

Local ProgramDefinition heapProp_sep_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
Next Obligation.
  intros P Q σ1 σ2 (σ11 & σ12 & -> & ? & ? & ?) ?.
  assert (σ11 ⊆ σ2) by (by etrans; [apply map_union_subseteq_l|]).
  exists σ11, (σ2 ∖ σ11). split_and!; [| |done|].
  - by rewrite map_difference_union.
  - by apply map_disjoint_difference_r1.
  - eapply heapProp_closed; [done|].
    apply map_union_reflecting_l with σ11; [done|..].
    + by apply map_disjoint_difference_r1.
    + by rewrite map_difference_union.
Qed.

Local DefinitionheapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.

Definition heapProp_sep:= unseal heapProp_sep_aux.

Local DefinitionheapProp_sep_unseal:
  @heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.

Local ProgramDefinition heapProp_wand_def (P Q : heapProp) : heapProp :=
  {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
Next Obligation.
  intros P Q σ1 σ2 HPQ ? σ' ??; simpl in *.
  apply heapProp_closed with (σ1 ∪ σ'); [by eauto using map_disjoint_weaken_l|].
  by apply map_union_mono_r.
Qed.

Local DefinitionheapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.

Definition heapProp_wand:= unseal heapProp_wand_aux.

Local DefinitionheapProp_wand_unseal:
  @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.

Local DefinitionheapProp_persistently_def (P : heapProp) : heapProp :=
  heapProp_pure (heapProp_entails heapProp_emp P).

Local DefinitionheapProp_persistently_aux : seal (@heapProp_persistently_def).
Proof. by eexists. Qed.

Definition heapProp_persistently:= unseal heapProp_persistently_aux.

Local DefinitionheapProp_persistently_unseal:
  @heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.

Definition heapProp_later(P : heapProp) : heapProp := P.

Local DefinitionheapProp_unseal :=
  (heapProp_pure_unseal, heapProp_and_unseal,
   heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
   heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
   heapProp_persistently_unseal).

Ltac unseal:= rewrite !heapProp_unseal /=.

Local ArgumentsheapProp_holds !_ _ /.

Lemma heapProp_bi_mixin:
    BiMixin
      heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
      heapProp_impl (@heapProp_forall) (@heapProp_exist)
      heapProp_sep heapProp_wand.
  Proof.
    split.
    -
      split; repeat destruct 1; constructor; naive_solver.
    -
      intros P Q; split.
      + intros [HPQ]; split; split; naive_solver.
      + intros [[HPQ] [HQP]]; split; naive_solver.
    -
      unseal=> n φ1 φ2 Hφ; split; naive_solver.
    -
      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
    -
      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
    -
      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
    -
      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> ? x; by apply HΦ.
    -
      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> -[x ?]; exists x; by apply HΦ.
    -
      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
    -
      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
    -
      unseal=> φ P ?; by split.
    -
      unseal=> φ P HP; split=> σ ?. by apply HP.
    -
      unseal=> P Q; split=> σ [??]; done.
    -
      unseal=> P Q; split=> σ [??]; done.
    -
      unseal=> P Q R [HPQ] [HPR]; split=> σ; split; auto.
    -

Lemma heapProp_bi_persistently_mixin:
    BiPersistentlyMixin
      heapProp_entails heapProp_emp heapProp_and
      (@heapProp_exist) heapProp_sep heapProp_persistently.
  Proof.
    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
    -
      unfold heapProp_emp. unseal. intros A Φ [H].
      destruct (H ∅) as [x ?]; [done|]. exists x. split=> σ _.
      eapply heapProp_closed; [done|]. by apply map_empty_subseteq.
    - by rewrite heapProp_persistently_unseal.
  Qed.

Lemma heapProp_bi_later_mixin:
    BiLaterMixin
      heapProp_entails heapProp_pure heapProp_or heapProp_impl
      (@heapProp_forall) (@heapProp_exist)
      heapProp_sep heapProp_persistently heapProp_later.
  Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.

Global InstanceheapProp_pure_forall : BiPureForall heapPropI.
Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.

Global InstanceheapProp_affine : BiAffine heapPropI.
Proof. exact: bi.True_intro. Qed.

Lemma heapProp_proofmode_test{A} (P Q Q' R : heapProp) (Φ Ψ : A → heapProp) :
  P ∗ Q ∗ Q' -∗
  □ R -∗
  □ (R -∗ ∃ x, Φ x) -∗
  ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
Proof.
  iIntros "(HP & HQ & HQ') #HR #HRΦ".
  iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
  iExists x. iFrame. by iSplitL.
Qed.