From 0b56a3e33006b486b001e6d9aedc4afd2a4ec26a Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sat, 30 Jan 2016 12:53:35 +0100
Subject: [PATCH] show that we can implement the predecessor function

---
 barrier/lifting.v |  6 +++---
 barrier/tests.v   | 26 +++++++++++++++++++++++---
 2 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/barrier/lifting.v b/barrier/lifting.v
index 9306d369f..b226119c9 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -259,14 +259,14 @@ Proof.
 Qed.
 
 Lemma wp_le_false n1 n2 E Q :
-  n1 > n2 →
+  ~(n1 ≤ n2) →
   ▷Q LitFalseV ⊑ wp (Σ:=Σ) E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros Hle. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = LitFalse); last first.
   - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
+    exfalso. omega.
+  - intros ?. do 3 eexists. econstructor; omega.
   - reflexivity.
   - apply later_mono, forall_intro=>e2. apply impl_intro_l.
     apply const_elim_l=>->.
diff --git a/barrier/tests.v b/barrier/tests.v
index e822df3d1..3d215912f 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -93,9 +93,29 @@ Module LiftingTests.
       eapply impl_elim; first by eapply and_elim_l. apply and_intro.
       + apply const_intro; omega.
       + by rewrite !and_elim_r.
-    - rewrite -wp_le_false; last by omega.
-      rewrite -wp_case_inr // -!later_intro -wp_value' //.
+    - rewrite -wp_le_false /= // -wp_case_inr //.
+      rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
-      assert (Heq: n1 = pred n2) by omega. by subst n1=>{Hle Hgt}.
+      assert (Heq: n1 = pred n2) by omega. by subst n1.
+  Qed.
+
+  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
+                             (LitNat 0)
+                             (App (FindPred (Var 0)) (LitNat 0))
+                         ).
+  Lemma Pred_spec n E Q :
+    ▷Q (LitNatV $ pred n) ⊑ wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
+  Proof.
+    rewrite -wp_lam //. asimpl.
+    rewrite -(wp_bind _ _ (CaseCtx EmptyCtx _ _)).
+    assert (Decision (n ≤ 0)) as Hn by apply _.
+    destruct Hn as [Hle|Hgt].
+    - rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
+      apply later_mono. rewrite -!later_intro -wp_value' //.
+      assert (Heq: n = 0) by omega. by subst n.
+    - rewrite -wp_le_false /= // -wp_case_inr //.
+      apply later_mono. rewrite -!later_intro -FindPred_spec. apply and_intro.
+      + by apply const_intro; omega.
+      + done.
   Qed.
 End LiftingTests.
-- 
GitLab