Andrea Asperti [Thu, 3 Nov 2011 12:48:32 +0000 (12:48 +0000)]
1. we compare the expected branching with the actual one and
prune the candidate when the latter is larger. The optimization
is meant to rule out stange applications of flexible terms,
such as the application of eq_f that always succeeds.
2. At top level, we index local equalitites for paramodulation for
each cluster (i.e. we assume metas in a same cluster shares the
same context *)
Andrea Asperti [Wed, 2 Nov 2011 10:23:45 +0000 (10:23 +0000)]
--Tre the expected branching with the actual one and
prune the candidate when the latter is larger. The optimization
is meant to rule out stange applications of flexible terms,
such as the application of eq_f that always succeeds.
There is some gain but less than expected
Andrea Asperti [Fri, 28 Oct 2011 10:58:22 +0000 (10:58 +0000)]
-applicative_case has been rewritten and simplified;
the strategy should be clear, now.
- if we have an unkown ?n goal we instantiate it with I:True:Prop.
Due to the topological ordering of goals, ?n should not appear
in any other open goal, so its instantiation can be arbitrary.
- paramodulation is has only an implicit knowledge of the symmetry
of equality, hence it is in trouble to prove (a=b) = (b=a).
A try_sym tactic has been added to smart application to cover this
case.
Andrea Asperti [Fri, 28 Oct 2011 08:40:50 +0000 (08:40 +0000)]
New management of the resulting substitution in deep eq.
We reduced several time the goal vs the active table, possibly
resulting in a clash of names generating cyclic substitutions.
Andrea Asperti [Fri, 28 Oct 2011 08:13:03 +0000 (08:13 +0000)]
-pplicative_case has been rewritten and simplified;
the strategy should be clear, now.
- if we have an unkown ?n goal we instantiate it with I:True:Prop.
Due to the topological ordering of goals, ?n should not appear
in any other open goal, so its instantiation can be arbitrary.
- paramodulation is has only an implicit knowledge of the symmetry
of equality, hence it is in trouble to prove (a=b) = (b=a).
A try_sym tactic has been added to smart application to cover this
case.-This line, and those below, will be ignored--
Wilmer Ricciotti [Thu, 20 Oct 2011 10:45:34 +0000 (10:45 +0000)]
Matitaweb: added preliminary support for interactive disambiguation.
Ambiguous expressions are reported to the client and highlighted.
The possible interpretations are shown in stderr.
Wilmer Ricciotti [Tue, 18 Oct 2011 09:40:12 +0000 (09:40 +0000)]
Changes in "destruct" tactic (allowing performance improvements):
1) discrimination principles are now generated upon definition of an inductive
type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john
major's principles); in case JMeq wasn't loaded at that time, it is possible
to explicitly request the definition by means of the command
discriminator I.
2) destruct uses the aforementioned principle rather than generating a cut at
each discrimination step
3) destruct performs generalizations using the basic generalize0_tac, rather
than generalize_tac: this should bring small performance improvements.
"include" is no longer turned into an "include alias"
when the file to be included is already loaded. This
greatly speeds up inclusion, at the price of having
to manually add some "include alias" here and there.
New version (by Wilmer). The main difference w.r.t. previous one
is that it should not normalize the hypotheses and the conclusion
without any need to do that.
BEWARE: this version seems to be a little buggy. See "Wilmer: XXX"
comments in CerCo files. I commit it anyway and let the debug to
Wilmer. It only fails in three places.
projects / helm.git / log