]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years ago...
Enrico Tassi [Thu, 3 Jul 2008 08:00:54 +0000 (08:00 +0000)]
...

16 years agosome work
Enrico Tassi [Wed, 2 Jul 2008 21:43:55 +0000 (21:43 +0000)]
some work

16 years agosvn:ignore set on LambdaDelta-2
Ferruccio Guidi [Wed, 2 Jul 2008 17:54:41 +0000 (17:54 +0000)]
svn:ignore set on LambdaDelta-2

16 years ago- new tactic applyP for use in the *P*rocedural script reconstruction
Ferruccio Guidi [Wed, 2 Jul 2008 17:33:03 +0000 (17:33 +0000)]
- new tactic applyP for use in the *P*rocedural script reconstruction
- LAMBDA-TYPES: the mma files from the LambdaDelta section

16 years agoFixed a bug which prevented mutually recursive definitions of 3 or more
Wilmer Ricciotti [Wed, 2 Jul 2008 15:12:24 +0000 (15:12 +0000)]
Fixed a bug which prevented mutually recursive definitions of 3 or more
functions from being added to the library

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 15:05:26 +0000 (15:05 +0000)]
...

16 years agoreturn 1 in case of failure
Enrico Tassi [Wed, 2 Jul 2008 12:50:18 +0000 (12:50 +0000)]
return 1 in case of failure

16 years ago0.5.2
Enrico Tassi [Wed, 2 Jul 2008 12:14:48 +0000 (12:14 +0000)]
0.5.2

16 years ago0.5.2
Enrico Tassi [Wed, 2 Jul 2008 12:14:29 +0000 (12:14 +0000)]
0.5.2

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:32:37 +0000 (09:32 +0000)]
...

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:18:27 +0000 (09:18 +0000)]
...

16 years ago...
Enrico Tassi [Wed, 2 Jul 2008 09:18:21 +0000 (09:18 +0000)]
...

16 years agocalculation of the sort user to choose the rewriting principle fixed
Enrico Tassi [Wed, 2 Jul 2008 09:13:12 +0000 (09:13 +0000)]
calculation of the sort user to choose the rewriting principle fixed
(the one of the goal was used also to rewrite in an hypothesis)

16 years ago- lambda-delta: some speed up (not very much :) actually)
Ferruccio Guidi [Tue, 1 Jul 2008 18:21:22 +0000 (18:21 +0000)]
- lambda-delta: some speed up (not very much :) actually)
- LAMBDA-TYPES: bug fix in Makefile

16 years agoshifting done, merge attacked
Enrico Tassi [Tue, 1 Jul 2008 14:25:20 +0000 (14:25 +0000)]
shifting done, merge attacked

16 years agoshift almost done
Enrico Tassi [Tue, 1 Jul 2008 12:00:22 +0000 (12:00 +0000)]
shift almost done

16 years agonew specification
Enrico Tassi [Mon, 30 Jun 2008 22:50:55 +0000 (22:50 +0000)]
new specification

16 years agowe improved the data structures used in the translation to the intermediate
Ferruccio Guidi [Mon, 30 Jun 2008 19:34:06 +0000 (19:34 +0000)]
we improved the data structures used in the translation to the intermediate
language

16 years agosome more work on q
Enrico Tassi [Mon, 30 Jun 2008 18:54:26 +0000 (18:54 +0000)]
some more work on q

16 years agowe tranlate an Automath book in an itermediate format where:
Ferruccio Guidi [Mon, 30 Jun 2008 14:07:46 +0000 (14:07 +0000)]
we tranlate an Automath book in an itermediate format where:
- the local references are resolved as position indexes
- the global references are disambiguated
- the parameter applications are completed
For now the trnslation is slow because the involved data structures are
inefficient

16 years agosome more work to factorize out uninteresting parts of the proof...
Enrico Tassi [Sat, 28 Jun 2008 11:28:34 +0000 (11:28 +0000)]
some more work to factorize out uninteresting parts of the proof...
still to close the key lemma...

16 years agomore work to try to understand where the issue is
Enrico Tassi [Fri, 27 Jun 2008 19:11:42 +0000 (19:11 +0000)]
more work to try to understand where the issue is

16 years agolost in the wood
Enrico Tassi [Fri, 27 Jun 2008 16:32:24 +0000 (16:32 +0000)]
lost in the wood

16 years agomore work
Enrico Tassi [Thu, 26 Jun 2008 21:35:10 +0000 (21:35 +0000)]
more work

16 years agofew more steps
Enrico Tassi [Thu, 26 Jun 2008 20:48:25 +0000 (20:48 +0000)]
few more steps

16 years agomore work
Enrico Tassi [Thu, 26 Jun 2008 20:22:19 +0000 (20:22 +0000)]
more work

16 years agosome more work
Enrico Tassi [Thu, 26 Jun 2008 13:52:36 +0000 (13:52 +0000)]
some more work

16 years agomore work on q
Enrico Tassi [Thu, 26 Jun 2008 11:43:08 +0000 (11:43 +0000)]
more work on q

16 years agosome more work
Enrico Tassi [Wed, 25 Jun 2008 14:54:47 +0000 (14:54 +0000)]
some more work

16 years agobetter, reparsable, notation
Enrico Tassi [Wed, 25 Jun 2008 09:11:34 +0000 (09:11 +0000)]
better, reparsable, notation

16 years agoremoved <_,_> notation second interpretation for dependent pair, since it used
Enrico Tassi [Tue, 24 Jun 2008 18:48:31 +0000 (18:48 +0000)]
removed <_,_> notation second interpretation for dependent pair, since it used
to have an exponential slowdown on refinement of huge terms....

16 years agonotation factored, coercion commant taking terms and not only URI
Enrico Tassi [Tue, 24 Jun 2008 14:47:16 +0000 (14:47 +0000)]
notation factored, coercion commant taking terms and not only URI

16 years agomissing file added
Enrico Tassi [Tue, 24 Jun 2008 13:49:55 +0000 (13:49 +0000)]
missing file added

16 years agometaAut.xlate_item started
Ferruccio Guidi [Mon, 23 Jun 2008 21:04:44 +0000 (21:04 +0000)]
metaAut.xlate_item started

16 years agowe set the http daemon timeout to 15 minutes, which is the default timeout of wget...
Ferruccio Guidi [Mon, 23 Jun 2008 17:27:35 +0000 (17:27 +0000)]
we set the http daemon timeout to 15 minutes, which is the default timeout of   wget, because some proof terms are processed in more than 5 minutes.

16 years agomore work, but russell too slow
Enrico Tassi [Mon, 23 Jun 2008 16:11:47 +0000 (16:11 +0000)]
more work, but russell too slow

16 years agoadd \\ in front of tex macros
Enrico Tassi [Mon, 23 Jun 2008 15:06:12 +0000 (15:06 +0000)]
add \\ in front of tex macros

16 years agonotation support fixed to parentesize in a more sane way and
Enrico Tassi [Mon, 23 Jun 2008 13:49:50 +0000 (13:49 +0000)]
notation support fixed to parentesize in a more sane way and
andded two windows:
1) tex/utf8 table
2) terms grammar

16 years agostylesheet application moved after header send
Ferruccio Guidi [Mon, 23 Jun 2008 13:12:34 +0000 (13:12 +0000)]
stylesheet application moved after header send

16 years agoxxx
Enrico Tassi [Mon, 23 Jun 2008 07:42:40 +0000 (07:42 +0000)]
xxx

16 years ago- grafiteParser.ml: the callback invocation was displaced
Ferruccio Guidi [Sun, 22 Jun 2008 15:13:14 +0000 (15:13 +0000)]
- grafiteParser.ml: the callback invocation was displaced
- cicNotationPres.ml: hack to have more brackets because
  (forall .. \to ..) was rendered without brackets. FIXME!
- LAMBDA-TYPES: improved Makefile

16 years agoleft -> right
Enrico Tassi [Fri, 20 Jun 2008 18:36:39 +0000 (18:36 +0000)]
left -> right

16 years agoFixed bugs in the documentation of notation.
Claudio Sacerdoti Coen [Fri, 20 Jun 2008 16:39:32 +0000 (16:39 +0000)]
Fixed bugs in the documentation of notation.
All TODOs left I do not know how to fill.

16 years agoMore documentation for notation.
Claudio Sacerdoti Coen [Fri, 20 Jun 2008 16:19:16 +0000 (16:19 +0000)]
More documentation for notation.

16 years agoFurther documentation for notation.
Claudio Sacerdoti Coen [Fri, 20 Jun 2008 12:02:13 +0000 (12:02 +0000)]
Further documentation for notation.

16 years ago- partial implementation of pattern for case documented
Claudio Sacerdoti Coen [Fri, 20 Jun 2008 11:04:18 +0000 (11:04 +0000)]
- partial implementation of pattern for case documented
- notation partially documented
- omitting the precedence level in a notation declaration is no longer allowed

16 years agofixed core notation
Enrico Tassi [Thu, 19 Jun 2008 17:40:02 +0000 (17:40 +0000)]
fixed core notation

16 years agonotation fixed to be NON associative by default
Enrico Tassi [Thu, 19 Jun 2008 17:39:53 +0000 (17:39 +0000)]
notation fixed to be NON associative by default

16 years ago1. bug fixed in generalize_pattern: a lazy const_tac should have been
Claudio Sacerdoti Coen [Thu, 19 Jun 2008 16:34:41 +0000 (16:34 +0000)]
1. bug fixed in generalize_pattern: a lazy const_tac should have been
   relocated. The interesting case is

   generalize in match a in \vdash %

   where a occurs in the goal under at least one binder

2. pattern for cases partially implemented. It is now possible to perform
   a case on the hypotheses as long as the conclusion and hypothesis patterns
   are trivial (i.e. %)

16 years ago- notation fixed according to the new stricter semantics
Claudio Sacerdoti Coen [Thu, 19 Jun 2008 16:32:36 +0000 (16:32 +0000)]
- notation fixed according to the new stricter semantics
- generalize no longer required before case

16 years ago- Procedural: we now check that an eliminator opens as many goals as the ...
Ferruccio Guidi [Thu, 19 Jun 2008 12:15:38 +0000 (12:15 +0000)]
- Procedural: we now check that an eliminator opens as many goals as the                      constructors of the eliminated type
              So nat_double_ind is not an eliminator for Nat :)
- Base-2    : now compiles correctly because we fixed the preamble :)

16 years agonotation on steroids: 'term 40 x' is a valid variable name in notation and
Enrico Tassi [Thu, 19 Jun 2008 11:18:58 +0000 (11:18 +0000)]
notation on steroids: 'term 40 x' is a valid variable name in notation and
places 'x' at term level 40 even if the notation is placed elsewhere

16 years agointerpretation documented
Claudio Sacerdoti Coen [Wed, 18 Jun 2008 22:55:35 +0000 (22:55 +0000)]
interpretation documented

16 years agoinitial support for notation that specifies the precedence of term variables, that...
Enrico Tassi [Wed, 18 Jun 2008 15:03:32 +0000 (15:03 +0000)]
initial support for notation that specifies the precedence of term variables, that allows to omit many useless parenthesis

16 years agoremoved unused variable
Enrico Tassi [Wed, 18 Jun 2008 15:02:53 +0000 (15:02 +0000)]
removed unused variable

16 years agosome work on Q
Enrico Tassi [Wed, 18 Jun 2008 08:07:53 +0000 (08:07 +0000)]
some work on Q

16 years agogeneral reorganization and first (unconditional) proof of lebesgue over naturals
Enrico Tassi [Tue, 17 Jun 2008 14:30:28 +0000 (14:30 +0000)]
general reorganization and first (unconditional) proof of lebesgue over naturals

16 years agoreordering of lexicon status partially avoided to make it sure
Enrico Tassi [Tue, 17 Jun 2008 14:18:12 +0000 (14:18 +0000)]
reordering of lexicon status partially avoided to make it sure
that interpretations are not moved around. I still argue that an alias can be
removed from the back of an interpretation, no idea how this would interfere with CSC recent patch

16 years agotransformation from automath to intermediate language started
Ferruccio Guidi [Mon, 16 Jun 2008 17:19:52 +0000 (17:19 +0000)]
transformation from automath to intermediate language started

16 years agoDedekind sigma completeness for the natural numbers.
Enrico Tassi [Mon, 16 Jun 2008 15:24:57 +0000 (15:24 +0000)]
Dedekind sigma completeness for the natural numbers.

16 years agotypo
Enrico Tassi [Mon, 16 Jun 2008 12:42:38 +0000 (12:42 +0000)]
typo

16 years agosome notation added with a bit PITA
Enrico Tassi [Fri, 13 Jun 2008 15:53:27 +0000 (15:53 +0000)]
some notation added with a bit PITA

16 years agofinal relevance check
Wilmer Ricciotti [Fri, 13 Jun 2008 12:59:14 +0000 (12:59 +0000)]
final relevance check

16 years agocopyright information added in the grundlagen text
Ferruccio Guidi [Fri, 13 Jun 2008 12:57:50 +0000 (12:57 +0000)]
copyright information added in the grundlagen text

16 years agowhen -debug do not catch
Enrico Tassi [Fri, 13 Jun 2008 12:02:28 +0000 (12:02 +0000)]
when -debug do not catch

16 years agowhen -debug do not catch
Enrico Tassi [Fri, 13 Jun 2008 12:02:10 +0000 (12:02 +0000)]
when -debug do not catch

16 years agoreplace assert false with AssertFailure
Enrico Tassi [Fri, 13 Jun 2008 12:01:37 +0000 (12:01 +0000)]
replace assert false with AssertFailure

16 years agoInitial version of the Helena Checker
Ferruccio Guidi [Fri, 13 Jun 2008 11:47:41 +0000 (11:47 +0000)]
Initial version of the Helena Checker
- For now just parses an automath book (automath grammar by F. Wiedijg)
  the grundlagen is provided as (the only existing) example
- In the future will convert an automath book to a lambda-delta environment
  several lambda-delta extensions will be supported

16 years agoNew lemma
Claudio Sacerdoti Coen [Fri, 13 Jun 2008 09:07:16 +0000 (09:07 +0000)]
New lemma
theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

16 years agomore notation
Enrico Tassi [Fri, 13 Jun 2008 07:14:52 +0000 (07:14 +0000)]
more notation

16 years ago...
Enrico Tassi [Fri, 13 Jun 2008 07:14:40 +0000 (07:14 +0000)]
...

16 years agoprint the name not found in the env
Enrico Tassi [Fri, 13 Jun 2008 07:14:30 +0000 (07:14 +0000)]
print the name not found in the env

16 years agoTesting some performance tricks by caching the list of the first n primes and
Enrico Tassi [Thu, 12 Jun 2008 15:52:34 +0000 (15:52 +0000)]
Testing some performance tricks by caching the list of the first n primes and
showing that they are good either with nth_prime (sloooooooooowww) or with
sieve (slooooow and not proved correct yet). With sieve we are currently able
to verify the list of the first 103 primes in a sort of reasonable time.
The 103rd prime is only 593 :-(

16 years agobetter names in a lemma to increase readability
Enrico Tassi [Thu, 12 Jun 2008 08:53:45 +0000 (08:53 +0000)]
better names in a lemma to increase readability

16 years agofixed some regressions
Enrico Tassi [Thu, 12 Jun 2008 08:40:06 +0000 (08:40 +0000)]
fixed some regressions

16 years agoNew, much faster implementation of factorize.
Claudio Sacerdoti Coen [Wed, 11 Jun 2008 18:00:20 +0000 (18:00 +0000)]
New, much faster implementation of factorize.

16 years agogran casino
Enrico Tassi [Wed, 11 Jun 2008 16:58:16 +0000 (16:58 +0000)]
gran casino

16 years agometa not considered before in outtype
Enrico Tassi [Wed, 11 Jun 2008 09:24:08 +0000 (09:24 +0000)]
meta not considered before in outtype

16 years agobla bla bla
Enrico Tassi [Tue, 10 Jun 2008 15:58:54 +0000 (15:58 +0000)]
bla bla bla

16 years agorelevance check for Match
Wilmer Ricciotti [Tue, 10 Jun 2008 15:32:22 +0000 (15:32 +0000)]
relevance check for Match

16 years agoinitial qork for models
Enrico Tassi [Tue, 10 Jun 2008 13:26:13 +0000 (13:26 +0000)]
initial qork for models

16 years agoAdded check of relevance lists for inductive types/constructors and
Wilmer Ricciotti [Tue, 10 Jun 2008 13:15:21 +0000 (13:15 +0000)]
Added check of relevance lists for inductive types/constructors and
fixpoint definitions.

16 years agolebesgue proved
Enrico Tassi [Tue, 10 Jun 2008 11:23:59 +0000 (11:23 +0000)]
lebesgue proved

16 years agosnapshot
Enrico Tassi [Tue, 10 Jun 2008 07:24:46 +0000 (07:24 +0000)]
snapshot

16 years agoMost of the time, URIs can now be replaced with identifiers in "interpretation".
Claudio Sacerdoti Coen [Mon, 9 Jun 2008 20:19:41 +0000 (20:19 +0000)]
Most of the time, URIs can now be replaced with identifiers in "interpretation".
Warning: identifiers are mapped to URIs according to the last declared
alias.

16 years agoIt is now possible to use identifiers in place of URI in "interpreation".
Claudio Sacerdoti Coen [Mon, 9 Jun 2008 20:17:20 +0000 (20:17 +0000)]
It is now possible to use identifiers in place of URI in "interpreation".
The identifier is mapped to an URI according to the last declared alias.

16 years agoReverting to the previous version some files which weren't intended to be
Wilmer Ricciotti [Mon, 9 Jun 2008 16:12:10 +0000 (16:12 +0000)]
Reverting to the previous version some files which weren't intended to be
changed.

16 years agomore proof irrelevance
Wilmer Ricciotti [Mon, 9 Jun 2008 16:02:24 +0000 (16:02 +0000)]
more proof irrelevance

16 years agoinitial work on lebesque
Enrico Tassi [Mon, 9 Jun 2008 14:11:17 +0000 (14:11 +0000)]
initial work on lebesque

16 years agoexhaustivity completed
Enrico Tassi [Mon, 9 Jun 2008 10:24:09 +0000 (10:24 +0000)]
exhaustivity completed

16 years agoexhaustivity, some work
Enrico Tassi [Mon, 9 Jun 2008 08:24:27 +0000 (08:24 +0000)]
exhaustivity, some work

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 18:48:45 +0000 (18:48 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 18:20:20 +0000 (18:20 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:56:36 +0000 (17:56 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:42:05 +0000 (17:42 +0000)]
generalize no more required before elim

16 years agogeneralize no more required by elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:14:43 +0000 (17:14 +0000)]
generalize no more required by elim

16 years agoGeneralize no more required for elim.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:12:43 +0000 (17:12 +0000)]
Generalize no more required for elim.

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:06:02 +0000 (17:06 +0000)]
generalize no more required before elim

16 years agogeneralize no more useful for elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 14:08:51 +0000 (14:08 +0000)]
generalize no more useful for elim

16 years agoBug fixed: wrong default pattern for generalize.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 14:00:37 +0000 (14:00 +0000)]
Bug fixed: wrong default pattern for generalize.