Coq: what does it mean to "saturate" a proof's context?

Question

As found in MPI-SWS' std++:

(** The class [TCUnless] can be used to check that search for [P]
fails. This is useful as a guard for certain instances together with
classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
(e.g. when saturating the context). *)
Notation TCUnless P := (TCIf P TCFalse TCTrue).

Answer 1

Given a set of starting hypotheses and a way to combine them into new hypotheses, "saturating the context" means to create as many hypotheses as possible from the starting set. This is used in proof automation to brute-force a solution.

Let's give a silly example: assume we're trying to prove that 3 <= 7, starting from the following hypotheses:

H1: 100 <= 100
H2: forall m n, S m < n -> m < n
H3: forall m n, S m < S n -> m < n

Then to saturate the context we would combine these three hypotheses repeatedly, obtaining proofs for thousands of propositions such as 99 <= 100, 99 <= 99, 98 <= 100, etc. One of these propositions would be 3 <= 7, so you could just conclude by calling the tactic assumption.