From 900b58aebfc3c00f895237e8783972209266ccfb Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Mon, 13 Apr 2020 14:48:47 +0200
Subject: [PATCH] a bit of cleanup in bit.v

---
 theories/examples/bit.v | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/theories/examples/bit.v b/theories/examples/bit.v
index 487786e..d732c21 100644
--- a/theories/examples/bit.v
+++ b/theories/examples/bit.v
@@ -16,26 +16,21 @@ Definition bit_nat : expr :=
   (#1, flip_nat, (λ: "b", "b" = #1)).
 
 Definition bitτ : type :=
-  ∃: (TVar 0)%nat * (TVar 0%nat → TVar 0%nat) * (TVar 0%nat → TBool).
+  ∃: (TVar 0) * (TVar 0 → TVar 0) * (TVar 0 → TBool).
 
 Section bit_refinement.
   Context `{relocG Σ}.
 
   Definition bitf (b : bool) : nat :=
-    match b with
-    | true => 1
-    | false => 0
-    end.
+    if b then 1 else 0.
 
   (* This is the graph of the `bitf` function *)
   Definition bitτi : lrel Σ := LRel (λ v1 v2,
     (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(bitf b)⌝))%I.
 
-  Lemma bit_refinement Δ :
-    ⊢ REL bit_bool << bit_nat : interp bitτ Δ.
+  Lemma bit_refinement Δ : ⊢ REL bit_bool << bit_nat : interp bitτ Δ.
   Proof.
-    unfold bit_bool, bit_nat.
-    unfold bitτ. simpl.
+    unfold bitτ; simpl.
     iApply (refines_exists bitτi).
     progress repeat iApply refines_pair.
     - rel_values.
-- 
GitLab