]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

15 years agoadded notation for 'Vdash
Enrico Tassi [Thu, 15 Jan 2009 15:36:52 +0000 (15:36 +0000)]
added notation for 'Vdash

15 years agoif the user attempts to insert a duplicate coercions the system forbids it
Enrico Tassi [Thu, 15 Jan 2009 15:34:43 +0000 (15:34 +0000)]
if the user attempts to insert a duplicate coercions the system forbids it

15 years agounvariant also for coercions to funclass
Enrico Tassi [Thu, 15 Jan 2009 15:33:22 +0000 (15:33 +0000)]
unvariant also for coercions to funclass

15 years ago- name mangling changed, added __ to separate additional number
Enrico Tassi [Thu, 15 Jan 2009 15:32:52 +0000 (15:32 +0000)]
- name mangling changed, added __ to separate additional number
- composing a coercion with an identity does not affect the body, and a variant is generated

15 years agono more universe inconsistency printed to stderr
Enrico Tassi [Thu, 15 Jan 2009 15:31:25 +0000 (15:31 +0000)]
no more universe inconsistency printed to stderr

15 years agocoercions that are marked as variant are unfolded when inserted
Enrico Tassi [Thu, 15 Jan 2009 11:07:37 +0000 (11:07 +0000)]
coercions that are marked as variant are unfolded when inserted

15 years agoCoercions graph is printed between real types and not approximated ones
Enrico Tassi [Thu, 15 Jan 2009 11:05:44 +0000 (11:05 +0000)]
Coercions graph is printed between real types and not approximated ones

15 years agoo_continous_relations are really o_relation_pair... up to a bug of Matita
Claudio Sacerdoti Coen [Wed, 14 Jan 2009 23:07:58 +0000 (23:07 +0000)]
o_continous_relations are really o_relation_pair... up to a bug of Matita
(a meta left in the metasenv :-(

15 years agoo-basic_pairs are indeed examples of o-basic_topologies!
Claudio Sacerdoti Coen [Wed, 14 Jan 2009 00:01:55 +0000 (00:01 +0000)]
o-basic_pairs are indeed examples of o-basic_topologies!
some more work is required to prove the same for morphisms

15 years agomany changes regarding coercions:
Enrico Tassi [Tue, 13 Jan 2009 10:54:34 +0000 (10:54 +0000)]
many changes regarding coercions:
- new `prefer coercion foo` command to reorder the list of coercions associated with a src >-> tgt pair
- rewritten coercions undoing mechanism
- coercion composition fixed (generates more coercions)
- librarySync rewritten, procedures to generate derived lemmas (eliminators, invertion lemmas, ...) are hooks registerd by other modules that can thus live anywhere (also in tactics/ like the one for inversion)
- manual fixed to talk about the new command
- coercions graph is drawn together with a list of coercions that makes their precedence visible (and can be altered with the prefer coercion command)
- dump-moo fixed to print coercions
- removed `Coercion attribute in XML files (YOU NEED TO RECOMPILE)

15 years ago- Added new output in standard C.
Claudio Sacerdoti Coen [Tue, 13 Jan 2009 10:50:29 +0000 (10:50 +0000)]
- Added new output in standard C.

15 years agoSome work on o-algebras towards the proof that a and j are saturation/reduction
Claudio Sacerdoti Coen [Mon, 12 Jan 2009 23:49:29 +0000 (23:49 +0000)]
Some work on o-algebras towards the proof that a and j are saturation/reduction
operators.

15 years agoThe new coercion from SET to Type0 with higher priority really helps a lot:
Claudio Sacerdoti Coen [Thu, 8 Jan 2009 18:47:38 +0000 (18:47 +0000)]
The new coercion from SET to Type0 with higher priority really helps a lot:
almost all explicit occurrences of carr have been removed.

15 years agomore composites to make all happy!
Enrico Tassi [Thu, 8 Jan 2009 18:12:28 +0000 (18:12 +0000)]
more composites to make all happy!

15 years agoeq over SET1 and SET no longer used
Enrico Tassi [Thu, 8 Jan 2009 16:48:36 +0000 (16:48 +0000)]
eq over SET1 and SET no longer used

15 years agosome more if/fi conversion due to the new . binding
Enrico Tassi [Thu, 8 Jan 2009 12:05:34 +0000 (12:05 +0000)]
some more if/fi conversion due to the new . binding

15 years agounary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
Enrico Tassi [Thu, 8 Jan 2009 11:57:57 +0000 (11:57 +0000)]
unary_morphism_N : seoidN -> setoidN -> setoidN (was ... -> setoidN+1)
notation for . is now bound to fi instead of if (i.e. rewrites -> )

15 years agovirtuals for () removed and bound to 'o'
Enrico Tassi [Thu, 8 Jan 2009 09:47:46 +0000 (09:47 +0000)]
virtuals for () removed and bound to 'o'
memory changed, used similar symbols are presented first but not altering their original order

15 years agoJust a snapshot.
Claudio Sacerdoti Coen [Thu, 8 Jan 2009 09:08:09 +0000 (09:08 +0000)]
Just a snapshot.

15 years agocoercions reordering implemented
Enrico Tassi [Tue, 6 Jan 2009 18:19:28 +0000 (18:19 +0000)]
coercions reordering implemented

15 years agoupdated
Enrico Tassi [Tue, 6 Jan 2009 18:16:45 +0000 (18:16 +0000)]
updated

15 years agoMore work on concrete spaces.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 17:44:05 +0000 (17:44 +0000)]
More work on concrete spaces.

15 years agoSome work on concrete spaces.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 17:28:59 +0000 (17:28 +0000)]
Some work on concrete spaces.

15 years agoCool: only 8 universes in use.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 16:41:01 +0000 (16:41 +0000)]
Cool: only 8 universes in use.

15 years ago1) Some reorganization.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 16:20:00 +0000 (16:20 +0000)]
1) Some reorganization.
2) Funny: the proof that basic_topologies are an example of o_basic_topology
   is immediate.

15 years agoSome renaming to avoid confusion between saturations and o_saturations.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 15:16:49 +0000 (15:16 +0000)]
Some renaming to avoid confusion between saturations and o_saturations.

15 years agoFixing universe levels for saturations and (partially) basic_topologies.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 15:06:31 +0000 (15:06 +0000)]
Fixing universe levels for saturations and (partially) basic_topologies.

15 years agoThe functor from BP to OBP has been defined (but no property proved yet).
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 14:10:51 +0000 (14:10 +0000)]
The functor from BP to OBP has been defined (but no property proved yet).

15 years agoOk, even if not stated formally, now we know that the map from REL to OA is
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 13:58:06 +0000 (13:58 +0000)]
Ok, even if not stated formally, now we know that the map from REL to OA is
a functor!

15 years agoorelation_of_relation preserves equality and identities.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 13:13:23 +0000 (13:13 +0000)]
orelation_of_relation preserves equality and identities.

15 years agoBasic pairs restored; require renaming to use them together with o-basic_pairs.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 02:05:57 +0000 (02:05 +0000)]
Basic pairs restored; require renaming to use them together with o-basic_pairs.

15 years agoSome progress: everything works well now.
Claudio Sacerdoti Coen [Tue, 6 Jan 2009 01:50:28 +0000 (01:50 +0000)]
Some progress: everything works well now.