Commit b22f4b8f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Instantiate Iris proof mode with CFML sep logic.

parent a28dbcd8
......@@ -6,4 +6,5 @@ LambdaSep
LambdaSepCredits
LambdaSepRO
LambdaCF
LambdaCFCredits
\ No newline at end of file
LambdaCFCredits
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 LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleList ProofMode
# The official list of files that should be compiled by [make]
......
From Sep Require Export SepFunctor.
From iris Require Export bi.
Module SepLogicProofMode (SL : SepLogicCore).
Module Export SS := SepLogicSetup SL.
Canonical Structure hpropC := leibnizC hprop.
(* TODO *)
Definition hpersistently (H : hprop) : hprop := H.
(* TODO : remove plainly from the interface. *)
Definition hplainly (H : hprop) : hprop := H.
(* Proofmode's hpure has to be absorbing. So we redefine it here, and
we add later by hand the necessary infrastructure for hpure. *)
Definition hpure_proofmode (φ : Prop) : hprop := \[φ] \* \Top.
Program Canonical Structure hpropI : bi :=
Bi hpropC _ _ (@pred_incl _) hempty hpure_proofmode hand hor
(@pred_impl _) hforall hexists hstar hwand
hplainly hpersistently _ _.
Next Obligation. apply discrete_ofe_mixin, _. Qed.
Next Obligation.
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 ??? ->%prop_ext.
- solve_proper.
- solve_proper.
- solve_proper.
- by intros ???? ->%fun_ext_1.
- by intros ???? ->%fun_ext_1.
- solve_proper.
- solve_proper.
- solve_proper.
- solve_proper.
- intros ?????. rewrite /hpure_proofmode hstar_pure.
split; [done|apply htop_intro].
- intros ??. rewrite /hpure_proofmode=>Hφ h Hh. apply Hφ.
+ rewrite /hpure_proofmode hstar_pure in Hh. apply Hh.
+ rewrite hstar_pure. split; [done|]. apply htop_intro.
- rewrite /hpure_proofmode=>??? 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.
- auto.
- auto.
- auto.
- auto.
- auto.
- auto.
- admit. (* TODO : remove plainly from the interface. *)
- admit. (* TODO : remove plainly from the interface. *)
- auto.
- auto.
- auto.
- auto.
- auto.
- admit. (* TODO : define hpersistently correctly. *)
- admit. (* TODO : define hpersistently correctly. *)
Admitted.
End SepLogicProofMode.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment