Commit 8bc4cec0 authored by Ralf Jung's avatar Ralf Jung

create a hint database for solving some simple uPred's

parent bd7ebdec
...@@ -980,4 +980,14 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed. ...@@ -980,4 +980,14 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r P Q `{!AlwaysStable Q} : (P Q) P (P Q). Lemma always_entails_r P Q `{!AlwaysStable Q} : (P Q) P (P Q).
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End uPred_logic. End uPred. End uPred_logic.
(* uPred Hint DB *)
Create HintDb uPred.
Hint Resolve or_elim or_intro_l' or_intro_r' : uPred.
Hint Resolve and_intro and_elim_l' and_elim_r' : uPred.
Hint Resolve always_mono : uPred.
Hint Resolve sep_elim_l' sep_elim_r' sep_mono : uPred.
Hint Immediate True_intro False_elim : uPred.
End uPred.
...@@ -92,7 +92,7 @@ Lemma vs_open_close N E P Q R : ...@@ -92,7 +92,7 @@ Lemma vs_open_close N E P Q R :
Proof. Proof.
intros; apply (always_intro _ _), impl_intro_l. intros; apply (always_intro _ _), impl_intro_l.
rewrite always_and_sep_r assoc [(P _)%I]comm -assoc. rewrite always_and_sep_r assoc [(P _)%I]comm -assoc.
eapply pvs_open_close; [by eauto using sep_elim_l'..|]. eapply pvs_open_close; [by eauto with uPred..|].
rewrite sep_elim_r. apply wand_intro_l. rewrite sep_elim_r. apply wand_intro_l.
(* Oh wow, this is annyoing... *) (* Oh wow, this is annyoing... *)
rewrite assoc -always_and_sep_r'. rewrite assoc -always_and_sep_r'.
......
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