soundness.v 915 Bytes
Newer Older
1
From iris.base_logic Require Export primitive derived.
2 3 4 5 6 7
Import uPred_entails uPred_primitive.

Section adequacy.
Context {M : ucmraT}.

(** Consistency and adequancy statements *)
8
Lemma soundness φ n : (Nat.iter n (λ P, |==>  P) (@uPred_pure M φ))%I  φ.
9 10 11 12 13 14 15 16 17 18
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 :
19
  ¬ (Nat.iter n (λ P, |==>  P) (False : uPred M))%I.
20 21
Proof. exact (soundness False n). Qed.

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