]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoCProp_i <= Type_i , Type_i <= CProp_i
Enrico Tassi [Tue, 15 Jul 2008 12:00:24 +0000 (12:00 +0000)]
CProp_i <= Type_i , Type_i <= CProp_i

16 years agomodels over N fixed
Enrico Tassi [Tue, 15 Jul 2008 10:16:06 +0000 (10:16 +0000)]
models over N fixed

16 years agonew q_function representation
Enrico Tassi [Tue, 15 Jul 2008 09:18:23 +0000 (09:18 +0000)]
new q_function representation

16 years agoremoved dummy comment
Enrico Tassi [Tue, 15 Jul 2008 09:09:30 +0000 (09:09 +0000)]
removed dummy comment

16 years agoUsing Prop conjuction on Props lowers the universes.
Enrico Tassi [Tue, 15 Jul 2008 09:08:15 +0000 (09:08 +0000)]
Using Prop conjuction on Props lowers the universes.
SigT instead of ExT

16 years agolambda-delta: we added the support for position indexes in global references
Ferruccio Guidi [Mon, 14 Jul 2008 20:17:22 +0000 (20:17 +0000)]
lambda-delta: we added the support for position indexes in global references
              we added a pretty printer for the intermediate language
librarian   : utime stamps now appear only in debug mode

16 years agoProcedural: we added the support for rendering definitions and axioms
Ferruccio Guidi [Mon, 14 Jul 2008 11:57:42 +0000 (11:57 +0000)]
Procedural: we added the support for rendering definitions and axioms

16 years agoProcedural: we added the support for theorem flavours and we fixed the handling ...
Ferruccio Guidi [Sun, 13 Jul 2008 15:02:49 +0000 (15:02 +0000)]
Procedural: we added the support for theorem flavours and we fixed the handling             of unexpected proof constructions

16 years agocicUtil : we added a context to is_sober to check for consistancy
Ferruccio Guidi [Sun, 13 Jul 2008 11:06:20 +0000 (11:06 +0000)]
cicUtil            : we added a context to is_sober to check for consistancy
                     of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
                     of the expected prod :)
acic2Procedural    : we added a consistancy check that was missing

16 years agoProcedural: bug fix in the procedural rendering of the abstraction
Ferruccio Guidi [Sat, 12 Jul 2008 22:17:46 +0000 (22:17 +0000)]
Procedural: bug fix in the procedural rendering of the abstraction

16 years agolibrarian: retrieval of buildable files speeded up a lot
Ferruccio Guidi [Sat, 12 Jul 2008 20:40:30 +0000 (20:40 +0000)]
librarian: retrieval of buildable files speeded up a lot
Procedural: some bug fixes
termContentPres.ml: syntax of let-in construction fixed
LAMBDA-TYPES: some improvements in the Makefile

16 years agoNew feature/bug fixed (hopefully): it is now possible to use fixed (term)
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:43:21 +0000 (11:43 +0000)]
New feature/bug fixed (hopefully): it is now possible to use fixed (term)
variables in fold bodies.
The notation for exists is now fully working as expected.

16 years agoNotation for existential partially fixed: it is now possible to write
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:17:17 +0000 (11:17 +0000)]
Notation for existential partially fixed: it is now possible to write
\exists a,b,c:T.P
(possibly omitting the type).
In any case, however, the type is got rid of during parsing.

16 years agoA very nice experiment using notation: we define the notation for natural
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 17:22:19 +0000 (17:22 +0000)]
A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).

16 years agoExists is no longer an ad-hoc notation hard-coded in the parser.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 16:49:18 +0000 (16:49 +0000)]
Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.

16 years agoAdded new ternary layout \infrule premises conclusion name.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 14:29:09 +0000 (14:29 +0000)]
Added new ternary layout \infrule premises conclusion name.
Very useful to render proof terms as trees.

16 years agovalue has a specification
Enrico Tassi [Thu, 10 Jul 2008 10:16:48 +0000 (10:16 +0000)]
value has a specification

16 years agoupdated changelog
Enrico Tassi [Thu, 10 Jul 2008 08:13:16 +0000 (08:13 +0000)]
updated changelog

16 years agomore work on dama
Enrico Tassi [Thu, 10 Jul 2008 08:00:45 +0000 (08:00 +0000)]
more work on dama

16 years agofixed regression in casting an argument to funclass, this incidentally leaded to...
Enrico Tassi [Thu, 10 Jul 2008 08:00:30 +0000 (08:00 +0000)]
fixed regression in casting an argument to funclass, this incidentally leaded to a single look_for_coercion_function

16 years agosome bug fixes
Ferruccio Guidi [Wed, 9 Jul 2008 18:24:46 +0000 (18:24 +0000)]
some bug fixes

16 years agobetter notation
Enrico Tassi [Wed, 9 Jul 2008 14:16:17 +0000 (14:16 +0000)]
better notation

16 years agominor fixes
Enrico Tassi [Wed, 9 Jul 2008 13:40:43 +0000 (13:40 +0000)]
minor fixes

16 years agoCProp hierarchy fixed:
Enrico Tassi [Wed, 9 Jul 2008 11:19:02 +0000 (11:19 +0000)]
CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel

Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency

16 years agotab -> ' '
Enrico Tassi [Wed, 9 Jul 2008 11:07:16 +0000 (11:07 +0000)]
tab -> '        '

16 years ago...
Enrico Tassi [Wed, 9 Jul 2008 10:55:55 +0000 (10:55 +0000)]
...

16 years agosimplified coercDb implementation with additional info about the position of
Enrico Tassi [Mon, 7 Jul 2008 21:01:17 +0000 (21:01 +0000)]
simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.

New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:

  C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z

where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps

16 years ago- we replaced a normalize with a whd in the classification algorithm
Ferruccio Guidi [Fri, 4 Jul 2008 18:46:29 +0000 (18:46 +0000)]
- we replaced a normalize with a whd in the classification algorithm
- we turned on the display of the inner types to debug drop/props.ma

16 years agoMore definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 15:31:22 +0000 (15:31 +0000)]
More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".

16 years ago- Procedural: bug fix in rendering the application: we must handle the
Ferruccio Guidi [Fri, 4 Jul 2008 12:03:19 +0000 (12:03 +0000)]
- Procedural: bug fix in rendering the application: we must handle the
              arguments that are inferrable but do not occur in the goal
- LAMBDA-TYPES: bug fix in Makefile: MAS was not computed correctly

16 years agoCompatibility finished.
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 11:57:33 +0000 (11:57 +0000)]
Compatibility finished.

16 years agoNice: cotransitivity proved.
Claudio Sacerdoti Coen [Fri, 4 Jul 2008 10:21:26 +0000 (10:21 +0000)]
Nice: cotransitivity proved.

16 years agoMore work.
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 21:54:34 +0000 (21:54 +0000)]
More work.

16 years agoFirst few lemmas. But I have some problems in making Matita accept
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 21:31:55 +0000 (21:31 +0000)]
First few lemmas. But I have some problems in making Matita accept
my constructor.

16 years agoFirst experiment in Padua about formal topologies.
Claudio Sacerdoti Coen [Thu, 3 Jul 2008 15:22:12 +0000 (15:22 +0000)]
First experiment in Padua about formal topologies.

16 years ago...snapshot
Enrico Tassi [Thu, 3 Jul 2008 14:20:35 +0000 (14:20 +0000)]
...snapshot

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