]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agocommit by user andrea
matitaweb [Tue, 6 Mar 2012 11:37:20 +0000 (11:37 +0000)]
commit by user andrea

12 years ago- lambda_delta: "conversion" and "equivalence" components started
Ferruccio Guidi [Sun, 4 Mar 2012 19:23:00 +0000 (19:23 +0000)]
- lambda_delta: "conversion" and "equivalence" components started
- formal_topology: porting to lib started. cprop_connectives compiles!

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 17:42:35 +0000 (17:42 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 17:07:30 +0000 (17:07 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 16:57:10 +0000 (16:57 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 15:25:37 +0000 (15:25 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 15:02:54 +0000 (15:02 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Fri, 2 Mar 2012 09:42:54 +0000 (09:42 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 09:42:52 +0000 (09:42 +0000)]
commit by user andrea

12 years agoSplitted chapter 7
matitaweb [Fri, 2 Mar 2012 09:02:13 +0000 (09:02 +0000)]
Splitted chapter 7

12 years agocommit by user andrea
matitaweb [Fri, 2 Mar 2012 08:49:27 +0000 (08:49 +0000)]
commit by user andrea

12 years agomissing files in the former commit :(
Ferruccio Guidi [Thu, 1 Mar 2012 21:01:30 +0000 (21:01 +0000)]
missing files in the former commit :(

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 17:52:50 +0000 (17:52 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 16:38:03 +0000 (16:38 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Thu, 1 Mar 2012 13:00:50 +0000 (13:00 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 12:26:57 +0000 (12:26 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 11:54:56 +0000 (11:54 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 11:31:22 +0000 (11:31 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Wed, 29 Feb 2012 10:45:22 +0000 (10:45 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:59:14 +0000 (13:59 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:55:24 +0000 (13:55 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:17:46 +0000 (13:17 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 13:11:17 +0000 (13:11 +0000)]
commit by user andrea

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 09:29:28 +0000 (09:29 +0000)]
commit by user andrea

12 years agocommit by user utente2
matitaweb [Tue, 28 Feb 2012 08:23:15 +0000 (08:23 +0000)]
commit by user utente2

12 years agocommit by user andrea
matitaweb [Tue, 28 Feb 2012 08:23:11 +0000 (08:23 +0000)]
commit by user andrea

12 years agosome additions to Basic_2
Ferruccio Guidi [Mon, 27 Feb 2012 21:46:51 +0000 (21:46 +0000)]
some additions to Basic_2

12 years ago- property S6 of stronfly normalizing terms proved
Ferruccio Guidi [Mon, 27 Feb 2012 21:43:36 +0000 (21:43 +0000)]
- property S6 of stronfly normalizing terms proved
- more properties concerning context sensitive computation

12 years agosite update
Ferruccio Guidi [Fri, 24 Feb 2012 18:21:09 +0000 (18:21 +0000)]
site update

12 years ago- we added a web page (Apps_2) for the checked applications of Basic_2
Ferruccio Guidi [Fri, 24 Feb 2012 16:27:56 +0000 (16:27 +0000)]
- we added a web page (Apps_2) for the checked applications of Basic_2
- we added some files to Basic_2
- we improved the Makefiles

12 years ago- "functional" component moved to Apps_2
Ferruccio Guidi [Fri, 24 Feb 2012 12:53:09 +0000 (12:53 +0000)]
- "functional" component moved to Apps_2
- property S5 of the candidates of reducibility almost proved ...

12 years agocommit by user andrea
matitaweb [Thu, 23 Feb 2012 10:46:38 +0000 (10:46 +0000)]
commit by user andrea

12 years agorefiner porting from matita 1.
Wilmer Ricciotti [Thu, 23 Feb 2012 09:48:07 +0000 (09:48 +0000)]
refiner porting from matita 1.

12 years agoIntegrations
matitaweb [Wed, 22 Feb 2012 12:31:42 +0000 (12:31 +0000)]
Integrations

12 years agoComplete outline. Raw scripts.
matitaweb [Wed, 22 Feb 2012 09:28:17 +0000 (09:28 +0000)]
Complete outline. Raw scripts.

12 years ago- more properties on strongly normalizing terms ...
Ferruccio Guidi [Tue, 21 Feb 2012 18:30:32 +0000 (18:30 +0000)]
- more properties on strongly normalizing terms ...

12 years ago- site update
Ferruccio Guidi [Tue, 21 Feb 2012 10:37:41 +0000 (10:37 +0000)]
- site update

12 years agoadditions to Basic_2 ...
Ferruccio Guidi [Mon, 20 Feb 2012 19:11:10 +0000 (19:11 +0000)]
additions to Basic_2 ...

12 years agoinitial properies of the "same top term constructor" predicate
Ferruccio Guidi [Mon, 20 Feb 2012 18:59:54 +0000 (18:59 +0000)]
initial properies of the "same top term constructor" predicate

12 years agomore results on strongly normalizing terms
Ferruccio Guidi [Sat, 18 Feb 2012 19:16:56 +0000 (19:16 +0000)]
more results on strongly normalizing terms

12 years agoadditions to Basic_2
Ferruccio Guidi [Tue, 14 Feb 2012 20:16:38 +0000 (20:16 +0000)]
additions to Basic_2

12 years ago- more properties on strongly normalizing terms
Ferruccio Guidi [Tue, 14 Feb 2012 20:07:50 +0000 (20:07 +0000)]
- more properties on strongly normalizing terms
- bugfix in Basic_1 annotations

12 years agoadditions to Basic_2
Ferruccio Guidi [Sat, 11 Feb 2012 19:50:31 +0000 (19:50 +0000)]
additions to Basic_2

12 years ago- strong normalization of abbreviation proved
Ferruccio Guidi [Sat, 11 Feb 2012 19:48:08 +0000 (19:48 +0000)]
- strong normalization of abbreviation proved
- bug fix in the generation lemma for abbreviationof context=sensitive parallel reduction

12 years ago- design table for Basic_2
Ferruccio Guidi [Thu, 9 Feb 2012 19:51:29 +0000 (19:51 +0000)]
- design table for Basic_2
- summary table for Basic_2 and Ground_2
- some additions to the Basic_2 file table
- some new cell styles for xhtbl
- syntax cor comments added to xhtbl
- some improvements in the Makefiles

12 years ago- first properties of strongly normalizing terms
Ferruccio Guidi [Thu, 9 Feb 2012 19:30:41 +0000 (19:30 +0000)]
- first properties of strongly normalizing terms
- contex-sensitive normal forms
- context-sensitive parallel computation of terms

12 years ago- one file and three lemmas added to Basic 2
Ferruccio Guidi [Thu, 2 Feb 2012 18:43:22 +0000 (18:43 +0000)]
- one file and three lemmas added to Basic 2
- bugfix in Makefile

12 years ago- three lemmas on context sensitive parallel reduction closed
Ferruccio Guidi [Thu, 2 Feb 2012 18:29:52 +0000 (18:29 +0000)]
- three lemmas on context sensitive parallel reduction closed

12 years ago- notation fix for reducible and normal forms
Ferruccio Guidi [Wed, 1 Feb 2012 16:19:30 +0000 (16:19 +0000)]
- notation fix for reducible and normal forms
- some refactoring
- improved Makefile produces a table with numerical summary

12 years agothe Basic_2 page was not regenerated ...
Ferruccio Guidi [Wed, 1 Feb 2012 15:53:33 +0000 (15:53 +0000)]
the Basic_2 page was not regenerated ...

12 years agowe added summary and timeline to the Basic_2 page
Ferruccio Guidi [Wed, 1 Feb 2012 15:49:09 +0000 (15:49 +0000)]
we added summary and timeline to the Basic_2 page

12 years agoNotation for destructuring let-in for triples fixed.
Claudio Sacerdoti Coen [Tue, 31 Jan 2012 10:09:05 +0000 (10:09 +0000)]
Notation for destructuring let-in for triples fixed.

12 years ago- transitivity of lenv refinement for atomic arity asignment proved! ...
Ferruccio Guidi [Sun, 29 Jan 2012 16:05:55 +0000 (16:05 +0000)]
- transitivity of lenv refinement for atomic arity asignment proved! ...
- results on context-free normal forms refacored
- some annotation added

12 years agomore files added to Basic_2
Ferruccio Guidi [Sun, 29 Jan 2012 15:59:04 +0000 (15:59 +0000)]
more files added to Basic_2

12 years agosupport for abstract candidates of reducibility closed! ...
Ferruccio Guidi [Fri, 27 Jan 2012 21:01:01 +0000 (21:01 +0000)]
support for abstract candidates of reducibility closed! ...

12 years agomore files added to Basic_2
Ferruccio Guidi [Fri, 27 Jan 2012 20:54:52 +0000 (20:54 +0000)]
more files added to Basic_2

12 years agoFixes a bug in is_flexible (when checking a meta in subst, we did a recursive
Wilmer Ricciotti [Fri, 27 Jan 2012 14:31:20 +0000 (14:31 +0000)]
Fixes a bug in is_flexible (when checking a meta in subst, we did a recursive
call on its body without applying the local context, resulting in various
assertion failures).

12 years agoBetter error messages.
Claudio Sacerdoti Coen [Fri, 27 Jan 2012 14:25:42 +0000 (14:25 +0000)]
Better error messages.

12 years ago- one file added to Basic_2
Ferruccio Guidi [Thu, 26 Jan 2012 17:03:11 +0000 (17:03 +0000)]
- one file added to Basic_2

12 years ago- main lemmas about abstract reducibility candidates closed
Ferruccio Guidi [Thu, 26 Jan 2012 16:48:05 +0000 (16:48 +0000)]
- main lemmas about abstract reducibility candidates closed
- notation updated (and one bug solved)
- Makefile: stats display improved

12 years agoInversion principles generation falls back to cases tactic when elim is not
Wilmer Ricciotti [Mon, 23 Jan 2012 13:47:33 +0000 (13:47 +0000)]
Inversion principles generation falls back to cases tactic when elim is not
available.

12 years agobig fixin the structure of Basic_2
Ferruccio Guidi [Sat, 21 Jan 2012 21:28:26 +0000 (21:28 +0000)]
big fixin the structure of Basic_2

12 years agomore files to Basic_2
Ferruccio Guidi [Sat, 21 Jan 2012 21:16:02 +0000 (21:16 +0000)]
more files to Basic_2

12 years ago- main proof for strong normalization closed! ...
Ferruccio Guidi [Sat, 21 Jan 2012 21:05:57 +0000 (21:05 +0000)]
- main proof for strong normalization closed! ...
- bug fix in lenv refinement for abstract candidates of reducibility (lsubc)
- lenv refinement for atomic arity assignment defined (lsuba) and relation
with lsubc proved

12 years agoclosure property S4 added to abstract candidates of reducibility ...
Ferruccio Guidi [Thu, 19 Jan 2012 16:10:12 +0000 (16:10 +0000)]
closure property S4 added to abstract candidates of reducibility ...

12 years agothe support for candidates of reducibility continues ...
Ferruccio Guidi [Mon, 16 Jan 2012 12:09:42 +0000 (12:09 +0000)]
the support for candidates of reducibility continues ...

12 years agosome additionsand refactoring in Basic_2
Ferruccio Guidi [Mon, 16 Jan 2012 12:06:47 +0000 (12:06 +0000)]
some additionsand refactoring in Basic_2

12 years agomore file names added to Basic_2
Ferruccio Guidi [Fri, 13 Jan 2012 15:44:30 +0000 (15:44 +0000)]
more file names added to Basic_2

12 years ago- the development of abstract reducibility candidates continues ...
Ferruccio Guidi [Fri, 13 Jan 2012 15:27:13 +0000 (15:27 +0000)]
- the development of abstract reducibility candidates continues ...
- some annotations added

12 years agoImproves the presentation of hypotheses in the goal pane.
Wilmer Ricciotti [Thu, 12 Jan 2012 12:03:29 +0000 (12:03 +0000)]
Improves the presentation of hypotheses in the goal pane.

12 years agoFixes r11788 (partial, thus broken commit).
Wilmer Ricciotti [Wed, 11 Jan 2012 10:45:07 +0000 (10:45 +0000)]
Fixes r11788 (partial, thus broken commit).

12 years agounpatched version for the new CamplP5
Ferruccio Guidi [Tue, 10 Jan 2012 20:42:17 +0000 (20:42 +0000)]
unpatched version for the new CamplP5

12 years agopatched version for old CamlP5
Ferruccio Guidi [Tue, 10 Jan 2012 20:31:44 +0000 (20:31 +0000)]
patched version for old CamlP5

12 years agoBugfix: NCicUnification.could_reduce now performs whd in the applied fixpoint
Wilmer Ricciotti [Tue, 10 Jan 2012 14:28:55 +0000 (14:28 +0000)]
Bugfix: NCicUnification.could_reduce now performs whd in the applied fixpoint
case, to prevent the recursive call from raising assert failure.

12 years agoA complete snapshot for re
Andrea Asperti [Tue, 10 Jan 2012 08:31:46 +0000 (08:31 +0000)]
A complete snapshot for re

12 years agomore characters shortcuts
Ferruccio Guidi [Sun, 8 Jan 2012 15:52:10 +0000 (15:52 +0000)]
more characters shortcuts

12 years agoBasic_2: restyling and more notation
Ferruccio Guidi [Sun, 8 Jan 2012 15:50:57 +0000 (15:50 +0000)]
Basic_2: restyling and more notation

12 years ago- notation restyling ...
Ferruccio Guidi [Sun, 8 Jan 2012 15:01:27 +0000 (15:01 +0000)]
- notation restyling ...

12 years agoBasic_2: - we addedsome files
Ferruccio Guidi [Sat, 7 Jan 2012 22:11:51 +0000 (22:11 +0000)]
Basic_2: - we addedsome files
         - we added some notation
 - we updated the table style

12 years agolambda_delta: global environments handling: redefined and first results
Ferruccio Guidi [Sat, 7 Jan 2012 19:29:46 +0000 (19:29 +0000)]
lambda_delta: global environments handling: redefined and first results
              rtm: first definitions
lib/arithmetics/nat: a missing lemma added
predefined_virtuals: we added circled numbers, circled letters and
other characters
depend, depend.opt: regenerated

12 years agothe support for reducibility candidates evolves ,,,,
Ferruccio Guidi [Wed, 4 Jan 2012 16:32:04 +0000 (16:32 +0000)]
the support for reducibility candidates evolves ,,,,

12 years agoComplete version
Andrea Asperti [Tue, 3 Jan 2012 16:16:45 +0000 (16:16 +0000)]
Complete version

12 years agomodified definition of memb
Andrea Asperti [Tue, 3 Jan 2012 16:00:01 +0000 (16:00 +0000)]
modified definition of memb

12 years agoreverse
Andrea Asperti [Tue, 3 Jan 2012 15:58:23 +0000 (15:58 +0000)]
reverse

12 years agomore properties of union
Andrea Asperti [Tue, 3 Jan 2012 15:57:18 +0000 (15:57 +0000)]
more properties of union

12 years agonoteq_to_eqnot
Andrea Asperti [Tue, 3 Jan 2012 15:55:51 +0000 (15:55 +0000)]
noteq_to_eqnot

12 years agonotation and dependences bug fix
Ferruccio Guidi [Mon, 26 Dec 2011 19:54:26 +0000 (19:54 +0000)]
notation and dependences bug fix

12 years agoBasic 2 page update
Ferruccio Guidi [Sun, 25 Dec 2011 19:52:48 +0000 (19:52 +0000)]
Basic 2 page update

12 years ago- support for candidates of reducibility continues ...
Ferruccio Guidi [Sun, 25 Dec 2011 19:47:29 +0000 (19:47 +0000)]
- support for candidates of reducibility continues ...
- change in the notation of relatiional relocation and local env.
slicing, to allow more usual notation for functional relocation (not
working yet)

12 years agoBasic_2 update ...
Ferruccio Guidi [Tue, 20 Dec 2011 14:33:42 +0000 (14:33 +0000)]
Basic_2 update ...

12 years ago- the definition of the framework for strong normalization continues ...
Ferruccio Guidi [Tue, 20 Dec 2011 14:29:27 +0000 (14:29 +0000)]
- the definition of the framework for strong normalization continues ...
- functional version of relocation and core substitution implemented
- standard arithmetics library updated

12 years agoIn case paramodulation fails we apply unit equalities.
Andrea Asperti [Fri, 16 Dec 2011 16:36:56 +0000 (16:36 +0000)]
In case paramodulation fails we apply unit equalities.

12 years agoSplitted DeqSets in their own file. Notation for memb to hide the type.
Andrea Asperti [Thu, 15 Dec 2011 15:22:19 +0000 (15:22 +0000)]
Splitted DeqSets in their own file. Notation for memb to hide the type.

12 years agoHints sui DeqSets
Andrea Asperti [Thu, 15 Dec 2011 15:19:42 +0000 (15:19 +0000)]
Hints sui DeqSets

12 years agoMore stuff from CerCo to the standard library.
Claudio Sacerdoti Coen [Wed, 14 Dec 2011 15:41:12 +0000 (15:41 +0000)]
More stuff from CerCo to the standard library.

12 years agoSome more lemmas from CerCo.
Claudio Sacerdoti Coen [Wed, 14 Dec 2011 14:39:09 +0000 (14:39 +0000)]
Some more lemmas from CerCo.

12 years agoMatitaweb: large commit porting to the new Matita 0.95 syntax.
Wilmer Ricciotti [Wed, 14 Dec 2011 13:51:15 +0000 (13:51 +0000)]
Matitaweb: large commit porting to the new Matita 0.95 syntax.
Integrates some old patches.
Fixes a bug with GotoPos which prevented errors from being shown.

12 years ago1) Notation for dependent pairs differentiated from that for sigma types.
Claudio Sacerdoti Coen [Wed, 14 Dec 2011 12:18:07 +0000 (12:18 +0000)]
1) Notation for dependent pairs differentiated from that for sigma types.
2) Russell now works directly on mk_Sig/pi1

12 years agoDependent pairs (i.e. Sigma types in Type[0]) are back, but are not the default
Claudio Sacerdoti Coen [Tue, 13 Dec 2011 15:10:12 +0000 (15:10 +0000)]
Dependent pairs (i.e. Sigma types in Type[0]) are back, but are not the default
ones.

12 years ago1) PSig and Sig merged into a single Sigma type in Prop.
Claudio Sacerdoti Coen [Tue, 13 Dec 2011 13:47:28 +0000 (13:47 +0000)]
1) PSig and Sig merged into a single Sigma type in Prop.
2) One function in list.ma that required the Sigma type in Type has been
   removed.