It is barely used and causes a lot of confusion when used like 'l ↦ - * P'

Add duplicable type class

See merge request iris/iris!481

Makefile: fix recursive invocation to use `$(MAKE)`

See merge request iris/iris!561

Calling `make` is known-bad in many cases, but never as much as here:

```
make[2]: Nothing to be done for `pre-all'.
touch theories/algebra/ofe.vo
touch theories/algebra/monoid.vo
touch theories/algebra/cmra.vo
[...]
touch theories/heap_lang/lib/array.vo
make[2]: Nothing to be done for `post-all'.
make[1]: *** wait: No child processes.  Stop.
gmake: *** [Makefile:3: all] Error 2
```

Fix typos

See merge request iris/iris!559

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 iris/iris!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 iris/iris!548

Strengthen validy of fragment of view camera

See merge request iris/iris!546