(* iris/bi/internal_eq.v *)
From iris.algebra Require Import excl csum
From iris.bi Require Export sbi
From iris.bi Require Import derived_laws_later
From iris.prelude Require Import options

Definition internal_eq`{!Sbi PROP} {A : ofe} (a b : A) : PROP :=
  <si_pure> siProp_internal_eq a b.

Global Argumentsinternal_eq : simpl never.

Global TypeclassesOpaque internal_eq.

Global Instance: Params (@internal_eq) 3 := {}.
Infix "≡" := internal_eq : bi_scope.
Infix "≡@{ A }" := (internal_eq (A := A)) (only parsing) : bi_scope.

Lemma sbi_prop_ext_mixin{PROP : bi} `{!SiEmpValid PROP} :
  (∀ P Q : PROP, <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q) →
  SbiPropExtMixin PROP _.
Proof. done. Qed.

Local HintResolve bi.or_elim bi.or_intro_l' bi.or_intro_r' : core.

Local HintResolve bi.True_intro bi.False_elim : core.

Local HintResolve bi.and_elim_l' bi.and_elim_r' bi.and_intro : core.

Local HintResolve bi.forall_intro : core.

Local HintExtern 100 (NonExpansive _) => solve_proper : core.

Lemma prop_ext_si_emp_valid_2P Q : <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q.
  Proof. apply sbi_mixin_prop_ext_si_emp_valid_2, sbi_sbi_prop_ext_mixin. Qed.

Global Instanceinternal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq PROP _ A).
  Proof.
    intros n x x' ? y y' ?. by apply si_pure_ne, siProp_primitive.internal_eq_ne.
  Qed.

Global Instanceinternal_eq_proper (A : ofe) :
    Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq PROP _ A).
  Proof. apply (ne_proper_2 _). Qed.

Lemma internal_eq_refl{A : ofe} P (a : A) : P ⊢ a ≡ a.
  Proof.
    rewrite (bi.True_intro P) -si_pure_pure.
    apply si_pure_mono, siProp_primitive.internal_eq_refl.
  Qed.

Lemma equiv_internal_eq{A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
  Proof. intros ->. apply internal_eq_refl. Qed.

Lemma pure_internal_eq{A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
  Proof. apply bi.pure_elim'=> ->. apply internal_eq_refl. Qed.

Local HintResolve equiv_internal_eq : core.

Lemma internal_eq_rewrite{A : ofe} a b (Ψ : A → PROP) :
    NonExpansive Ψ →
    internal_eq a b ⊢ Ψ a → Ψ b.
  Proof.
    intros.
    pose (Φ a' := (<si_emp_valid> (True -∗ Ψ a → Ψ a'))%I).
    assert (⊢ Φ a) as HΦa.
    { apply si_emp_valid_emp_valid, bi.wand_intro_l.
      by rewrite right_id -bi.entails_impl_True. }
    trans (<si_pure> (Φ a → Φ b) : PROP)%I.
    - apply si_pure_mono. apply siProp_primitive.internal_eq_rewrite.
      solve_proper.
    - unfold bi_emp_valid in HΦa. rewrite -HΦa left_id.
      rewrite /Φ si_pure_si_emp_valid_elim.
      by rewrite -(bi.True_intro emp)%I left_id.
  Qed.

Lemma internal_eq_rewrite'{A : ofe} a b (Ψ : A → PROP) P :
    NonExpansive Ψ →
    (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
  Proof.
    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
    apply bi.impl_elim_l'. by apply internal_eq_rewrite.
  Qed.

Lemma internal_eq_sym{A : ofe} (a b : A) : a ≡ b ⊢@{PROP} b ≡ a.
  Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.

Lemma internal_eq_trans{A : ofe} (a b c : A) : a ≡ b ∧ b ≡ c ⊢ a ≡ c.
  Proof.
    apply (internal_eq_rewrite' b a (λ b, b ≡ c)%I); auto.
    rewrite bi.and_elim_l. apply internal_eq_sym.
  Qed.

Lemma f_equivI{A B : ofe} (f : A → B) `{!NonExpansive f} x y :
    x ≡ y ⊢ f x ≡ f y.
  Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.

Lemma discrete_eq_1{A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
  Proof.
    intros. rewrite -si_pure_pure.
    by apply si_pure_mono, siProp_primitive.discrete_eq_1.
  Qed.

Lemma discrete_eq{A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    a ≡ b ⊣⊢ ⌜a ≡ b⌝.
  Proof.
    intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
  Qed.

Lemma fun_extI{A} {B : A → ofe} (f g : discrete_fun B) :
    (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
  Proof.
    rewrite /internal_eq -si_pure_forall.
    by apply si_pure_mono, siProp_primitive.fun_extI.
  Qed.

Lemma sig_equivI_1{A : ofe} (P : A → Prop) (x y : sig P) :
    `x ≡ `y ⊢@{PROP} x ≡ y.
  Proof. by apply si_pure_mono, siProp_primitive.sig_equivI_1. Qed.

Lemma prod_equivI{A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
  Proof.
    apply (anti_symm _).
    - apply bi.and_intro; apply f_equivI; apply _.
    - rewrite {3}(surjective_pairing x) {3}(surjective_pairing y).
      apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
      apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
  Qed.

Lemma sum_equivI{A B : ofe} (x y : A + B) :
    x ≡ y ⊣⊢
      match x, y with
      | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
      end.
  Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y,
               match x, y with
               | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
               end)%I); auto.
      destruct x; auto.
    - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
  Qed.

Lemma option_equivI{A : ofe} (x y : option A) :
    x ≡ y ⊣⊢ match x, y with
             | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
             end.
  Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y,
               match x, y with
               | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
               end)%I); auto.
      destruct x; auto.
    - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
  Qed.

Lemma csum_equivI{A B : ofe} (sx sy : csum A B) :
    sx ≡ sy ⊣⊢ match sx, sy with
               | Cinl x, Cinl y => x ≡ y
               | Cinr x, Cinr y => x ≡ y
               | CsumInvalid, CsumInvalid => True
               | _, _ => False
               end.
  Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' sx sy (λ sy',
               match sx, sy' with
               | Cinl x, Cinl y => x ≡ y
               | Cinr x, Cinr y => x ≡ y
               | CsumInvalid, CsumInvalid => True
               | _, _ => False
               end)%I); [solve_proper|auto|].
      destruct sx; eauto.
    - destruct sx; destruct sy; eauto;
      apply f_equivI, _.
  Qed.

Lemma excl_equivI{O : ofe} (x y : excl O) :
    x ≡ y ⊣⊢ match x, y with
             | Excl a, Excl b => a ≡ b
             | ExclInvalid, ExclInvalid => True
             | _, _ => False
             end.
  Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' x y (λ y',
               match x, y' with
               | Excl a, Excl b => a ≡ b
               | ExclInvalid, ExclInvalid => True
               | _, _ => False
               end)%I); [solve_proper|auto|].
      destruct x; eauto.
    - destruct x as [e1|]; destruct y as [e2|]; [|by eauto..].
      apply f_equivI, _.
  Qed.

Lemma sig_equivI{A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
  Proof.
    apply (anti_symm _).
    - apply sig_equivI_1.
    - apply f_equivI, _.
  Qed.

Lemma sigT_equivI{A : Type} {P : A → ofe} (x y : sigT P) :
      x ≡ y ⊣⊢
      ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
    Proof.
      apply (anti_symm _).
      - apply (internal_eq_rewrite' x y (λ y,
                 ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y))%I.
        + move => n [a pa] [b pb] [/=]; intros -> => /= Hab.
          apply bi.exist_ne => ?. by rewrite Hab.
        + done.
        + rewrite -(bi.exist_intro eq_refl) /=. auto.
      - apply bi.exist_elim. move: x y => [a pa] [b pb] /=. intros ->; simpl.
        apply (f_equivI _).
    Qed.

Lemma discrete_fun_equivI{A} {B : A → ofe} (f g : discrete_fun B) :
    f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
  Proof.
    apply (anti_symm _); auto using fun_extI.
    apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
  Qed.

Lemma ofe_morO_equivI{A B : ofe} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
  Proof.
    apply (anti_symm _).
    - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
    - rewrite -(discrete_fun_equivI (ofe_mor_car _ _ f) (ofe_mor_car _ _ g)).
      set (h1 (f : A -n> B) :=
        exist (λ f : A -d> B, NonExpansive (f : A → B)) f (ofe_mor_ne A B f)).
      set (h2 (f : sigO (λ f : A -d> B, NonExpansive (f : A → B))) :=
        @OfeMor _ A B (`f) (proj2_sig f)).
      assert (∀ f, h2 (h1 f) = f) as Hh by (by intros []).
      assert (NonExpansive h2) by (intros ??? EQ; apply EQ).
      by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
  Qed.

Lemma absorbingly_internal_eq{A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
  Proof. apply absorbingly_si_pure. Qed.

Lemma persistently_internal_eq{A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
  Proof. apply persistently_si_pure. Qed.

Global Instanceinternal_eq_absorbing {A : ofe} (x y : A) :
    Absorbing (PROP:=PROP) (x ≡ y).
  Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.

Global Instanceinternal_eq_persistent {A : ofe} (a b : A) :
    Persistent (PROP:=PROP) (a ≡ b).
  Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.

Lemma later_equivI_1{A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
  Proof.
    rewrite /internal_eq -si_pure_later.
    by apply si_pure_mono, siProp_primitive.later_equivI_1.
  Qed.

Lemma later_equivI_2{A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
  Proof.
    rewrite /internal_eq -si_pure_later.
    by apply si_pure_mono, siProp_primitive.later_equivI_2.
  Qed.

Lemma later_equivI{A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
  Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.

Lemma f_equivI_contractive{A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
    ▷ (x ≡ y) ⊢ f x ≡ f y.
  Proof.
    rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]].
    rewrite !Hfg. by apply f_equivI.
  Qed.

Lemma internal_eq_rewrite_contractive{A : ofe} a b (Ψ : A → PROP) :
    Contractive Ψ →
    ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
  Proof.
    intros. rewrite f_equivI_contractive.
    apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
  Qed.

Lemma internal_eq_rewrite_contractive'{A : ofe} a b (Ψ : A → PROP) P :
    Contractive Ψ →
    (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
  Proof.
    intros HΨ Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
    apply bi.impl_elim_l'. by apply internal_eq_rewrite_contractive.
  Qed.

Global Instanceeq_timeless {A : ofe} (a b : A) :
    TCOr (Discrete a) (Discrete b) →
    Timeless (PROP:=PROP) (a ≡ b).
  Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.

Lemma internal_eq_iffP Q : P ≡ Q ⊢ P ↔ Q.
  Proof.
    apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using bi.iff_refl.
  Qed.

Lemma affinely_internal_eq_wand_iffP Q : <affine> (P ≡ Q) ⊢ P ∗-∗ Q.
  Proof.
    apply (internal_eq_rewrite' P Q (λ Q, P ∗-∗ Q))%I; auto.
    - by rewrite bi.affinely_elim.
    - rewrite bi.affinely_elim_emp. apply bi.wand_iff_refl.
  Qed.

Lemma internal_eq_wand_iffP Q : P ≡ Q ⊢ <absorb> (P ∗-∗ Q).
  Proof.
    rewrite -(bi.persistent_absorbingly_affinely (P ≡ Q)).
    by rewrite affinely_internal_eq_wand_iff.
  Qed.

Lemma si_pure_internal_eq{A : ofe} (x y : A) : <si_pure> (x ≡ y) ⊣⊢ x ≡ y.
  Proof. done. Qed.

Lemma prop_ext_si_emp_validP Q : P ≡ Q ⊣⊢@{siPropI} <si_emp_valid> (P ∗-∗ Q).
  Proof.
    apply (anti_symm _); [|apply prop_ext_si_emp_valid_2].
    rewrite -(@si_pure_entails PROP) si_pure_internal_eq.
    apply (internal_eq_rewrite' P Q
      (λ Q, <si_pure> <si_emp_valid> (P ∗-∗ Q)))%I; auto.
    rewrite -bi.wand_iff_refl si_emp_valid_emp si_pure_pure. auto.
  Qed.

Lemma later_equivI_prop_2P Q : ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
  Proof.
    rewrite -!si_pure_internal_eq -si_pure_later !prop_ext_si_emp_valid.
    by rewrite -si_emp_valid_later bi.later_wand_iff.
  Qed.

Lemma internal_eq_soundness{A : ofe} (x y : A) : (⊢@{PROP} x ≡ y) → x ≡ y.
  Proof.
    intros ?%si_pure_emp_valid. by apply siProp_primitive.internal_eq_soundness.
  Qed.

Lemma internal_eq_entails{A B : ofe} (a1 a2 : A) (b1 b2 : B) :
    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
  Proof. rewrite si_pure_entails. apply siProp_primitive.internal_eq_entails. Qed.

Lemma ne_internal_eq{A B : ofe} (f : A → B) :
    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
  Proof.
    split; [apply f_equivI|]. intros Hf n x1 x2. by apply internal_eq_entails.
  Qed.

Lemma ne_2_internal_eq{A B C : ofe} (f : A → B → C) :
    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
  Proof.
    split.
    - intros Hf x1 x2 y1 y2.
      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
    - intros Hf n x1 x2 Hx y1 y2 Hy.
      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
      apply ne_internal_eq; [|done].
      intros [??] [??]. rewrite prod_equivI. apply Hf.
  Qed.

Lemma contractive_internal_eq{A B : ofe} (f : A → B) :
    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
  Proof.
    split; [apply f_equivI_contractive|].
    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
  Qed.

Global Instancesbi_later_contractive : BiLaterContractive PROP.
  Proof using Type*.
    rewrite /BiLaterContractive.
    apply contractive_internal_eq, later_equivI_prop_2.
  Qed.