]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agoAssert false removed (in line with the variable case).
Andrea Asperti [Mon, 21 Nov 2011 09:42:44 +0000 (09:42 +0000)]
Assert false removed (in line with the variable case).

12 years ago{pattern} => in pattern;
Claudio Sacerdoti Coen [Mon, 21 Nov 2011 09:42:37 +0000 (09:42 +0000)]
{pattern} => in pattern;

12 years ago{pattern} => in pattern;
Claudio Sacerdoti Coen [Mon, 21 Nov 2011 09:41:59 +0000 (09:41 +0000)]
{pattern} => in pattern;

12 years agoTypo in comment
Andrea Asperti [Mon, 21 Nov 2011 09:19:28 +0000 (09:19 +0000)]
Typo in comment

12 years agohints
Enrico Tassi [Fri, 18 Nov 2011 17:11:53 +0000 (17:11 +0000)]
hints

12 years agocoercions
Enrico Tassi [Fri, 18 Nov 2011 16:45:22 +0000 (16:45 +0000)]
coercions

12 years agoSolves a bug that caused the auto statistics to refer to objects that are not
Wilmer Ricciotti [Fri, 18 Nov 2011 16:04:58 +0000 (16:04 +0000)]
Solves a bug that caused the auto statistics to refer to objects that are not
loaded in the environment, forcing them to be loaded and causing all sorts of
problems.

12 years agoAdded help for discriminator and inverter.
Wilmer Ricciotti [Fri, 18 Nov 2011 16:02:48 +0000 (16:02 +0000)]
Added help for discriminator and inverter.

12 years agoshort notation for "coercion"
Enrico Tassi [Fri, 18 Nov 2011 15:48:16 +0000 (15:48 +0000)]
short notation for "coercion"

12 years ago...
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:46:07 +0000 (15:46 +0000)]
...

12 years ago...
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:39:39 +0000 (15:39 +0000)]
...

12 years agominor Makefile fixes for the release
Enrico Tassi [Fri, 18 Nov 2011 15:21:25 +0000 (15:21 +0000)]
minor Makefile fixes for the release

12 years agoAuto parameters documented for 0.99.1.
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:17:05 +0000 (15:17 +0000)]
Auto parameters documented for 0.99.1.

12 years agoNo longer used parameters of auto removed.
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:15:22 +0000 (15:15 +0000)]
No longer used parameters of auto removed.

12 years agoThe macro /by _/ now expands again to something parsable.
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:00:42 +0000 (15:00 +0000)]
The macro /by _/ now expands again to something parsable.

12 years ago/by {}/ ==> /by/
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 15:00:17 +0000 (15:00 +0000)]
/by {}/ ==> /by/

12 years agoFor release 0.99.1.
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 14:31:39 +0000 (14:31 +0000)]
For release 0.99.1.

12 years ago* Almost ready for release 0.99.1.
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 13:07:03 +0000 (13:07 +0000)]
* 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

12 years agosupport for candidates of reducibility started ...
Ferruccio Guidi [Fri, 18 Nov 2011 12:27:16 +0000 (12:27 +0000)]
support for candidates of reducibility started ...

12 years agointros macro fixed
Claudio Sacerdoti Coen [Fri, 18 Nov 2011 12:06:38 +0000 (12:06 +0000)]
intros macro fixed

12 years agocollapse applications with a Match as head while indexing
Enrico Tassi [Thu, 17 Nov 2011 23:14:39 +0000 (23:14 +0000)]
collapse applications with a Match as head while indexing

12 years agocollapse applications with a Match as head while indexing
Enrico Tassi [Thu, 17 Nov 2011 23:14:26 +0000 (23:14 +0000)]
collapse applications with a Match as head while indexing

12 years agoTowards 0.95.1.
Claudio Sacerdoti Coen [Thu, 17 Nov 2011 00:07:33 +0000 (00:07 +0000)]
Towards 0.95.1.

12 years agoTowards the 0.95.1 release.
Claudio Sacerdoti Coen [Thu, 17 Nov 2011 00:04:01 +0000 (00:04 +0000)]
Towards the 0.95.1 release.

12 years agoIn preparation of 0.95.1 release.
Claudio Sacerdoti Coen [Thu, 17 Nov 2011 00:00:00 +0000 (00:00 +0000)]
In preparation of 0.95.1 release.

12 years ago- lambda_delta: context-free weak head normal forms continued ...
Ferruccio Guidi [Wed, 16 Nov 2011 23:40:42 +0000 (23:40 +0000)]
- lambda_delta: context-free weak head normal forms continued ...
-               delift started ...
- nnAuto: we removed an optimization that breaks lambda_delta

12 years agoNon working parts of the library commented out.
Claudio Sacerdoti Coen [Wed, 16 Nov 2011 17:50:21 +0000 (17:50 +0000)]
Non working parts of the library commented out.

12 years agoNever ported to new syntax.
Claudio Sacerdoti Coen [Wed, 16 Nov 2011 16:56:10 +0000 (16:56 +0000)]
Never ported to new syntax.

12 years agoinversion replaced by elim (???)
Andrea Asperti [Wed, 16 Nov 2011 15:15:13 +0000 (15:15 +0000)]
inversion replaced by elim (???)

12 years agosupport for weak head normal forms started ...
Ferruccio Guidi [Wed, 16 Nov 2011 13:14:07 +0000 (13:14 +0000)]
support for weak head normal forms started ...

12 years agocommit by user andrea
matitaweb [Wed, 16 Nov 2011 12:45:15 +0000 (12:45 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 16 Nov 2011 12:37:49 +0000 (12:37 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 16 Nov 2011 09:16:28 +0000 (09:16 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 16 Nov 2011 08:57:06 +0000 (08:57 +0000)]
commit by user andrea

12 years agoFixes a bug in NnAuto: printing the statistics triggered loading of
matitaweb [Tue, 15 Nov 2011 17:18:43 +0000 (17:18 +0000)]
Fixes a bug in NnAuto: printing the statistics triggered loading of
objects from the library into the environment.

12 years agocommit by user andrea
matitaweb [Tue, 15 Nov 2011 14:11:45 +0000 (14:11 +0000)]
commit by user andrea

12 years agoMatitaweb: Fixed typo which caused the compilation of matitadaemon.ml
matitaweb [Tue, 15 Nov 2011 11:46:25 +0000 (11:46 +0000)]
Matitaweb: Fixed typo which caused the compilation of matitadaemon.ml
to fail.

12 years agoMatitaweb: goto bottom can now be undone step by step and also reports errors
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.

12 years agonon-facts local candidates must be applied too in presence of
Andrea Asperti [Tue, 15 Nov 2011 08:25:59 +0000 (08:25 +0000)]
non-facts local candidates must be applied too in presence of
a trace

12 years agonon-facts local candidates must be applied too in presence of
Andrea Asperti [Tue, 15 Nov 2011 08:19:58 +0000 (08:19 +0000)]
non-facts local candidates must be applied too in presence of
a trace

13 years agofile names and description update
Ferruccio Guidi [Mon, 14 Nov 2011 17:22:11 +0000 (17:22 +0000)]
file names and description update

13 years ago- we proved that context-free reduction admits no one-step loops
Ferruccio Guidi [Mon, 14 Nov 2011 17:14:06 +0000 (17:14 +0000)]
- we proved that context-free reduction admits no one-step loops

13 years agoBug fix in inversion:
Wilmer Ricciotti [Mon, 14 Nov 2011 15:20:42 +0000 (15:20 +0000)]
Bug fix in inversion:
1) Dependent inversion only makes sense for JMeq
2) Removed test line fixing is_dependent = true

13 years agoAssert false is no longer true due to tooflex filtering.
Andrea Asperti [Mon, 14 Nov 2011 15:12:57 +0000 (15:12 +0000)]
Assert false is no longer true due to tooflex filtering.

13 years agoAdded dependent inversion (default case for jmeq)
Wilmer Ricciotti [Mon, 14 Nov 2011 15:09:07 +0000 (15:09 +0000)]
Added dependent inversion (default case for jmeq)

13 years agoToo flexible terms are pruned.
Andrea Asperti [Mon, 14 Nov 2011 07:58:46 +0000 (07:58 +0000)]
Too flexible terms are pruned.

13 years agocommit by user utente1
matitaweb [Fri, 11 Nov 2011 16:13:34 +0000 (16:13 +0000)]
commit by user utente1

13 years agocommit by user andrea
matitaweb [Fri, 11 Nov 2011 16:13:32 +0000 (16:13 +0000)]
commit by user andrea

13 years agoMatitaweb: fixes compilation errors and minor graphical problems.
matitaweb [Wed, 9 Nov 2011 14:48:55 +0000 (14:48 +0000)]
Matitaweb: fixes compilation errors and minor graphical problems.

13 years agoMatitaweb:
Wilmer Ricciotti [Wed, 9 Nov 2011 14:19:12 +0000 (14:19 +0000)]
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.

13 years agocommit by user andrea
matitaweb [Wed, 9 Nov 2011 10:13:47 +0000 (10:13 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 9 Nov 2011 09:34:13 +0000 (09:34 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 9 Nov 2011 08:44:23 +0000 (08:44 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Tue, 8 Nov 2011 16:54:31 +0000 (16:54 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 7 Nov 2011 14:55:17 +0000 (14:55 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 7 Nov 2011 14:43:20 +0000 (14:43 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Mon, 7 Nov 2011 09:16:20 +0000 (09:16 +0000)]
commit by user andrea

13 years agoRemoved some dead code.
Andrea Asperti [Mon, 7 Nov 2011 09:09:24 +0000 (09:09 +0000)]
Removed some dead code.

13 years agoNew management of justifications.
Andrea Asperti [Mon, 7 Nov 2011 09:02:42 +0000 (09:02 +0000)]
New management of justifications.
Justifications do not contain neither facts nor local hypothesis,
hence they must be computed by auto.

13 years agocommit by user andrea
matitaweb [Sat, 5 Nov 2011 16:56:56 +0000 (16:56 +0000)]
commit by user andrea

13 years ago- file names update
Ferruccio Guidi [Sat, 5 Nov 2011 15:54:03 +0000 (15:54 +0000)]
- file names update

13 years ago- lib: one lemma about equality was missing
Ferruccio Guidi [Fri, 4 Nov 2011 15:48:04 +0000 (15:48 +0000)]
- lib: one lemma about equality was missing
- lambda_delta: one inversion lemma closed

13 years ago- two discrimination lemmas
Ferruccio Guidi [Fri, 4 Nov 2011 11:59:52 +0000 (11:59 +0000)]
- two discrimination lemmas
- some decidability axioms (proof postponed)

13 years ago- contex-free normal forms started
Ferruccio Guidi [Thu, 3 Nov 2011 22:45:59 +0000 (22:45 +0000)]
- contex-free normal forms started
- final definition for context-sensitive reduction on local environments
- some refactoring

13 years ago1. we compare the expected branching with the actual one and
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 *)

13 years agoAt top level, we reindex the local equations for each cluster
Andrea Asperti [Thu, 3 Nov 2011 12:32:58 +0000 (12:32 +0000)]
At top level, we reindex the local equations for each cluster
(i.e. we assume each cluster shares a same context).

13 years agotrans_eq and sym_eq indexing restored. Apparently they are useful for several(?)
Claudio Sacerdoti Coen [Wed, 2 Nov 2011 12:57:20 +0000 (12:57 +0000)]
trans_eq and sym_eq indexing restored. Apparently they are useful for several(?)
theorems in CerCo (file positive.ma).

13 years agoMatitaweb: Added jquery.js (also used in some of the previous releases).
Wilmer Ricciotti [Wed, 2 Nov 2011 12:54:29 +0000 (12:54 +0000)]
Matitaweb: Added jquery.js (also used in some of the previous releases).

13 years agoMatitaweb:
Wilmer Ricciotti [Wed, 2 Nov 2011 12:52:37 +0000 (12:52 +0000)]
Matitaweb:
1) Added button to strip interpretations from the source
2) Fixed some UI bugs

13 years agoThe proof of append_cons used transitive_eq, not indexed.
Andrea Asperti [Wed, 2 Nov 2011 10:58:34 +0000 (10:58 +0000)]
The proof of append_cons used transitive_eq, not indexed.
If other cases will present we shall reindex it.

13 years agoDisabled printings.
Andrea Asperti [Wed, 2 Nov 2011 10:29:00 +0000 (10:29 +0000)]
Disabled printings.

13 years ago--Tre the expected branching with the actual one and
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

                            :his line, and those below, will be ignored--

M    ng_tactics/nnAuto.ml

13 years agocommit by user andrea
matitaweb [Fri, 28 Oct 2011 14:37:01 +0000 (14:37 +0000)]
commit by user andrea

13 years agoMatitaweb: added layout.js (currently manages resizing of UI).
Wilmer Ricciotti [Fri, 28 Oct 2011 13:49:57 +0000 (13:49 +0000)]
Matitaweb: added layout.js (currently manages resizing of UI).

13 years agoNew management of resulting subst in deep_eq: used to be malformed.
Andrea Asperti [Fri, 28 Oct 2011 10:59:33 +0000 (10:59 +0000)]
New management of resulting subst in deep_eq: used to be malformed.

13 years ago-applicative_case has been rewritten and simplified;
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.

13 years agoSome qed-
Andrea Asperti [Fri, 28 Oct 2011 09:34:23 +0000 (09:34 +0000)]
Some qed-

13 years agosome qed-
Andrea Asperti [Fri, 28 Oct 2011 09:33:44 +0000 (09:33 +0000)]
some qed-

13 years agoNew management of the resulting substitution in deep eq.
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.

13 years ago-pplicative_case has been rewritten and simplified;
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--

M    nnAuto.ml

13 years agoMatitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Wilmer Ricciotti [Thu, 27 Oct 2011 11:32:11 +0000 (11:32 +0000)]
Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping.
Added pretty-printing of unhandled NTacStatus.Error exceptions.

13 years agorefactoring ...
Ferruccio Guidi [Wed, 26 Oct 2011 08:31:53 +0000 (08:31 +0000)]
refactoring ...

13 years ago-- some renaming in basic_2
Ferruccio Guidi [Tue, 25 Oct 2011 12:27:34 +0000 (12:27 +0000)]
-- some renaming in basic_2

13 years agoold pr2_subst1 (Basic-1) closed!
Ferruccio Guidi [Tue, 25 Oct 2011 12:21:04 +0000 (12:21 +0000)]
old pr2_subst1 (Basic-1) closed!

13 years agoMatitaweb: first attempt at web UI for disambiguation.
Wilmer Ricciotti [Mon, 24 Oct 2011 16:40:58 +0000 (16:40 +0000)]
Matitaweb: first attempt at web UI for disambiguation.
Also includes a rather radical change in the way the graphical layout is
handled.

13 years agoNow it should compile :-)
Andrea Asperti [Fri, 21 Oct 2011 15:35:14 +0000 (15:35 +0000)]
Now it should compile :-)

13 years agoOptimization. Check removed.
Andrea Asperti [Fri, 21 Oct 2011 07:26:43 +0000 (07:26 +0000)]
Optimization. Check removed.

13 years agoDisabled debug.
Andrea Asperti [Fri, 21 Oct 2011 06:49:56 +0000 (06:49 +0000)]
Disabled debug.

13 years ago1. ported to camlp5
Andrea Asperti [Thu, 20 Oct 2011 16:16:24 +0000 (16:16 +0000)]
1. ported to camlp5
2. added a boolean to qed to governe indexing
   the syntax for disabling indexing is "qed-"

13 years agotypos
Andrea Asperti [Thu, 20 Oct 2011 16:13:06 +0000 (16:13 +0000)]
typos

13 years agoWe order alternatives according to the number of subgoals they open.
Andrea Asperti [Thu, 20 Oct 2011 15:54:22 +0000 (15:54 +0000)]
We order alternatives according to the number of subgoals they open.

13 years agoQED takes a boolean parameter governing indexing.
Andrea Asperti [Thu, 20 Oct 2011 15:49:59 +0000 (15:49 +0000)]
QED takes a boolean parameter governing indexing.
Syntax to avoid indexing is qed-

13 years agoAlternatives are ordered according to the number of subgoals
Andrea Asperti [Thu, 20 Oct 2011 15:47:59 +0000 (15:47 +0000)]
Alternatives are ordered according to the number of subgoals
they generate.

13 years agoJMeq lifted to work on Type[1].
Wilmer Ricciotti [Thu, 20 Oct 2011 13:58:55 +0000 (13:58 +0000)]
JMeq lifted to work on Type[1].

13 years agoRemoved some unneeded normalizations from the generation of discrimination
Wilmer Ricciotti [Thu, 20 Oct 2011 12:49:31 +0000 (12:49 +0000)]
Removed some unneeded normalizations from the generation of discrimination
principles (they had a bad effect on performance).

13 years agoMatitaweb: added preliminary support for interactive disambiguation.
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.

13 years agoMatitaweb: added a function MatitaAuthentication.get_users returning
matitaweb [Wed, 19 Oct 2011 15:58:38 +0000 (15:58 +0000)]
Matitaweb: added a function MatitaAuthentication.get_users returning
the list of the registered users.

13 years ago- the relocation properties of cpr are closed!
Ferruccio Guidi [Wed, 19 Oct 2011 15:57:18 +0000 (15:57 +0000)]
- the relocation properties of cpr are closed!
- the support for global references is started ...
- some refactoring.

13 years agocommit by user andrea
matitaweb [Wed, 19 Oct 2011 10:34:46 +0000 (10:34 +0000)]
commit by user andrea

13 years agocommit by user andrea
matitaweb [Wed, 19 Oct 2011 08:07:45 +0000 (08:07 +0000)]
commit by user andrea