----------------------------------------------------------------------
HINT_EXISTS_TAC                                               (Tactic)
----------------------------------------------------------------------
HINT_EXISTS_TAC : tactic

SYNOPSIS
Reduces an existentially quantified goal by finding a witness which, from the
assumption list, satisfies at least partially the body of the existential.

DESCRIBE
When applied to a goal {?x. t1 /\ ... /\ tn}, the tactic {HINT_EXISTS_TAC}
looks for an assumption of the form {ti[u/x]}, where {i} belongs to {1..n},
and reduces the goal by taking {u} as a witness for {x}.

FAILURE
Fails unless the goal contains an assumption of the expected form.

EXAMPLE
- The goal:

   b = 0, a < 1, c > 0 ?- ?x. x < 1

is turned by {HINT_EXISTS_TAC} into:

   b = 0, a < 1, c > 0 ?- a < 1


- However the tactic also allows to make progress if only one conjunct of the
  existential is satisfied. For instance, the goal:

   b = 0, a < 1, c > 0 ?- ?x. x < 1 /\ x + x = c

is turned by {HINT_EXISTS_TAC} into:

   b = 0, a < 1, c > 0 ?- a < 1 /\ a + a = c


- The location of the conjunct does not matter, the goal:

   b = 0, a < 1, c > 0 ?- ?x. x + x = c /\ x < 1

is turned by {HINT_EXISTS_TAC} into:

   b = 0, a < 1, c > 0 ?- a + a = c /\ a < 1


- It can be convenient to chain the call to {HINT_EXISTS_TAC} with one to
  {ASM_REWRITE_TAC} in order to remove automatically the satisfied conjunct:

   b = 0, a < 1, c > 0 ?- ?x. x + x = c /\ x < 1

is turned by {HINT_EXISTS_TAC THEN ASM_REWRITE_TAC[]} into:

   b = 0, a < 1, c > 0 ?- a + a = c


USES
Avoid providing a witness explicitly, in order to make the tactic script less
fragile.



SEEALSO
Tactic.EXISTS_TAC.

----------------------------------------------------------------------