soundness.v 916 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 : (Nat.iter n (λ P, |==>  P) (@uPred_pure M φ))%I  φ.
10 11 12 13 14 15 16 17 18 19
Proof.
  cut ( x, {n} x  Nat.iter n (λ P, |==>  P)%I (@uPred_pure M φ) n x  φ).
  { intros help H. eapply (help ); eauto using ucmra_unit_validN.
    eapply H; try unseal; by eauto using ucmra_unit_validN. }
  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
  destruct (Hupd (S n) ) as (x'&?&?); rewrite ?right_id; auto.
  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
Qed.

Corollary consistency_modal n :
20
  ¬ (Nat.iter n (λ P, |==>  P) (False : uPred M))%I.
21 22
Proof. exact (soundness False n). Qed.

23
Corollary consistency : ¬ (False : uPred M)%I.
24 25
Proof. exact (consistency_modal 0). Qed.
End adequacy.