soundness.v 655 Bytes
Newer Older
1
From iris.base_logic Require Export base_logic.
2
Set Default Proof Using "Type".
3
Import uPred.
4
5
6
7
8

Section adequacy.
Context {M : ucmraT}.

(** Consistency and adequancy statements *)
9
Lemma soundness φ n : (^n  φ  : uPred M)%I  φ.
10
Proof.
11
12
  cut ((^n  φ  : uPred M)%I n ε  φ).
  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13
  rewrite /sbi_laterN; unseal. induction n as [|n IH]=> H; auto.
14
15
Qed.

16
Corollary consistency_modal n : ¬ (^n False : uPred M)%I.
17
18
Proof. exact (soundness False n). Qed.

19
Corollary consistency : ¬(False : uPred M)%I.
20
21
Proof. exact (consistency_modal 0). Qed.
End adequacy.