| Age | Commit message (Collapse) | Author |
|---|
|
Fix bug in Shrink obligations with Program in the process.
Fix implementation of shrink for abstract proofs
- Update doc in term.mli to reflect the fact that let-in's
are part of what is returned by [decompose_lam_assum].
|
|
|
|
|
|
|
|
|
|
Use a much dumber algorithm to recognize the shape of equalities.
|
|
Take advantage that the provided term is always a variable in Equality.is_eq_x.
|
|
Do not evar-normalize the argument provided by afterHyp.
|
|
Do not normalize all goals beforehand.
|
|
Do not evar-normalize the term to substitute with. The engine should be
insensitive to this kind of modification.
|
|
We use simple variable substitution instead of full-power term
matching.
|
|
We do not check that an hypothesis is used in context declarations that
occur before it.
|
|
Comments
--------
- The tactic specialize conveys a somehow intuitive reasoning concept
and I would support continuing maintaining it even if the design
comes in my opinion with some oddities. (Note that the experience of
MathComp and SSReflect also suggests that specialize is an
interesting concept in itself).
There are two variants to specialize:
- specialize (H args) with H an hypothesis looks natural: we
specialize H with extra arguments and the "as pattern" clause comes
naturally as an extension of it, destructuring the result using the
pattern.
- specialize term with bindings makes the choice of fully applying the
term filling missing expressions with bindings and to then behave as
generalize. Wouldn't we like a more fine-grained approach and the
result to remain in the context?
In this second case, the "as" clause works as if the term were posed
in the context with "pose proof".
|
|
There were three versions of injection:
1. "injection term" without "as" clause:
was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
was introduction hypotheses using ipat in reverse order without
checking that the number of ipat was the size of the injection
(activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
was introduction hypotheses using ipat in left-to-right order
checking that the number of ipat was the size of the injection
and clearing the injecting term by default if an hypothesis
(activated with "Set Injection L2R Pattern Order", default one from 8.5)
There is now:
4. "injection term" without "as" clause, new version:
introducing the components of the injection in the context in
left-to-right order using default intro-patterns "?"
and clearing the injecting term by default if an hypothesis
(activated with "Set Structural Injection")
The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
introducing the hypotheses in the goal what corresponds to the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".
The flag is currently off.
|
|
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
|
|
|
|
In pat%constr, creating new evars is now allowed only if "eintros" is
given, i.e. "intros" checks that no evars are created, and similarly
e.g. for "injection ... as ... pat%constr".
The form "eintros [...]" or "eintros ->" with the case analysis or
rewrite creating evars is now also supported.
This is not a commitment to say that it is good to have an e- modifier
to tactics. It is just to be consistent with the existing convention.
It seems to me that the "no e-" variants are good for beginners. However,
expert might prefer to use the e-variants by default. Opinions from
teachers and users would be useful.
To be possibly done: do that [= ...] work on hypotheses with side
conditions or parameters based on the idea that they apply the full
injection and not only the restriction of it to goals which are
exactly an equality, as it is today.
|
|
|
|
|
|
|
|
|
|
|
|
Suggested by R. Krebbers and C. Cohen, this makes modes
more applicable, by allowing to trigger resolution on partially
instantiated indices. This is a rough but fast approximation of the
pattern on which one would like instances to apply.
|
|
As noticed by C. Cohen it was confusingly different from standard
notation.
|
|
Fix test-suite files
|
|
Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.
|
|
Be more lenient, allowing non-class subgoals to remain
after resolution, this seems necessary when launching
resolution in goals containing evars.
Also put a tclONCE when hints don't need to backtrack.
|
|
|
|
- Treat shelved dependent subgoals that might not be
resolved after some proof search correctly by restarting
their resolution as soon as possible (if they are
typeclasses in only_classes mode).
- Treat dependencies between goals better, avoiding
backtracking more often when dependencies allow.
|
|
To deactivate the limitation of introductions (which was added to avoid
eta expansions in proof terms). This can cause huge blowups due to dumb
backtracking. The arrow introduction rule is reversible, so better do it
eagerly!
|
|
Set Typeclasses Compatibility "8.5". uses the old resolution
tactic (off by default, but useful for debugging incompatibilities)
Set Typeclasses Unification Compatibility "8.5".
uses the old clenv unification tactic in resolution even
with the new proof engine (on by default for now).
Also fix the 8.5-compatible unification with the new engine resolution
function, by using with_shelf and unshelve.
|
|
|
|
|
|
Report limit exceeded on _any_ branch so that we pursue search
if it was reached at least once. Add example by N. Tabareau in
test-suite.
|
|
Fix typo in proofview
|
|
with full backtracking across multiple goals.
|
|
simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
|
|
|
|
|
|
|
|
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
|
|
|
|
Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
|
|
|
|
Now, type_scope is consistently used whether it is an hypothesis or
the conclusion, and consistently not used when in "context".
The question of a compatibility support, e.g., as suggested by Jason,
using a scope is still open though.
See reports #3050 and #4398.
|
|
The exact and e_exact tactics were not registering the universes and
constraints of the hint correctly. Now using the same connect_hint_clenv
as unify_resolve, they do. Also correct the implementation of
prepare_hint to normalize the universes of the hint before abstracting
its undefined universes. They are going to be refreshed at each
application. This means that eauto using term can
use multiple different instantiations of the universes of term
if term introduces new universes. If we want just one instantiation
then the term should be abbreviated in the goal first.
|
|
|
|
|
|
|
|
|
