Opaquify proofs in gmap_partial_alter (fix #46)

Closes #46

See merge request !106

Paolo G. Giarrusso authored 5 years ago and Robbert Krebbers committed 5 years ago

- Ensure gmap well-formedness proofs are fully opaque.
- Use pattern-matching lambdas over lets.

Add lemmas regarding set_seq

See merge request !105

Remove `:>>` subclass instance declarations

See merge request !104

There are not documented in
https://coq.inria.fr/refman/addendum/type-classes.html?highlight=class#coq:cmd.class,
and they don't have any advantage, so it's better to stop using them.

Update gitignore for compatibility with Coq master

See merge request !103

See https://github.com/coq/coq/pull/10947 (.coqdeps.d now uses the name
of the Coq Makefile) and https://github.com/coq/coq/pull/8642 (Coq now
generates empty interface files *.vos when compiling).

Add congruence lemmas for closures

See merge request !102

Add two useful lemmas

See merge request !101

Mentioned Windows line ending fix in README

See merge request iris/stdpp!100

Generalize `list_find` lemmas to become bi-implications.

See merge request !99

Thanks to @jules for the suggestion and an initial proof.

Disambiguate Haskell-style notations for partially applied operators

Closes #42

See merge request !93

For example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as
a prefix, as done in VST for example.

This closes issue #42.

I have used the `sed` script below. This script took care of nearly all uses
apart from a few occurrences where a space was missing, e.g. `(,foo)`. In
this case, `coqc` will just fail, allowing one to patch up things manually.

The script is slightly too eager on Iris developments, where it also replaces
`($ ...)` introduction patterns. When porting Iris developments you thus may
want to remove the line for `$`.

```
sed '
s/(= /(.= /g;
s/ =)/ =.)/g;
s/(≠ /(.≠ /g;
s/ ≠)/ ≠.)/g;
s/(≡ /(.≡ /g;
s/ ≡)/ ≡.)/g;
s/(≢ /(.≢ /g;
s/ ≢)/ ≢.)/g;
s/(∧ /(.∧ /g;
s/ ∧)/ ∧.)/g;
s/(∨ /(.∨ /g;
s/ ∨)/ ∨.)/g;
s/( /(. /g;
s/ )/ .)/g;
s/(→ /(.→ /g;
s/ →)/ →.)/g;
s/($ /(.$ /g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(, /(., /g;
s/ ,)/ ,.)/g;
s/(∘ /(.∘ /g;
s/ ∘)/ ∘.)/g;
s/(∪ /(.∪ /g;
s/ ∪)/ ∪.)/g;
s/(⊎ /(.⊎ /g;
s/ ⊎)/ ⊎.)/g;
s/(∩ /(.∩ /g;
s/ ∩)/ ∩.)/g;
s/(∖ /(.∖ /g;
s/ ∖)/ ∖.)/g;
s/(⊆ /(.⊆ /g;
s/ ⊆)/ ⊆.)/g;
s/(⊈ /(.⊈ /g;
s/ ⊈)/ ⊈.)/g;
s/(⊂ /(.⊂ /g;
s/ ⊂)/ ⊂.)/g;
s/(⊄ /(.⊄ /g;
s/ ⊄)/ ⊄.)/g;
s/(∈ /(.∈ /g;
s/ ∈)/ ∈.)/g;
s/(∉ /(.∉ /g;
s/ ∉)/ ∉.)/g;
s/(≫= /(.≫= /g;
s/ ≫=)/ ≫=.)/g;
s/(!! /(.!! /g;
s/ !!)/ !!.)/g;
s/(⊑ /(.⊑ /g;
s/ ⊑)/ ⊑.)/g;
s/(⊓ /(.⊓ /g;
s/ ⊓)/ ⊓.)/g;
s/(⊔ /(.⊔ /g;
s/ ⊔)/ ⊔.)/g;
s/(:: /(.:: /g;
s/ ::)/ ::.)/g;
s/(++ /(.++ /g;
s/ ++)/ ++.)/g;
s/(≡ₚ /(.≡ₚ /g;
s/ ≡ₚ)/ ≡ₚ.)/g;
s/(≢ₚ /(.≢ₚ /g;
s/ ≢ₚ)/ ≢ₚ.)/g;
s/(::: /(.::: /g;
s/ :::)/ :::.)/g;
s/(+++ /(.+++ /g;
s/ +++)/ +++.)/g;
' -i $(find -name "*.v")
```

Fix w.r.t. coq/coq#10764.

See merge request !98

More lemmas for `filter` w.r.t. maps

See merge request !96

Fix Open/Close scope

See merge request !94

Use Open/Close Scope without Local (i.e., export the scope opening)
only when the scope corresponds to the main purpose of the module.