* Almost ready for release 0.99.1.
* Syntax changed:
*H => * as H
-H1 .. HN => -H1 .. -HN
intros => ##
pattern: in ... => {...}
* Library ported to the new syntax
Wilmer Ricciotti [Tue, 15 Nov 2011 11:38:04 +0000 (11:38 +0000)]
Matitaweb: goto bottom can now be undone step by step and also reports errors
(basic error reporting as in advance).
Should fix a problem with the status.
Matitaweb:
1) Adds a feature to enrich automation statements with their trace (after
successful execution)
2) Introduces a different syntax (/... trace lemma1, lemma2 .../) for
system-generated traces (as opposed to user-provided)
3) Graphical update hiding system-generated traces (they are provided as
a tooltip for inspection, when hovering with the mouse pointer on the
tactic)
4) Fixes a bug in the computation of the cursor position in the script.
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.
projects / helm.git / log