]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agoNew algorithm based on in-place modification of the graph.
Claudio Sacerdoti Coen [Thu, 12 Mar 2009 00:08:54 +0000 (00:08 +0000)]
New algorithm based on in-place modification of the graph.
Conjecture solved in the negative:

(CMM?)+ | (MM?C)+

cCw = Cw
-Cw = MCw
cMw = CMw
-MMw = -w
-MCw = MMCw
iw = w

15 years agomatitacLib: Gc.compact added after the compilation of mmas
Ferruccio Guidi [Wed, 11 Mar 2009 18:39:42 +0000 (18:39 +0000)]
matitacLib: Gc.compact added after the compilation of mmas
            Now LAMBDA-TYPES compiles in ~ 100m
Makefile: daily test of LAMBDA-TYPES re-enabled

15 years agoProcedural: id tactics are not counted, ie they are placeholders
Ferruccio Guidi [Wed, 11 Mar 2009 15:37:54 +0000 (15:37 +0000)]
Procedural: id tactics are not counted, ie they are placeholders
LAMBDA-TYPES: bugfix in depend +
              makefile entries for %.ma %.mma %.ma.opt %.mma.opt

15 years agobug fix + better obj flavour guessing via inner sorts
Ferruccio Guidi [Wed, 11 Mar 2009 13:43:20 +0000 (13:43 +0000)]
bug fix + better obj flavour guessing via inner sorts

15 years agothe level 1 reconstruction procedure is now in Procedural1
Ferruccio Guidi [Wed, 11 Mar 2009 13:20:57 +0000 (13:20 +0000)]
the level 1 reconstruction procedure is now in Procedural1
Procedural2 coming soon ....

15 years ago....
Ferruccio Guidi [Wed, 11 Mar 2009 12:31:32 +0000 (12:31 +0000)]
....

15 years agonew dependences
Ferruccio Guidi [Wed, 11 Mar 2009 12:07:19 +0000 (12:07 +0000)]
new dependences

15 years agounification hints with recursive calls do work!
Enrico Tassi [Wed, 11 Mar 2009 09:48:31 +0000 (09:48 +0000)]
unification hints with recursive calls do work!

15 years agoadded margin option to the pp
Enrico Tassi [Wed, 11 Mar 2009 09:48:14 +0000 (09:48 +0000)]
added margin option to the pp

15 years agomore examples
Enrico Tassi [Wed, 11 Mar 2009 09:47:54 +0000 (09:47 +0000)]
more examples

15 years agounificatiom hints with premises
Enrico Tassi [Tue, 10 Mar 2009 21:07:46 +0000 (21:07 +0000)]
unificatiom hints with premises

15 years agoadded some commented debugging instructions :)
Ferruccio Guidi [Tue, 10 Mar 2009 20:16:58 +0000 (20:16 +0000)]
added some commented debugging instructions :)

15 years agounification hints almost ready
Enrico Tassi [Tue, 10 Mar 2009 17:51:12 +0000 (17:51 +0000)]
unification hints almost ready

15 years agonotation ++
Enrico Tassi [Tue, 10 Mar 2009 17:49:39 +0000 (17:49 +0000)]
notation ++

15 years agoA version of applyS with bounded iterations of given_clause (10+10).
Andrea Asperti [Tue, 10 Mar 2009 16:07:03 +0000 (16:07 +0000)]
A version of applyS with bounded iterations of given_clause (10+10).
Not sure it works on the full library.

15 years agoRemoved the context from the metasenv to avoid trivial typing errors (lists
Andrea Asperti [Tue, 10 Mar 2009 15:52:26 +0000 (15:52 +0000)]
Removed the context from the metasenv to avoid trivial typing errors (lists
with different lengths).

15 years ago...
Enrico Tassi [Mon, 9 Mar 2009 18:21:23 +0000 (18:21 +0000)]
...

15 years agoMinor improvements in pretty-printing.
Claudio Sacerdoti Coen [Fri, 6 Mar 2009 16:23:45 +0000 (16:23 +0000)]
Minor improvements in pretty-printing.

15 years agoNew version: only new nodes are normalized; moreover, reduction stops as soon
Claudio Sacerdoti Coen [Thu, 5 Mar 2009 11:47:13 +0000 (11:47 +0000)]
New version: only new nodes are normalized; moreover, reduction stops as soon
as the term becomes shorter.

15 years ago- fixed hint generation, more hints are generated
Enrico Tassi [Tue, 3 Mar 2009 20:16:35 +0000 (20:16 +0000)]
- fixed hint generation, more hints are generated
- fixpoint refinement added
- Appl [Meta _; ... ] handled correctly, no double Appl or Beta redex is
  generated (both in regular code and interators)

15 years ago...
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:37:33 +0000 (23:37 +0000)]
...

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:26 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:13 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:36:00 +0000 (23:36 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:46 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:31 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:16 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:35:02 +0000 (23:35 +0000)]
New version.

15 years agoNew version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:34:46 +0000 (23:34 +0000)]
New version.

15 years agoFirst version.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:34:30 +0000 (23:34 +0000)]
First version.

15 years agoOld algorithm moved to old to leave place to the new one.
Claudio Sacerdoti Coen [Mon, 2 Mar 2009 23:33:21 +0000 (23:33 +0000)]
Old algorithm moved to old to leave place to the new one.

15 years agocicInspect: node count fixed
Ferruccio Guidi [Mon, 2 Mar 2009 20:34:04 +0000 (20:34 +0000)]
cicInspect: node count fixed
proceduralTeX: bug fix
LAMBDA-TYPES/Legacy-2/preamble.ma: bug fix
character: updated

15 years agouri renaming and new nodes count
Ferruccio Guidi [Mon, 2 Mar 2009 12:39:33 +0000 (12:39 +0000)]
uri renaming and new nodes count

15 years agosome renaming to comply with new naming policy ...
Ferruccio Guidi [Mon, 2 Mar 2009 12:03:37 +0000 (12:03 +0000)]
some renaming to comply with new naming policy ...

15 years agocicInspect: now we can choose not to count the Cic.Implicit constructors
Ferruccio Guidi [Thu, 26 Feb 2009 21:15:13 +0000 (21:15 +0000)]
cicInspect: now we can choose not to count the Cic.Implicit constructors
proceduralTypes, proceduralOptimizer: we do not count the Cic.Implict nodes
proceduralTeX: bug fix

15 years agoProceduralTeX completed and tested on the terms given as examples in the paper about...
Ferruccio Guidi [Wed, 25 Feb 2009 20:54:13 +0000 (20:54 +0000)]
ProceduralTeX completed and tested on the terms given as examples in the paper about the procedural reconstruction

15 years ago...
Enrico Tassi [Wed, 25 Feb 2009 09:11:26 +0000 (09:11 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 24 Feb 2009 15:23:38 +0000 (15:23 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 24 Feb 2009 15:19:41 +0000 (15:19 +0000)]
...

15 years agoNew module for TeX rendering of procedural input/output
Ferruccio Guidi [Sat, 21 Feb 2009 22:19:18 +0000 (22:19 +0000)]
New module for TeX rendering of procedural input/output
Used in the papers about the procedural representation

15 years ago...
Enrico Tassi [Fri, 20 Feb 2009 10:08:20 +0000 (10:08 +0000)]
...

15 years ago...
Enrico Tassi [Fri, 20 Feb 2009 09:22:21 +0000 (09:22 +0000)]
...

15 years ago- Coq/preamble: missing alias added
Ferruccio Guidi [Tue, 17 Feb 2009 19:37:22 +0000 (19:37 +0000)]
- Coq/preamble: missing alias added
- nUri: head comment fixed
- Procedural: the cases tactic is now detected and generated
              but does not compile :))
- grafiteAstPp: output syntax of the cases tactic fixed
- grafiteParser: impovement in the code for the elim tactic

15 years agosome notational experiments
Enrico Tassi [Mon, 16 Feb 2009 16:27:36 +0000 (16:27 +0000)]
some notational experiments

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 19:46:21 +0000 (19:46 +0000)]
...

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 15:19:09 +0000 (15:19 +0000)]
...

15 years ago...
Enrico Tassi [Sun, 15 Feb 2009 14:58:52 +0000 (14:58 +0000)]
...

15 years agocommented some printings
Enrico Tassi [Sun, 15 Feb 2009 14:57:16 +0000 (14:57 +0000)]
commented some printings

15 years agominor changes to make the library compile after wilmers new exists.
Enrico Tassi [Sun, 15 Feb 2009 14:56:26 +0000 (14:56 +0000)]
minor changes to make the library compile after wilmers new exists.

15 years agoAxiomatization of real numbers (work in progress)
Wilmer Ricciotti [Fri, 13 Feb 2009 15:16:55 +0000 (15:16 +0000)]
Axiomatization of real numbers (work in progress)

15 years agoerrata corrige.
Andrea Asperti [Thu, 12 Feb 2009 17:44:39 +0000 (17:44 +0000)]
errata corrige.

15 years agoFixed a problem of lifting.
Andrea Asperti [Thu, 12 Feb 2009 11:38:54 +0000 (11:38 +0000)]
Fixed a problem of lifting.

15 years agosome work to refine objs
Enrico Tassi [Wed, 11 Feb 2009 16:27:33 +0000 (16:27 +0000)]
some work to refine objs

15 years ago...
Enrico Tassi [Wed, 11 Feb 2009 10:30:15 +0000 (10:30 +0000)]
...

15 years agob:action are now considered as m:maction and thus are expanded
Enrico Tassi [Mon, 9 Feb 2009 16:06:53 +0000 (16:06 +0000)]
b:action are now considered as m:maction and thus are expanded

15 years ago...
Enrico Tassi [Fri, 6 Feb 2009 17:56:27 +0000 (17:56 +0000)]
...

15 years ago...
Enrico Tassi [Thu, 5 Feb 2009 10:57:16 +0000 (10:57 +0000)]
...

15 years agoa non necessary but morally required change. The matched term in
Enrico Tassi [Thu, 5 Feb 2009 10:48:28 +0000 (10:48 +0000)]
a non necessary but morally required change. The matched term in
are_convertible is compared with test_eq_only=true (not really needed since
if it reduces to something it is a constructor an thus an application that already honors the test_eq_only=true check for arguments

15 years agosome work to speed up the system
Enrico Tassi [Tue, 3 Feb 2009 20:50:20 +0000 (20:50 +0000)]
some work to speed up the system

15 years agocase tactic first tries with a simple outtype and then with a more sofisticated one
Enrico Tassi [Tue, 3 Feb 2009 20:39:00 +0000 (20:39 +0000)]
case tactic first tries with a simple outtype and then with a more sofisticated one
only if necessary since refine time may be long

15 years ago...
Enrico Tassi [Mon, 2 Feb 2009 14:44:47 +0000 (14:44 +0000)]
...

15 years agoCicTypeChecker.typecheck now takes an additional parameter:
Enrico Tassi [Mon, 2 Feb 2009 13:28:08 +0000 (13:28 +0000)]
CicTypeChecker.typecheck now takes an additional parameter:
- trust:bool, set to false only by the proofChecker daemon, while
  the refiner (for example) passes true

15 years agoHmmm, going too low.
Claudio Sacerdoti Coen [Mon, 2 Feb 2009 09:10:54 +0000 (09:10 +0000)]
Hmmm, going too low.
We need a more abstract proof (see Theorem 5.15, page 157 old book).

15 years ago...
Claudio Sacerdoti Coen [Mon, 2 Feb 2009 08:25:32 +0000 (08:25 +0000)]
...

15 years agoTowards fullness.
Claudio Sacerdoti Coen [Sun, 1 Feb 2009 20:46:43 +0000 (20:46 +0000)]
Towards fullness.

15 years agoRenaming.
Claudio Sacerdoti Coen [Sun, 1 Feb 2009 18:19:44 +0000 (18:19 +0000)]
Renaming.

15 years agoRenaming.
Claudio Sacerdoti Coen [Sun, 1 Feb 2009 18:17:40 +0000 (18:17 +0000)]
Renaming.

15 years agofix convertibility in case of application test_eq_only is =true for
Enrico Tassi [Fri, 30 Jan 2009 14:51:27 +0000 (14:51 +0000)]
fix convertibility in case of application test_eq_only is =true for
arguments, since we dont know if reduction eventually moves them in
contravariant position

15 years agomore polishing
Enrico Tassi [Thu, 29 Jan 2009 13:00:42 +0000 (13:00 +0000)]
more polishing

15 years ago...
Enrico Tassi [Thu, 29 Jan 2009 11:48:31 +0000 (11:48 +0000)]
...

15 years agoapplication arguments are compared with test_eq_only=true
Enrico Tassi [Thu, 29 Jan 2009 11:20:49 +0000 (11:20 +0000)]
application arguments are compared with test_eq_only=true

15 years agosome work
Enrico Tassi [Wed, 28 Jan 2009 21:24:42 +0000 (21:24 +0000)]
some work

15 years ago...
Enrico Tassi [Wed, 28 Jan 2009 17:55:31 +0000 (17:55 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 28 Jan 2009 17:55:20 +0000 (17:55 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 28 Jan 2009 09:14:48 +0000 (09:14 +0000)]
...

15 years ago...
Enrico Tassi [Wed, 28 Jan 2009 09:11:42 +0000 (09:11 +0000)]
...

15 years agomaction, mpadded and mstyle added to documentation
Enrico Tassi [Tue, 27 Jan 2009 15:13:53 +0000 (15:13 +0000)]
maction, mpadded and mstyle added to documentation

15 years agominor fixes
Enrico Tassi [Mon, 26 Jan 2009 17:12:56 +0000 (17:12 +0000)]
minor fixes

15 years agomaction support added to notation, adopted for = AKA = \sub t
Enrico Tassi [Mon, 26 Jan 2009 17:12:38 +0000 (17:12 +0000)]
maction support added to notation, adopted for = AKA  = \sub t
deactivated the library/formal_topology directory since it is completely broken and outdated

15 years agomaction layout added to notation
Enrico Tassi [Mon, 26 Jan 2009 17:11:10 +0000 (17:11 +0000)]
maction layout added to notation

15 years agowe were generating a name for the main fix twice
Enrico Tassi [Mon, 26 Jan 2009 17:10:50 +0000 (17:10 +0000)]
we were generating a name for the main fix twice

15 years agoadded a number to identical error messages to ease tracing them
Enrico Tassi [Mon, 26 Jan 2009 17:10:31 +0000 (17:10 +0000)]
added a number to identical error messages to ease tracing them

15 years agoOEIS sequence identifier found for P(n)
Ferruccio Guidi [Fri, 23 Jan 2009 11:25:44 +0000 (11:25 +0000)]
OEIS sequence identifier found for P(n)

15 years agoTODO
Claudio Sacerdoti Coen [Thu, 22 Jan 2009 18:53:09 +0000 (18:53 +0000)]
TODO

15 years agosome minor fixes
Enrico Tassi [Wed, 21 Jan 2009 17:52:33 +0000 (17:52 +0000)]
some minor fixes

15 years agoa bit of work done while travelling to padova
Enrico Tassi [Wed, 21 Jan 2009 13:57:40 +0000 (13:57 +0000)]
a bit of work done while travelling to padova

15 years ago- new notation.ma file with local and common notation
Enrico Tassi [Mon, 19 Jan 2009 18:02:22 +0000 (18:02 +0000)]
- new notation.ma file with local and common notation
- o-bp have now a O as prefix, the same for o-cs
- BP_to_OBP proved to be a functor, not faitfull nor full (simply stated)

15 years ago...
Claudio Sacerdoti Coen [Mon, 19 Jan 2009 12:43:45 +0000 (12:43 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Mon, 19 Jan 2009 11:21:07 +0000 (11:21 +0000)]
...

15 years agoall pullbacks are attempted in sequence, removed many unfold
Enrico Tassi [Mon, 19 Jan 2009 09:56:34 +0000 (09:56 +0000)]
all pullbacks are attempted in sequence, removed many unfold

15 years agouniverse inconsistency fixed
Claudio Sacerdoti Coen [Sun, 18 Jan 2009 22:13:10 +0000 (22:13 +0000)]
universe inconsistency fixed

15 years agoSUBSETS_full up to universe inconsistency
Claudio Sacerdoti Coen [Sun, 18 Jan 2009 02:58:50 +0000 (02:58 +0000)]
SUBSETS_full up to universe inconsistency

15 years agofaithful
Claudio Sacerdoti Coen [Sat, 17 Jan 2009 20:10:36 +0000 (20:10 +0000)]
faithful

15 years agoCAT2
Claudio Sacerdoti Coen [Sat, 17 Jan 2009 19:36:45 +0000 (19:36 +0000)]
CAT2

15 years agoceommented out metasenv
Enrico Tassi [Fri, 16 Jan 2009 13:37:56 +0000 (13:37 +0000)]
ceommented out metasenv

15 years ago...
Enrico Tassi [Fri, 16 Jan 2009 13:28:08 +0000 (13:28 +0000)]
...

15 years agoSambin's result holds trivially since most of the fields of the objects of
Claudio Sacerdoti Coen [Fri, 16 Jan 2009 01:37:16 +0000 (01:37 +0000)]
Sambin's result holds trivially since most of the fields of the objects of
the two categories are definitionally equal!

15 years agobasic topologies are trivially o-basic topologies
Claudio Sacerdoti Coen [Fri, 16 Jan 2009 01:19:23 +0000 (01:19 +0000)]
basic topologies are trivially o-basic topologies
the same for their morphisms

15 years ago1. new coercion(s) from CPropi to CProp
Claudio Sacerdoti Coen [Fri, 16 Jan 2009 00:45:58 +0000 (00:45 +0000)]
1. new coercion(s) from CPropi to CProp
2. fixed notation for subsetS
3. coercions still have problems: the coercion from objs1 REL is not
   accepted because it is identified with the coercion from objs1 SET

15 years agothe new coercion behaviour (variants + composition with ID) and the new
Enrico Tassi [Thu, 15 Jan 2009 15:38:23 +0000 (15:38 +0000)]
the new coercion behaviour (variants + composition with ID) and the new
discipline of declaring hints for carrier of structures (setoids and categories) and no
other hints simplified many passages