WIP: better definition of uPred_pure. still not enough.

theories/base_logic/primitive.v

@@ -7,20 +7,28 @@ Local Hint Extern 10 (_ ≤ _) => omega.
 
 (** logical connectives *)
 Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := ∀ m, m ≤ n → ✓{m} x → φ |}.
+  {| uPred_holds n x := φ ∨ ¬ ✓{n} x |}.
 Solve Obligations with naive_solver eauto using cmra_validN_includedN.
-Next Obligation. intros. simpl in *. intros. eapply H; first done. eapply cmra_validN_includedN; try done.
-                 eapply cmra_includedN_le; done. Qed.
-Next Obligation. intros. simpl in *. intros. eapply H; last done. omega. Qed.
-Next Obligation. intros. simpl in *. intros. exfalso.
-                 (* Scratch this, uPred_invalid doesn't hold.  We have validity at the wrong step-index. *)
+Next Obligation.
+  intros. simpl in *. intros. destruct H; first by auto. right. intro.
+  apply H.
+  (* Scratch this, uPred_closed doesn't hold.  We have validity at the wrong step-index. *)
 Abort.
 
 Program Definition uPred_pure_def' {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := ✓{n} x → φ |}.
-Solve Obligations of uPred_pure_def' with naive_solver eauto using cmra_validN_includedN.
-Next Obligation of uPred_pure_def'. intros. simpl in *. intros. apply H.
-                    (* This doesn't hold; again we have validity at the wrong step-index. *)
+  {| uPred_holds n x := φ ∨ ∀ m, m ≤ n → ¬✓{m} x |}.
+Next Obligation of uPred_pure_def'.
+  intros. simpl in *. destruct H; first by auto. right. intros.
+  intro. eapply H; last eapply cmra_validN_includedN; try done.
+  eapply cmra_includedN_le; done.
+Qed.
+Next Obligation of uPred_pure_def'.
+  intros. simpl in *. destruct H; first by auto. right. intros.
+  apply H. omega.
+Qed.
+Next Obligation of uPred_pure_def'.
+  intros. simpl in *. right. intros. intro. apply H.
+  (* This doesn't hold; again we have validity at the wrong step-index. *)
 Abort.
 
 Definition uPred_pure_aux : seal (@uPred_pure_def). by eexists. Qed.