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

12 years agoinject/eject replaced by mk_Sig/pi1.
Claudio Sacerdoti Coen [Tue, 13 Dec 2011 12:38:18 +0000 (12:38 +0000)]
inject/eject replaced by mk_Sig/pi1.

12 years ago1) New file russell with the coercions to activate Russell-style proving.
Claudio Sacerdoti Coen [Tue, 13 Dec 2011 12:17:18 +0000 (12:17 +0000)]
1) New file russell with the coercions to activate Russell-style proving.
2) More stuff on lists integrated from CerCo library

12 years agoChapter 5 = re.ma ; chapter 6 = moves.ma
matitaweb [Tue, 13 Dec 2011 11:45:17 +0000 (11:45 +0000)]
Chapter 5 = re.ma ; chapter 6 = moves.ma

12 years agoNew chapter 4
matitaweb [Tue, 13 Dec 2011 11:44:06 +0000 (11:44 +0000)]
New chapter 4

12 years agoMatitaweb: clicking buttons disables the GUI to prevent another operation from
Wilmer Ricciotti [Tue, 13 Dec 2011 11:40:23 +0000 (11:40 +0000)]
Matitaweb: clicking buttons disables the GUI to prevent another operation from
being issued before the first one has completed.

12 years agoSplitted re into lang.ma nd re.ma
Andrea Asperti [Tue, 13 Dec 2011 11:38:15 +0000 (11:38 +0000)]
Splitted re into lang.ma nd re.ma

12 years agoSig in Prop
Andrea Asperti [Tue, 13 Dec 2011 11:12:02 +0000 (11:12 +0000)]
Sig in Prop

12 years agoMore stuff integrated from CerCo on sigma types (that are now a record)
Claudio Sacerdoti Coen [Tue, 13 Dec 2011 10:44:50 +0000 (10:44 +0000)]
More stuff integrated from CerCo on sigma types (that are now a record)
and option.

12 years agoaxiom-
Enrico Tassi [Tue, 13 Dec 2011 08:43:55 +0000 (08:43 +0000)]
axiom-

12 years agopair => mk_Prod (one more was left in notation)
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 23:53:16 +0000 (23:53 +0000)]
pair => mk_Prod (one more was left in notation)

12 years agoprecedence level of if-then-else fixed
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 23:13:43 +0000 (23:13 +0000)]
precedence level of if-then-else fixed

12 years agoAdded elimination principles for destructuring let-ins.
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 22:41:13 +0000 (22:41 +0000)]
Added elimination principles for destructuring let-ins.

12 years agoSome integrations from CerCo. In particular:
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 20:17:23 +0000 (20:17 +0000)]
Some integrations from CerCo. In particular:

1) notation for destructuring let-ins for pairs, triples, quadruples, etc.
2) if-then-else is now a notation for pattern matching on booleans

12 years agosupport -axiom to avoind indexing an axiom (since there is no qed)
Enrico Tassi [Mon, 12 Dec 2011 20:14:53 +0000 (20:14 +0000)]
support -axiom to avoind indexing an axiom (since there is no qed)

12 years ago- we improved and updated the generated web pages
Ferruccio Guidi [Mon, 12 Dec 2011 17:10:51 +0000 (17:10 +0000)]
- we improved and updated the generated web pages

12 years agoPairs are now records.
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 16:52:47 +0000 (16:52 +0000)]
Pairs are now records.

Pros: projections from concrete records are now automatically reduced away.
Cons: the name of the constructor is no longer pair, but mk_Prod.

12 years agoParentheses are now needed. I do not know why and when this has changed.
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 16:35:41 +0000 (16:35 +0000)]
Parentheses are now needed. I do not know why and when this has changed.

12 years agoMatitaweb: changes to matitadaemon.ml to make it work with new secure user db.
Wilmer Ricciotti [Mon, 12 Dec 2011 15:45:52 +0000 (15:45 +0000)]
Matitaweb: changes to matitadaemon.ml to make it work with new secure user db.

12 years agoMatitaweb: added utility for conversion of user dbs from the old to the new
Wilmer Ricciotti [Mon, 12 Dec 2011 15:37:38 +0000 (15:37 +0000)]
Matitaweb: added utility for conversion of user dbs from the old to the new
format.

12 years agoRe-Ported to
Claudio Sacerdoti Coen [Mon, 12 Dec 2011 15:37:04 +0000 (15:37 +0000)]
Re-Ported to

- camlp5 version 6.02.2 + patches
- ocaml version 3.11.2-4

If you are still using the old version of OCaml + Camlp5, do not update
these two files.

12 years agoMatitaweb: secure SHA-256 encryption for passwords.
Wilmer Ricciotti [Mon, 12 Dec 2011 15:27:04 +0000 (15:27 +0000)]
Matitaweb: secure SHA-256 encryption for passwords.
Includes an utility for converting the user db to the new format.