Commit 69220d28 authored by charguer's avatar charguer

functorized_iris

parent 4632198a
......@@ -10,7 +10,7 @@ License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaCF LambdaStruct.
From Sep Require Import LambdaCF LambdaStruct LambdaSepProofMode.
Import ProofMode.
Generalizable Variables A B.
......@@ -308,7 +308,7 @@ Proof using.
intros L. induction_wf: list_sub_wf L. intros p.
applys rule_app_fix=>//=. applys rule_if'.
- ram_apply rule_neq. auto with iFrame.
- unlock. xpull=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
- unlock. xpull ;=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|]. xpull=>p' x L' ?. subst.
applys rule_let. { ram_apply rule_get_tl. auto with iFrame. }
unlock=> q /=. xpull=>->.
......
......@@ -1168,38 +1168,3 @@ Proof using.
Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Proof mode definitions for LambdaSep *)
Module ProofMode.
Export SepBasicTactics.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop :=
Hexists H, H \* \[triple t H Q].
Lemma wp_equiv : forall t H Q,
triple t H Q <-> (H ==> wp t Q).
Proof using.
intros. unfold wp. iff M.
{ hsimpl. rew_heap~. }
{ applys~ rule_consequence (rm M). xpull~. }
Qed.
Instance triple_as_valid t H Q : AsValid (triple t H Q) (H - wp t Q).
Proof. rewrite /AsValid wp_equiv. apply as_valid. Qed.
Instance frame_wp p t R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (wp t Φ) (wp t Ψ).
Proof.
rewrite /Frame /wp=> HR. iIntros "[HR H]". iDestruct "H" as (H) "[HH %]".
iExists (H ?p R)%I. iFrame. iPureIntro. eapply rule_frame_consequence=>//.
iIntros (?) "[??]". iApply HR. iFrame.
Qed.
Instance wp_absorbing t Q : Absorbing (wp t Q).
Proof.
apply wp_equiv. rewrite /bi_absorbingly -htop_True comm.
apply rule_htop_pre. iIntros "$".
Qed.
End ProofMode.
Set Implicit Arguments.
From Sep Require Import LambdaSep.
(* ---------------------------------------------------------------------- *)
(** Proof mode definitions for LambdaSep *)
Require Import SepGPM.
Module ProofMode.
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicTactics.SS.
Export SepBasicGPM.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop :=
Hexists H, H \* \[triple t H Q].
Lemma wp_equiv : forall t H Q,
triple t H Q <-> (H ==> wp t Q).
Proof using.
intros. unfold wp. iff M.
{ hsimpl. rew_heap~. }
{ applys~ rule_consequence (rm M). xpull~. }
Qed.
Instance triple_as_valid t H Q : AsValid (triple t H Q) (H - wp t Q).
Proof. rewrite /AsValid wp_equiv. apply as_valid. Qed.
Instance frame_wp p t R Φ Ψ :
( v, Frame p R (Φ v) (Ψ v)) Frame p R (wp t Φ) (wp t Ψ).
Proof.
rewrite /Frame /wp=> HR. iIntros "[HR H]". iDestruct "H" as (H) "[HH %]".
iExists (H ?p R)%I. iFrame. iPureIntro. eapply rule_frame_consequence=>//.
iIntros (?) "[??]". iApply HR. iFrame.
Qed.
Instance wp_absorbing t Q : Absorbing (wp t Q).
Proof.
apply wp_equiv. rewrite /bi_absorbingly -htop_True comm.
apply rule_htop_pre. iIntros "$".
Qed.
(**--- TODO: factorize in SepGPM (with tactic rebinding?) *)
(* ProofMode's [iIntros] tend to move pure facts in Coq's context.
While, in general, this is desirable, this is not what we want
after having applied [local_ramified_frame] because we would loose
pure facts that will not be unified in [Q] when [Q] is an evar. As
a result, we use a specific version of this lemma where Q1 is
locked, and hence pure facts cannot escape.
This specific version is only used when the post-condition is
indeed an evar. *)
Lemma local_ramified_frame_locked {B} : forall (Q1 : B hprop) H1 F H Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* (locked Q1 \---* Q) ->
F H Q.
Proof using. unlock. apply local_ramified_frame. Qed.
Ltac ram_apply lem :=
lazymatch goal with
| |- ?F _ ?Q =>
(is_evar Q; eapply local_ramified_frame_locked) ||
eapply local_ramified_frame
end; [xlocal_core tt|eapply lem|iPrepare].
(* TODO: try to factorize this: *)
Ltac hpull_xpull_iris_hook tt ::=
unfold_proofmode.
End ProofMode.
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaCFTactics LambdaStruct ExampleListProofMode LambdaSepRO ExampleROProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
SRC := TLCbuffer Fmap SepFunctor SepTactics SepGPM LambdaSemantics LambdaSep LambdaSepProofMode LambdaCF LambdaCFTactics LambdaStruct ExampleListProofMode LambdaSepRO ExampleROProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO
......
......@@ -237,10 +237,351 @@ Parameter himpl_frame_l : forall H2 H1 H1',
End SepLogicCore.
(* ********************************************************************** *)
(** * FunctorSignature *)
(** NOTE: for simplicity, we duplicate all contents, not just types *)
Module Type SepLogicSetupSig (SL : SepLogicCore).
Export SL.
Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types P : Prop.
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** Disjunction *)
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
(** Non-separating conjunction *)
Definition hand (H1 H2 : hprop) : hprop :=
fun h => H1 h /\ H2 h.
(** Magic wand *)
Definition hwand (H1 H2 : hprop) : hprop :=
hexists (fun (H:hprop) => H \* (hpure (H \* H1 ==> H2))).
Notation "H1 \--* H2" := (hwand H1 H2)
(at level 43) : heap_scope.
(** Magic wand for post-conditions *)
Definition qwand A (Q1 Q2:A->hprop) :=
hforall (fun x => hwand (Q1 x) (Q2 x)).
Notation "Q1 \---* Q2" := (qwand Q1 Q2)
(at level 43) : heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Additional notation for entailment *)
Delimit Scope heap_scope with heap.
(** [H1 ==+> H2] is short for [H1 ==> H1 \* H2] *)
Notation "H1 ==+> H2" := (H1%heap ==> H1%heap \* H2%heap)
(at level 55, only parsing) : heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Additional notation for lifted existentials *)
Notation "'Hexists' x1 , H" := (hexists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (hexists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (hexists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) , H" := (Hexists (x1:T1), Hexists (x2:T2), H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) ( x2 : T2 ) ( x3 : T3 ) , H" := (Hexists (x1:T1), Hexists (x2:T2), Hexists (x3:T3), H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Notation for triples *)
(** Notation [F PRE H POST Q] for stating specifications, e.g.
[triple t PRE H POST Q] is the same as [triple t H Q] *)
Notation "F 'PRE' H 'POST' Q" :=
(F H Q)
(at level 69, only parsing) : heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Properties of [hprop] *)
Global Instance hinhab : Inhab hprop.
Proof using. intros. apply (Inhab_of_val hempty). Qed.
(* ---------------------------------------------------------------------- *)
(* ** Derived properties of [hempty], [hstar], [hpure], and [hexists] *)
Lemma hstar_hempty_r : forall H,
H \* \[] = H.
Proof using.
applys neutral_r_of_comm_neutral_l.
applys~ hstar_comm.
applys~ hstar_hempty_l.
Qed.
Lemma hstar_pure : forall P H h,
(\[P] \* H) h = (P /\ H h).
Proof using.
intros. extens. unfold hpure.
rewrite hstar_hexists.
rewrite* hstar_hempty_l.
iff (p&M) (p&M). { split~. } { exists~ p. }
Qed.
Lemma hpure_intro : forall P h,
\[] h ->
P ->
\[P] h.
Proof using.
introv M N. rewrite <- (hstar_hempty_l \[P]).
rewrite hstar_comm. rewrite~ hstar_pure.
Qed.
Lemma hpure_inv : forall P h,
\[P] h ->
P /\ \[] h.
Proof using.
introv M. rewrite <- hstar_pure.
rewrite~ hstar_hempty_r.
Qed.
Lemma hempty_eq_hpure_true :
\[] = \[True].
Proof using.
applys pred_ext_1. intros h. iff M.
{ applys* hpure_intro. }
{ forwards*: hpure_inv M. }
Qed.
Lemma hfalse_hstar_any : forall H,
\[False] \* H = \[False].
Proof using.
intros. applys pred_ext_1. intros h. rewrite hstar_pure. iff M.
{ false*. } { lets: hpure_inv M. false*. }
Qed.
Lemma hpure_eq_hexists_empty : forall P,
\[P] = (Hexists (p:P), \[]).
Proof using. auto. Qed.
Lemma hexists_intro : forall A (x:A) (J:A->hprop) h,
J x h ->
(hexists J) h.
Proof using. intros. exists~ x. Qed.
Lemma hexists_inv : forall A (J:A->hprop) h,
(hexists J) h ->
exists x, J x h.
Proof using. intros. destruct H as [x H]. exists~ x. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Derived properties of [himpl] *)
Lemma himpl_frame_r : forall H1 H2 H2',
H2 ==> H2' ->
(H1 \* H2) ==> (H1 \* H2').
Proof using.
introv M. do 2 rewrite (@hstar_comm H1). applys~ himpl_frame_l.
Qed.
Lemma himpl_hprop_l : forall P H H',
(P -> H ==> H') ->
(\[P] \* H) ==> H'.
Proof using.
introv W Hh. rewrite hstar_pure in Hh. applys* W.
Qed.
Lemma himpl_hprop_r : forall P H H',
P ->
(H ==> H') ->
H ==> (\[P] \* H').
Proof using.
introv HP W. intros h Hh. rewrite~ hstar_pure.
Qed.
Lemma himpl_hexists_l : forall A H (J:A->hprop),
(forall x, J x ==> H) ->
(hexists J) ==> H.
Proof using. introv W. intros h (x&Hh). applys* W. Qed.
Lemma himpl_hexists_r : forall A (x:A) H J,
(H ==> J x) ->
H ==> (hexists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma himpl_hexists : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hexists J1 ==> hexists J2.
Proof using. introv W. intros h (x&M). exists x. applys~ W. Qed.
Lemma himpl_hforall : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hforall J1 ==> hforall J2.
Proof using. introv W. intros h M x. applys W. applys M. Qed.
(* Note: missing properties for [himpl] on [hand] and [hor].
For properties on [hwand], see file [SepTactics]. *)
(* ---------------------------------------------------------------------- *)
(* ** Properties of [htop] *)
Lemma htop_intro : forall h,
\Top h.
Proof using. intros. exists~ (=h). Qed.
Lemma htop_eq :
\Top = (Hexists H, H).
Proof using. auto. Qed.
Lemma himpl_htop_r : forall H H',
H ==> H' ->
H ==> H' \* \Top.
Proof using.
introv M. unfold htop. rewrite (hstar_comm H').
rewrite hstar_hexists.
applys himpl_hexists_r \[]. rewrite~ hstar_hempty_l.
Qed.
Lemma htop_hstar_htop :
\Top \* \Top = \Top.
Proof using.
applys himpl_antisym.
{ unfold htop. rewrite hstar_hexists.
applys himpl_hexists_l. intros H.
rewrite hstar_comm.
rewrite hstar_hexists.
applys himpl_hexists_l. intros H'.
applys~ himpl_hexists_r (H' \* H). }
{ applys~ himpl_htop_r. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Auxiliary lemma showing that reasoning rule for extracting
pure propositions from preconditions is just a special case
of the reasoning rule for extracting existentials from preconditions. *)
Lemma rule_extract_hprop_from_extract_hexists :
forall (T:Type) (F:hprop->(T->hprop)->Prop),
(forall (A:Type) (J:A->hprop) (Q:T->hprop),
(forall x, F (J x) Q) ->
F (hexists J) Q) ->
(forall P H Q,
(P -> F H Q) ->
F (\[P] \* H) Q).
Proof using.
introv M. introv N. rewrite hpure_eq_hexists_empty.
rewrite hstar_hexists.
applys M. rewrite~ hstar_hempty_l.
Qed.
Arguments rule_extract_hprop_from_extract_hexists [T].
(* ---------------------------------------------------------------------- *)
(* ** Definition of [local] *)
(** Type of characteristic formulae on values of type B *)
Notation "'~~' B" := (hprop->(B->hprop)->Prop)
(at level 8, only parsing) : type_scope.
(** The [local] predicate is a predicate transformer that typically
applies to a characteristic formula, and allows for application
of the frame rule, of the rule of consequence, of the garbage
collection rule, and of extraction rules for existentials and
pure facts. *)
Definition local B (F:~~B) : ~~B :=
fun (H:hprop) (Q:B->hprop) =>
H ==> Hexists H1 H2 Q1,
H1 \* H2 \* \[F H1 Q1 /\ Q1 \*+ H2 ===> Q \*+ \Top].
(** The [is_local] predicate asserts that a predicate is subject
to all the rules that the [local] predicate transformer supports. *)
Definition is_local B (F:~~B) :=
F = local F.
(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x].
It is useful for describing loop invariants. *)
Definition is_local_pred A B (S:A->~~B) :=
forall x, is_local (S x).
(* ---------------------------------------------------------------------- *)
(* ** Notation for representation predicates *)
(** The arrow notation typically takes the form [x ~> R x],
to indicate that [X] is the logical value that describes the
heap structure [x], according to the representation predicate [R].
It is just a notation for the heap predicate [R X x]. *)
Definition repr (A:Type) (S:A->hprop) (x:A) : hprop :=
S x.
Notation "x '~>' S" := (repr S x)
(at level 33, no associativity) : heap_scope.
Lemma repr_eq : forall (A:Type) (S:A->hprop) (x:A),
(x ~> S) = (S x).
Proof using. auto. Qed.
(** [x ~> Id X] holds when [x] is equal to [X] in the empty heap.
[Id] is called the identity representation predicate. *)
Definition Id {A:Type} (X:A) (x:A) :=
\[ X = x ].
(* ---------------------------------------------------------------------- *)
(* ** Set operators to be opaque *)
Global Opaque hempty hpure hstar hexists htop repr.
End SepLogicSetupSig.
(* ********************************************************************** *)
(** * Functor *)
Module SepLogicSetup (SL : SepLogicCore).
Module SepLogicSetup (SL : SepLogicCore) : SepLogicSetupSig SL.
Export SL.
Implicit Types h : heap.
......@@ -518,6 +859,38 @@ Qed.
Arguments rule_extract_hprop_from_extract_hexists [T].
(* ---------------------------------------------------------------------- *)
(* ** Definition of [local] *)
(** Type of characteristic formulae on values of type B *)
Notation "'~~' B" := (hprop->(B->hprop)->Prop)
(at level 8, only parsing) : type_scope.
(** The [local] predicate is a predicate transformer that typically
applies to a characteristic formula, and allows for application
of the frame rule, of the rule of consequence, of the garbage
collection rule, and of extraction rules for existentials and
pure facts. *)
Definition local B (F:~~B) : ~~B :=
fun (H:hprop) (Q:B->hprop) =>
H ==> Hexists H1 H2 Q1,
H1 \* H2 \* \[F H1 Q1 /\ Q1 \*+ H2 ===> Q \*+ \Top].
(** The [is_local] predicate asserts that a predicate is subject
to all the rules that the [local] predicate transformer supports. *)
Definition is_local B (F:~~B) :=
F = local F.
(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x].
It is useful for describing loop invariants. *)
Definition is_local_pred A B (S:A->~~B) :=
forall x, is_local (S x).
(* ---------------------------------------------------------------------- *)
(* ** Notation for representation predicates *)
......
(* opam install coq-iris=branch.gen_proofmode.2018-03-16.1 *)
Set Implicit Arguments.
From TLC Require Export LibCore.
From Sep Require Export TLCbuffer SepFunctor.
From iris Require bi proofmode.tactics.
(* We undo the setup done by Stdpp. *)
Global Generalizable No Variables.
Global Obligation Tactic := Coq.Program.Tactics.program_simpl.
Module SepLogicGPM (SL : SepLogicCore) (SS : SepLogicSetupSig SL).
Export SS.
(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)
Module ProofModeInstantiate.
Import iris.bi.bi iris.proofmode.coq_tactics.
Export iris.proofmode.tactics.
Canonical Structure hpropC := leibnizC hprop.
Definition hpersistently (H : hprop) : hprop :=
fun _ => H heap_empty.
(* Proofmode's hpure has to be absorbing. So we redefine it here, and
we add later by hand the necessary infrastructure for CFML's hpure. *)
Definition hpure_abs (φ : Prop) : hprop := \[φ] \* \Top.
Program Canonical Structure hpropI : bi :=
Bi hprop _ _ (@pred_incl _) hempty hpure_abs hand hor
(@pred_impl _) hforall hexists hstar hwand hpersistently _ _.
Next Obligation. apply discrete_ofe_mixin, _. Qed.
Next Obligation.
Transparent hempty.
split; [split|..].
- intros ??; apply himpl_refl.
- intros ???; apply himpl_trans.
- intros. rewrite leibniz_equiv_iff. split=>?.
+ subst. auto.
+ apply himpl_antisym; naive_solver.
- by intros ??? ->%LibAxioms.prop_ext.
- solve_proper.
- solve_proper.
- solve_proper.
- by intros ???? ->%fun_ext_1.
- by intros ???? ->%fun_ext_1.
- solve_proper.
- solve_proper.
- solve_proper.
- intros ?????. rewrite /hpure_abs hstar_pure.
split; [done|apply htop_intro].
- intros ??. rewrite /hpure_abs=>Hφ h Hh. apply Hφ.
+ rewrite /hpure_abs hstar_pure in Hh. apply Hh.
+ rewrite hstar_pure. split; [done|]. apply htop_intro.
- rewrite /hpure_abs=>??? H. rewrite hstar_pure.
split; [|by apply htop_intro]. intros x. specialize (H x).
rewrite hstar_pure in H. apply H.
- by intros ??? [? _].
- by intros ??? [_ ?].
- intros P Q R HQ HR ?. by split; [apply HQ|apply HR].
- by left.
- by right.
- intros P Q R HP HQ ? [|]. by apply HP. by apply HQ.
- intros P Q R H ???. apply H. by split.
- intros P Q R H ? []. by apply H.
- intros A P Ψ H ???. by apply H.
- intros A Ψ a ? H. apply H.
- by eexists.
- intros A Φ Q H ? []. by eapply H.
- intros ??????. eapply pred_incl_trans. by apply himpl_frame_r.
rewrite (hstar_comm P Q') (hstar_comm Q Q'). by apply himpl_frame_r.
- intros. by rewrite hstar_hempty_l.
- intros. by rewrite hstar_hempty_l.
- intros. by rewrite hstar_comm.
- intros. by rewrite hstar_assoc.
- intros P Q R H ??. exists P. rewrite hstar_comm hstar_pure. auto.
- intros P Q R H. eapply pred_incl_trans.
{ rewrite hstar_comm. by apply himpl_frame_r. }
unfold hwand. rewrite hstar_comm hstar_hexists=>h [F HF].
rewrite (hstar_comm F) hstar_assoc hstar_pure in HF. destruct HF as [HR HF].
by apply HR.
- intros P Q H h. apply H.
- auto.
- unfold hpersistently, hempty. intros h _. auto.
- auto.
- auto.
- intros P Q h. replace (hpersistently P) with (\[P heap_empty] \* \Top).
{ rewrite hstar_assoc !hstar_pure=>-[? _]. auto using htop_intro. }
extens=>h'. rewrite hstar_pure /hpersistently. naive_solver auto using htop_intro.
- intros P Q h [HP HQ]. rewrite -(hstar_hempty_l Q) in HQ.
eapply himpl_frame_l, HQ. unfold hempty. intros ? ->. apply HP.
Qed.
Lemma hpure_pure φ : \[φ] = bi_affinely ⌜φ⌝.
Proof.
extens=>h. split.
- split; [by eapply hpure_inv|by apply (himpl_htop_r (H:=\[φ]))].
- intros [? Hφ]. apply hpure_intro; [done|].
change ((\[φ] \* \Top%I) h) in Hφ. rewrite hstar_pure in Hφ. naive_solver.
Qed.
Lemma htop_True : \Top = True%I.
Proof.
extens=>h. split=>?.
- rewrite /bi_pure /= /hpure_abs hstar_pure. auto.
- apply htop_intro.
Qed.
Opaque hpure_abs.
Ltac unfold_proofmode :=
change (@bi_and hpropI) with hand;
change (@bi_or hpropI) with hor;
change (@bi_emp hpropI) with hempty;
change (@bi_forall hpropI) with hforall;
change (@bi_exist hpropI) with hexists;
change (@bi_sep hpropI) with hstar;
change (@bi_wand hpropI) with hwand.
End ProofModeInstantiate.
(* ********************************************************************** *)
(* * Tactics for better integration of Iris Proof Mode with CFML Iris *)
Module ProofMode.
Export ProofModeInstantiate.
Import iris.proofmode.coq_tactics.
(* We need to repeat all these hints appearing in proofmode/tactics.v,
so that they state something about CFML connectives. [Hint Extern]
patterns are not matched modulo canonical structure unification. *)
Hint Extern 0 (_ ==> _) => iStartProof.
Hint Extern 0 (envs_entails _ \[_]) => iPureIntro.
Hint Extern 0 (envs_entails _ \[]) => iEmpIntro.
Hint Extern 0 (envs_entails _ (hforall _)) => iIntros (?).
Hint Extern 0 (envs_entails _ (_ \--* _)) => iIntros "?".
Hint Extern 1 (envs_entails _ (hand _ _)) => iSplit.
Hint Extern 1 (envs_entails _ (_ \* _)) => iSplit.
Hint Extern 1 (envs_entails _ (hexists _)) => iExists _.
Hint Extern 1 (envs_entails _ (hor _ _)) => iLeft.
Hint Extern 1 (envs_entails _ (hor _ _)) => iRight.
Hint Extern 2 (envs_entails _ (_ \* _)) => progress iFrame : iFrame.
(* Specific instances for CFML. *)
Hint Extern 3 (envs_entails _ ?P) => is_evar P; iAccu.
Hint Extern 3 (envs_entails _ (?P _)) => is_evar P; iAccu.
Hint Extern 0 (envs_entails _ (\[_] \* _)) => iSplitR.
Hint Extern 0 (envs_entails _ (\[_] _)) => iSplitR.
Hint Extern 0 (envs_entails _ (_ \* \[