show that even \later^n False is inconsistent (for any fixed n); properly use...

show that even \later^n False is inconsistent (for any fixed n); properly use pvs in counter_examples

algebra/upred.v

@@ -346,10 +346,18 @@ Qed.
 Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
 Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
 
-Lemma sound : ¬ (True ⊢ False).
-Proof.
-  unseal. intros [H]. apply (H 0 ∅); last done. apply ucmra_unit_validN.
-Qed.
+Lemma soundness_later n : ¬ (True ⊢ ▷^n False).
+Proof.
+  unseal. intros [H].
+  assert ((▷^n @uPred_pure_def M False) n ∅)%I as Hn.
+  (* So Coq still has no nice way to say "make this precondition of that lemma a goal"?!? *)
+  { apply H; by auto using ucmra_unit_validN. }
+  clear H. induction n.
+  - done.
+  - move: Hn. simpl. unseal. done.
+Qed.
+Theorem soundness : ¬ (True ⊢ False).
+Proof. exact (soundness_later 0). Qed.
 
 Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
 Proof.

program_logic/counter_examples.v

@@ -9,11 +9,12 @@ Section savedprop.
   Notation iProp := (uPred M).
   Notation "¬ P" := (□(P → False))%I : uPred_scope.
 
-  (* Saved Propositions. *)
-  Context (sprop : Type) (saved : sprop → iProp → iProp).
+  (* Saved Propositions and view shifts. *)
+  Context (sprop : Type) (saved : sprop → iProp → iProp) (pvs : iProp → iProp).
+  Hypothesis pvs_mono : forall P Q, (P ⊢ Q) → pvs P ⊢ pvs Q.
   Hypothesis sprop_persistent : forall i P, PersistentP (saved i P).
   Hypothesis sprop_alloc_dep :
-    forall (P : sprop → iProp), True ⊢ ∃ i, saved i (P i).
+    forall (P : sprop → iProp), True ⊢ pvs (∃ i, saved i (P i)).
   Hypothesis sprop_agree :
     forall i P Q, saved i P ∧ saved i Q ⊢ P ↔ Q.
 
@@ -50,16 +51,17 @@ Section savedprop.
 
   (* We can obtain such a [Q i]. *)
   Lemma make_Q :
-    True ⊢ ∃ i, Q i.
+    True ⊢ pvs (∃ i, Q i).
   Proof.
     apply sprop_alloc_dep.
   Qed.
 
   (* Put together all the pieces to derive a contradiction. *)
-  Lemma contradiction : False.
+  (* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
+  Lemma contradiction : True ⊢ pvs False.
   Proof.
-    apply (@uPred.sound M). iIntros "".
-    iPoseProof make_Q as "HQ". iDestruct "HQ" as (i) "HQ".
+    rewrite make_Q. apply pvs_mono.
+    iIntros "HQ". iDestruct "HQ" as (i) "HQ".
     iApply (@no_self_contradiction (A i) _).
     by iApply Q_self_contradiction.
   Qed.