Commit 5f53a267 authored by Robbert's avatar Robbert

Merge branch 'robbert/base_logic_soundness' into 'master'

Nicer soundness statements for the base_logic

See merge request iris/iris!229
parents ccfa1196 473ad60b
Pipeline #15762 passed with stage
in 11 minutes and 52 seconds
......@@ -206,9 +206,11 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
(** Consistency/soundness statement *)
Lemma soundness_iter φ n : Nat.iter n sbi_later ( φ : uPred M)%I φ.
Proof. exact: uPred_primitive.soundness. Qed.
Lemma soundness_pure φ : bi_emp_valid (PROP:=uPredI M) φ φ.
Proof. apply soundness_pure. Qed.
Lemma soundness_later P : bi_emp_valid ( P) bi_emp_valid P.
Proof. apply soundness_later. Qed.
End restate.
(** New unseal tactic that also unfolds the BI layer.
......
......@@ -92,15 +92,18 @@ Global Instance uPred_ownM_sep_homomorphism :
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
(** Consistency/soundness statement *)
Lemma soundness φ n : (^n φ : uPred M)%I φ.
Proof. rewrite laterN_iter. apply soundness_iter. Qed.
Corollary soundness φ n : (^n φ : uPred M)%I φ.
Proof.
induction n as [|n IH]=> /=.
- apply soundness_pure.
- intros H. by apply IH, soundness_later.
Qed.
Corollary consistency_modal n : ¬ (^n False : uPred M)%I.
Proof. exact (soundness False n). Qed.
Corollary consistency : ¬(False : uPred M)%I.
Proof. exact (consistency_modal 0). Qed.
End derived.
End uPred.
......@@ -801,12 +801,14 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
Proof. by unseal. Qed.
(** Consistency/soundness statement *)
Lemma soundness φ n : (True iter n uPred_later ( φ )%I) φ.
Lemma soundness_pure φ : (True φ ) φ.
Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
Lemma soundness_later P : (True P) (True P).
Proof.
cut (iter n (@uPred_later M) ( φ )%I n ε φ).
{ intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
unseal. induction n as [|n IH]=> H; auto.
unseal=> -[HP]; split=> n x Hx _.
apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
by apply (HP (S n)); eauto using ucmra_unit_validN.
Qed.
End primitive.
End uPred_primitive.
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