Commit 914f32ee authored by Robbert Krebbers's avatar Robbert Krebbers

More lenient pointer equality.

Pointer equality is now defined using absolute object offsets. The treatment
is similar to CompCert:

* Equality of pointers in the same object is defined provided the object has
  not been deallocated.
* Equality of pointers in different objects is defined provided both pointers
  have not been deallocated and both are strict (i.e. not end-of-array).

Thus, pointer equality is defined for all pointers that are not-end-of-array
and have not been deallocated. The following examples have defined behavior:

  int x, y;
  printf("%d\n", &x == &y);
  int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
  printf("%d\n", p == q);
  struct S { int a; int b; } s, *r = &s;
  printf("%d\n", &s.a + 1 == &(r->b));

The following not:

  int x, y;
  printf("%d\n", &x + 1 == &y);
parent 39d73ee8
......@@ -113,6 +113,13 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
Proof. by rewrite bool_decide_spec. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. by rewrite bool_decide_spec. Qed.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. by case_bool_decide. Qed.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false.
Proof. by case_bool_decide. Qed.
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
(P Q) bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed.
(** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment