introduce_hyp.v

From iris.proofmode Require Import base coq_tactics reduction tactics.
From iris_automation Require Import env_utils util_classes solve_defs tele_utils.
From iris_automation.steps Require Import namer_tacs pure_solver.
From iris.bi Require Import bi telescopes.

Import bi.

Section mergable.
  Context {PROP : bi}.
  Implicit Types P : PROP.

  Lemma merge_and_consume P1 C p P2 P3 R:
    MergableConsume P1 C →
    C p P2 P3 →
    □?p P2 ∗ (P3 -∗ R) ⊢ P1 -∗ R.
  Proof.
    move => Hmerge HC /=. (* /Hmerge {Hmerge} /= HPs.*)
    iIntros "[HP2 HPR] HP1".
    iApply "HPR".
    iApply mergable_consume; [done | iFrame].
  Qed.

  Lemma merge_no_consume P1 C p P2 P3 R :
    MergablePersist P1 C →
    C p P2 P3 →
    □?p P2 ∗ (□?p P2 ∗ P1 -∗ □ P3 -∗ R) ⊢ P1 -∗ R.
  Proof.
    move => Hmerge HC /=.
    iIntros "[HP2 HPR] HP1".
    iAssert (□ P3)%I with "[HP1 HP2]" as "#HP3".
    { iApply mergable_persist; [done | iFrame]. }
    by iApply ("HPR" with "[$HP1 $HP2]").
  Qed.

End mergable.


Section mergable_env.
  Context {PROP : bi}.

  Class MergableEnv (Δ : envs PROP) (P : PROP) (M : PROP) :=
    mergable_env : (of_envs Δ) ∗ P ⊢ □ M.

  Instance mergable_env_base Δ P : 
    BiAffine PROP →
    MergableEnv Δ P True | 999.
  Proof. rewrite /MergableEnv; eauto. Qed.

  Instance mergable_env_cons Δ P C mi p P2 P3 M PR :
    BiAffine PROP →
    MergablePersist P C →
    FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2 →
    MergableEnv (envs_option_delete true mi p Δ) P M →
    MakeAnd M P3 PR →
    MergableEnv Δ P PR | 100.
    (* TODO: can this be done for nonaffine? *)
  Proof.
    rewrite /MergablePersist /MergableEnv /MakeAnd => HA HCP HΔ.
    apply (ficext_satisfies) in HΔ as HC.
    apply (findinextcontext_spec true) in HΔ.
    rewrite HΔ => {HΔ}.
    rewrite -assoc => HΔ <-.
    iIntros "(HP2 & HΔ & HP)".
    rewrite intuitionistically_and.
    iAssert (□ M)%I as "#HM".
    { iClear "HP2". iStopProof. by rewrite HΔ. }
    iFrame "HM". iClear "HM".
    iClear "HΔ".
    iStopProof.
    rewrite comm HCP //.
  Qed.

End mergable_env.


Section lemmas.
  Context {PROP : bi}.

  Implicit Types P Q : PROP.

  Lemma introduce_hyp_premise P Q :
    (P -∗ Q) ⊣⊢ IntroduceHyp P Q.
  Proof. by rewrite /IntroduceHyp /=. Qed.

  Lemma introduce_hyp_premise_sep P P1 P2 Q :
    IntoSepCareful P P1 P2 →
    IntroduceHyp P1 (IntroduceHyp P2 Q) ⊢ IntroduceHyp P Q.
  Proof.
    rewrite /IntoSepCareful /IntroduceHyp /= => ->.
    iIntros "HPQ [HP1 HP2]".
    by iApply ("HPQ" with "HP1").
  Qed.

  Lemma introduce_hyp_premise_tele_exist {TT} P R Q :
    IntoTExist P TT R →
    IntroduceVars (TT := TT) $ tele_map (λ R, IntroduceHyp R Q) R ⊢ IntroduceHyp P Q.
  Proof.
    rewrite /IntoTExist /IntroduceHyp /IntroduceVars /= => ->.
    iIntros "HRQ".
    iDestruct 1 as (tt) "HR".
    iSpecialize ("HRQ" $! tt).
    rewrite tele_map_app.
    by iApply "HRQ".
  Qed.

  (* Currently, IntoTExist cannot handle dependent exists. 
  For IntroduceHyp, we can overcome this by introducing the exists one by one: *)

  Lemma introduce_hyp_premise_exist (P Q : PROP) {A : Type} (R : A → PROP) :
    IntoExistCareful P R →
    IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q) ⊢ IntroduceHyp P Q.
  Proof.
    rewrite /IntoExistCareful /IntroduceHyp /IntroduceVars /= => ->.
    iIntros "HRQ".
    iDestruct 1 as (r) "HR".
    by iApply "HRQ".
  Qed.

  Lemma introduce_hyp_premise_or P P1 P2 Q : 
    IntoOr P P1 P2 →
    IntroduceHyp P1 Q ∧ IntroduceHyp P2 Q ⊢ IntroduceHyp P Q.
  Proof. 
    rewrite /IntroduceHyp /IntoOr /= => ->. 
    iIntros "HPQ [HP1|HP2]".
    - iDestruct "HPQ" as "[HPQ1 _ ]".
      by iApply "HPQ1".
    - iDestruct "HPQ" as "[_ HPQ2]".
      by iApply "HPQ2".
  Qed.

  Lemma introduce_hyp_mergable_consume p P C Q R S :
    MergableConsume Q C →
    C p P R →
    □?p P ∗ IntroduceHyp R S ⊢ IntroduceHyp Q S.
  Proof.
    rewrite /IntroduceHyp /= => Hmerge HC.
    eapply merge_and_consume => //.
  Qed.

  Lemma introduce_hyp_mergable_no_consume p P C Q R S :
    MergablePersist Q C →
    C p P R →
    □?p P ∗ (□?p P ∗ Q -∗ IntroduceHyp (□ R) S) ⊢ IntroduceHyp Q S.
  Proof.
    rewrite /IntroduceHyp /= => Hmerge HC.
    eapply merge_no_consume => //.
  Qed.

  Lemma introduce_hyp_premise_intuit P P' Q :
    IntoPersistent false P P' →
    Affine P →
    (□ P' -∗ Q) ⊢ IntroduceHyp P Q.
  Proof.
    rewrite /IntoPersistent /IntroduceHyp /= => -.
    iIntros (HPP' HP) "HP'Q HP".
    iApply "HP'Q".
    iStopProof.
    rewrite /bi_intuitionistically.
    by apply affinely_intro.
  Qed.

  Lemma introduce_hyp_drop_modal P M P' C Q :
    IntoModal false P M P' →
    DropModal M Q C →
    C P' →
    IntroduceHyp P' Q ⊢ IntroduceHyp P Q.
  Proof.
    rewrite /IntoModal /DropModal /IntroduceHyp /= => -> HQ /HQ //.
  Qed.

End lemmas.

Section coq_tactics.
  Context {PROP : bi}.

  Implicit Types P Q : PROP.

  Lemma tac_introduce_hyp_premise_sep Δ P P1 P2 Q :
    IntoSepCareful P P1 P2 →
    envs_entails Δ $ IntroduceHyp P1 (IntroduceHyp P2 Q) →
    envs_entails Δ $ IntroduceHyp P Q.
  Proof.
    rewrite envs_entails_eq => HΔΔ' ->.
    apply introduce_hyp_premise_sep, _.
  Qed.

  Lemma tac_introduce_hyp_premise_exist Δ P {A} (R : A → PROP) Q:
    IntoExistCareful P R →
    envs_entails Δ $ IntroduceVars (TT := [tele_pair A]) (λ a, IntroduceHyp (R a) Q) →
    envs_entails Δ $ IntroduceHyp P Q.
  Proof.
    rewrite envs_entails_eq => HPR ->.
    by eapply introduce_hyp_premise_exist.
  Qed.

  Lemma tac_introduce_hyp_premise_or Δ P P1 P2 Q :
    IntoOr P P1 P2 →
    envs_entails Δ $ IntroduceHyp P1 Q →
    envs_entails Δ $ IntroduceHyp P2 Q →
    envs_entails Δ $ IntroduceHyp P Q.
  Proof.
    rewrite envs_entails_eq => HP HΔ1 HΔ2.
    rewrite -introduce_hyp_premise_or.
    by apply and_intro.
  Qed.

  Lemma tac_introduce_hyp_premise_modal Δ P M P' C Q :
    IntoModal false P M P' →
    DropModal M Q C →
    C P' →
    envs_entails Δ $ IntroduceHyp P' Q →
    envs_entails Δ $ IntroduceHyp P Q.
  Proof.
    rewrite envs_entails_eq => HP HQC HCP ->.
    by eapply introduce_hyp_drop_modal.
  Qed.

  Lemma tac_introduce_hyp_merge_consume Δ P1 R C mi p P2 P3 :
    TCAnd (MergableConsume P1 C) (FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2) →
    envs_entails (envs_option_delete true mi p Δ) $ IntroduceHyp P3 R →
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
    rewrite envs_entails_eq => [[HP1 HP2]] HΔ.
    rewrite (findinextcontext_spec true) HΔ.
    eapply introduce_hyp_mergable_consume => //.
    by eapply ficext_satisfies in HP2.
  Qed.

  (* TODO: phrase this as a match, without an extra Δ'. This will make proofs smaller, thus Qed faster.
        See also https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/224 . Also check the tactics below *)
  Lemma tac_introduce_hyp_merge_persist j Δ P1 a P1' R C mi p P2 P3 :
    TCAnd (MergablePersist P1 C) (FindInExtendedContext Δ (λ p P2, C p P2 P3) mi p P2) →
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp (□ P3)%I R
    | _ => False
    end →
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
    rewrite envs_entails_eq /IntroduceHyp => [[HP1 HP2]] HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
    iIntros "HΔ' HP1".
    assert (P1 ⊢ □?a P1') as HP1_ent.
    { revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
      unfold bi_intuitionistically.
      rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
    iAssert (□ P3)%I as "#HP3"; last first. (* 'iEnough' *)
    { rewrite (envs_add_fresh_sound Δ) //.
      rewrite HP1_ent.
      iSpecialize ("HΔ'" with "HP1"). 
      by iApply (HΔR with "HΔ'"). }
    rewrite (findinextcontext_spec true).
    iDestruct "HΔ'" as "[HP2 _]".
    iCombine "HP1 HP2" as "HP".
    rewrite mergable_persist; last first.
    { by eapply ficext_satisfies in HP2. }
    done.
  Qed.

  Lemma tac_introduce_hyp_merge_env j Δ P1 a P1' R P3 :
    MergableEnv Δ P1 P3 →
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ IntroduceHyp (□ P3)%I R
    | _ => False
    end →
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
    rewrite envs_entails_eq /IntroduceHyp => HΔ HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
    iIntros "HΔ' HP1".
    assert (P1 ⊢ □?a P1') as HP1_ent.
    { revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
      unfold bi_intuitionistically.
      rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //. }
    iAssert (□ P3)%I as "#HP3"; last first. (* 'iEnough' *)
    { rewrite (envs_add_fresh_sound Δ) //.
      rewrite HP1_ent.
      iSpecialize ("HΔ'" with "HP1"). 
      by iApply (HΔR with "HΔ'"). }
    iCombine "HΔ' HP1" as "H".
    rewrite HΔ.
    eauto.
  Qed.

  Global Instance mergable_persist_from_box P C :
    MergablePersist P C →
    MergablePersist (□ P)%I C | 5.
  Proof.
    rewrite /MergablePersist => HPC p P2 P3 /HPC <-.
    iIntros "[#$ $]".
  Qed.
  Global Instance mergable_consume_from_box P C :
    MergableConsume P C →
    MergableConsume (□ P)%I C | 5.
  Proof.
    rewrite /MergableConsume => HPC p P2 P3 /HPC <-.
    iIntros "[#$ $]".
  Qed.

  Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R : 
    TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
        (TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
    match envs_add_fresh a j P1' Δ with
    | Some Δ' => envs_entails Δ' $ R
    | _ => False
    end →
    envs_entails Δ $ IntroduceHyp P1 R.
  Proof.
    rewrite envs_entails_eq /IntroduceHyp => HP1p' HΔR.
    destruct (envs_add_fresh a j P1' Δ) as [Δ'| ] eqn:HΔ''; last done.
    rewrite (envs_add_fresh_sound Δ) // HΔR.
    apply bi.wand_mono => //.
    revert HP1p'. case => [[HP1P1' HP1a] ->| [-> ->] ] //=.
    unfold bi_intuitionistically.
    rewrite -HP1P1' /=. unfold bi_affinely. iIntros "H"; iSplit => //.
  Qed.

  Lemma tac_introduce_hyp_premise_pure Δ P φ Q ba :
    IntoPure P φ →
    TCIf (Affine P) (TCEq ba true) (TCEq ba false) →
    match (if ba then Some Δ else envs_add_fresh false None True%I Δ) with
    | Some Δ' => φ → envs_entails Δ' Q
    | _ => False
    end →
    envs_entails Δ $ IntroduceHyp P Q.
  Proof.
    rewrite envs_entails_eq => HPφ HP.
    destruct HP as [HP ->| ->].
    - assert (IntoPersistent false P ⌜φ⌝).
      { rewrite /IntoPersistent /= HPφ.
        by rewrite -(persistently_if_pure true φ) /= persistently_idemp. }
      rewrite -introduce_hyp_premise_intuit => HΔφ.
      iIntros "HΔ %".
      by iApply HΔφ.
    - rewrite /IntroduceHyp.
      destruct (envs_add_fresh false None True Δ) as [Δ'| ] eqn:HΔ''; last done.
      rewrite HPφ => Hφ.
      apply bi.wand_intro_l.
      apply bi.wand_elim_l', bi.pure_elim' => /Hφ.
      apply envs_add_fresh_sound in HΔ''.
      rewrite HΔ'' /= => <-.
      apply bi.wand_intro_r.
      rewrite bi.wand_elim_r //.
  Qed.

  Lemma tac_introduce_hyp_premise_emp Δ Q :
    envs_entails Δ Q →
    envs_entails Δ $ IntroduceHyp emp%I Q.
  Proof. 
    rewrite envs_entails_eq => ->.
    by rewrite -introduce_hyp_premise left_id. 
  Qed.

End coq_tactics.

Ltac simplifySolveSepPureHyp := 
  match goal with
  | |- ?φ → ?P => 
    first
    [ let H := fresh "H" in assert (¬φ) as H by trySolvePure; by move => /H
    (* tries to prove ¬φ, to eliminate contradictory cases *)
    | lazymatch φ with
      | True => intros _
      | ?a = ?a => intros _
      | _ => intros; simplify_eq; subst
      end]
  end.

Ltac introduceHypStep namer_tac :=
  first
  [notypeclasses refine (tac_introduce_hyp_premise_emp _ _ _ )
  |notypeclasses refine (tac_introduce_hyp_premise_sep _ _ _ _ _ _ _); [ iSolveTC | ]
  |notypeclasses refine (tac_introduce_hyp_premise_exist _ _ _ _ _ _); [ iSolveTC | simpl]
  |notypeclasses refine (tac_introduce_hyp_premise_or _ _ _ _ _ _ _ _ ); [ iSolveTC | simpl | simpl]
  |notypeclasses refine (tac_introduce_hyp_premise_modal _ _ _ _ _ _ _ _ _ _); 
    [iSolveTC | iSolveTC | simpl; iSolveTC | ]
  (* rules below this do actual introduction of separation logic premises *)
  |notypeclasses refine (tac_introduce_hyp_premise_pure _ _ _ _ _ _ _ _); 
    [ iSolveTC | iSolveTC | simpl; simplifySolveSepPureHyp ]
  |notypeclasses refine (tac_introduce_hyp_merge_consume _ _ _ _ _ _ _ _ _ _); 
    [iSolveTC | register_delete namer_tac; simpl ]
  | lazymatch goal with
    | |- envs_entails ?Δ (IntroduceHyp ?P _) =>
      let j := namer_tac NameTac.GetName Δ P in first
      [notypeclasses refine (tac_introduce_hyp_merge_persist j _ _ _ _ _ _ _ _ _ _ _ _ _);
        [iSolveTC | iSolveTC | simpl ]
      |notypeclasses refine (tac_introduce_hyp_not_mergable j _ _ _ _ _ _ _);
        [iSolveTC | simpl ] ]
    end].