Commit b1ddcc68 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode

parents d4dc9190 6c6d0d65
......@@ -742,6 +742,11 @@ Proof.
apply persistently_mono, impl_elim with P; auto.
Qed.
Lemma persistently_emp_intro P : P <pers> emp.
Proof.
by rewrite -(left_id emp%I bi_sep P) {1}persistently_emp_2 persistently_absorbing.
Qed.
Lemma persistently_True_emp : <pers> True <pers> emp.
Proof. apply (anti_symm _); auto using persistently_emp_intro. Qed.
......
......@@ -111,7 +111,7 @@ Section bi_mixin.
bi_mixin_persistently_idemp_2 P : <pers> P <pers> <pers> P;
(* In the ordered RA model: [ε ≼ core x]. *)
bi_mixin_persistently_emp_intro P : P <pers> emp;
bi_mixin_persistently_emp_2 : emp <pers> emp;
bi_mixin_persistently_forall_2 {A} (Ψ : A PROP) :
( a, <pers> (Ψ a)) <pers> ( a, Ψ a);
......@@ -394,8 +394,8 @@ Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
Lemma persistently_idemp_2 P : <pers> P <pers> <pers> P.
Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
Lemma persistently_emp_intro P : P <pers> emp.
Proof. eapply bi_mixin_persistently_emp_intro, bi_bi_mixin. Qed.
Lemma persistently_emp_2 : (emp : PROP) <pers> emp.
Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
Lemma persistently_forall_2 {A} (Ψ : A PROP) :
( a, <pers> (Ψ a)) <pers> ( a, Ψ a).
......
......@@ -303,7 +303,7 @@ Proof.
rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
- intros P Q [?]. split=> i /=. by f_equiv.
- intros P. split=> i. by apply bi.persistently_idemp_2.
- intros P. split=> i. by apply bi.persistently_emp_intro.
- split=> i. by apply bi.persistently_emp_intro.
- intros A Ψ. split=> i. by apply bi.persistently_forall_2.
- intros A Ψ. split=> i. by apply bi.persistently_exist_1.
- intros P Q. split=> i. apply bi.sep_elim_l, _.
......
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