GitLab

We prove that various types are infinite, notably:
- nat, N, positive and Z;
- string (using pretty-printing of nat);
- option, with an infinite element type;
- list, with an inhabited element type.

Furthermore, we instantiate Fresh for strings.

This implements a simple linear search for fresh elements.

This generalizes Fix_unfold to a setoid setting. In particular,
we can use this to unfold multi-argument fixpoints without
requiring functional extensionality.

Infinity is described by having an injection from nat.

The documentation for some typeclasses used the wrong
names for these typeclasses.

This addresses some concerns in !5.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

This fixes the issue of Hai in !6.

This allows for more control over `Hint Mode`.

This way, type class search will fail immediately on first type
class constraint of any of the `fin_map_dom` lemmas if no `Dom`
can be found.

This instance leads to exponential failing searches.

These trees are useful to show that other types are countable.

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None ↔ m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None ↔ m !! j = None.

That is, we have to specify the type of `m`.

See also Coq bug #5712.