Fix typos

See merge request iris/iris!557

Add library for monotonic nat ghost state

Closes #327

See merge request iris/iris!547

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Implemented as an algebra for rules about `auth max_natUR` and a
logic-level wrapper for the auth element (a nat) and fragment (a
persistent lower-bound).

Fixes #327.

Add swap lemmas for exist and forall

See merge request iris/iris!552

Add lemmas for validity of `●{_} _ ⋅ ●{_} _` for both view and auth.

See merge request !551

This also required changing the order a bit.

```coq
Lemma gmap_view_auth_frac_op_valid q1 q2 m1 m2 :
  ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2)  ✓ (q1 + q2)%Qp ∧ m1 ≡ m2.
Lemma gmap_view_auth_op_valid m1 m2 :
  ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2)  False.
```

The diff might be hard to read, because I had to change the order. The following
lemmas have been added:

```coq
Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
  ✓{n} (●V{q1} a1 ⋅ ●V{q2} a2)  ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ rel n a1 ε.
Lemma view_auth_op_validN n a1 a2 : ✓{n} (●V a1 ⋅ ●V a2)  False.

Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
  ✓ (●V{q1} a1 ⋅ ●V{q2} a2)  ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ∀ n, rel n a1 ε.
Lemma view_auth_op_valid a1 a2 : ✓ (●V a1 ⋅ ●V a2)  False.

Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
  ✓{n} (●{q1} a1 ⋅ ●{q2} a2)  ✓ (q1 + q2)%Qp ∧ a1 ≡{n}≡ a2 ∧ ✓{n} a1.
Lemma auth_auth_op_validN n a1 a2 : ✓{n} (● a1 ⋅ ● a2)  False.

Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
  ✓ (●{q1} a1 ⋅ ●{q2} a2)  ✓ (q1 + q2)%Qp ∧ a1 ≡ a2 ∧ ✓ a1.
Lemma auth_auth_op_valid a1 a2 : ✓ (● a1 ⋅ ● a2)  False.
```

add gmap_view type notation (mirroring auth)

See merge request iris/iris!544

gmap_view_auth: add fraction

Closes #356

See merge request !548

Strengthen validy of fragment of view camera

See merge request iris/iris!546

remove algebra/ dependency on base_logic/

Closes #355

See merge request !549

Thanks @Blaisorblade for reporting.

avoid relying on implicit instance generalization

See merge request iris/iris!545

clarify the intended use of gen_heap, and rename gen_heap_ctx -> gen_heap_interp

See merge request iris/iris!542