soundness.v 1013 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 *)
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
Lemma soundness φ n :
  bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==>  P) ( φ ))%I  φ.
11
12
13
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15
    eapply H; first by eauto using ucmra_unit_validN.
    rewrite /bi_emp /= /uPred_emp. by unseal. }
16
  unseal. induction n as [|n IH]=> x Hx Hupd; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  destruct (Hupd (S n) ε) as (x'&?&?); rewrite ?right_id; auto.
18
19
20
21
  eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
Qed.

Corollary consistency_modal n :
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  ¬bi_valid (PROP:=uPredI M) (Nat.iter n (λ P, |==>  P) (False : uPred M))%I.
23
24
Proof. exact (soundness False n). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Corollary consistency : ¬bi_valid (PROP:=uPredI M) False.
26
27
Proof. exact (consistency_modal 0). Qed.
End adequacy.