• Abel Nieto's avatar
    Add mapsto_mapsto_ne helper lemma · f227f6fa
    Abel Nieto authored
    Here's one case this lemma might be useful. Suppose we want to
    programmatically generate namespaces for e.g. locks:
    Definition lockN (l : loc) := nroot .@ "lock" .@ l.
    Then to know that two such namespaces are disjoint, we need to know
    that the corresponding locations are distinct. For that we use
    the lemma here introduced.
    Lemma ne l1 l2 v1 v2 :
      l1 ↦ v1 -∗ l2 ↦ v2 -∗ ⌜l1 ≠ l2⌝.
    Proof. iApply mapsto_mapsto_ne. (* goal ¬ ✓ 2%Qp *) by intros []. Qed.
To find the state of this project's repository at the time of any of these versions, check out the tags.