From baaee9e00c3da631db84eb340059a56b92188751 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 Jun 2014 16:29:24 +0200
Subject: [PATCH] Fix bugs in pointer operations

* Equality comparison of NULL and non NULL pointers should be defined
* Pointer comparisons, casts, and truth should only be defined for pointers
  that are alive
* Treat dead pointers as indeterminate values in refinements. The proofs that
  all operations preserve refinement indicate that dead pointers can be indeed
  by replaced by anything without affecting the program's behavior.
---
 theories/list.v    |  6 +++---
 theories/numbers.v |  5 -----
 theories/option.v  | 10 ++++++----
 3 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 78a0f2d1..eb16a6bb 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1260,12 +1260,12 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
   | _, [] => right (prefix_of_nil_not _ _)
   | x :: l1, y :: l2 =>
     match decide_rel (=) x y with
-    | left Exy =>
+    | left Hxy =>
       match go l1 l2 with
-      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Exy Hl1l2)
+      | left Hl1l2 => left (prefix_of_cons_alt _ _ _ _ Hxy Hl1l2)
       | right Hl1l2 => right (Hl1l2 ∘ prefix_of_cons_inv_2 _ _ _ _)
       end
-    | right Exy => right (Exy ∘ prefix_of_cons_inv_1 _ _ _ _)
+    | right Hxy => right (Hxy ∘ prefix_of_cons_inv_1 _ _ _ _)
     end
   end.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 84a7ce61..264f7ee3 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -500,11 +500,6 @@ Qed.
 Lemma Z_to_option_of_nat x : Z_to_option_nat (Z.of_nat x) = Some x.
 Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.
 
-(** The function [Z_of_sumbool] converts a sumbool [P] into an integer
-by yielding one if [P] and zero if [Q]. *)
-Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q} ) : Z :=
-  (if p then 1 else 0)%Z.
-
 (** Some correspondence lemmas between [nat] and [N] that are not part of the
 standard library. We declare a hint database [natify] to rewrite a goal
 involving [N] into a corresponding variant involving [nat]. *)
diff --git a/theories/option.v b/theories/option.v
index 62641831..5d4a9170 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -209,14 +209,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
     let y := fresh in destruct o as [y|] eqn:?;
       [change (x = f y) in H|change (x = None) in H]
-  | H : fmap (M:=option) _ ?o = ?x |- _ =>
+  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
-  | H : ?x = fmap (M:=option) _ ?o |- _ =>
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (Some (f y) = x) in H|change (None = x) in H]
+  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
-    destruct o eqn:?
+    let y := fresh in destruct o as [y|] eqn:?;
+      [change (x = Some (f y)) in H|change (x = None) in H]
   | _ => progress case_decide
   | _ => progress case_option_guard
   end.
-- 
GitLab