]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Thu, 30 Aug 2007 13:10:22 +0000 (13:10 +0000)]
print few more wired assertions
Enrico Tassi [Thu, 30 Aug 2007 13:10:08 +0000 (13:10 +0000)]
the version on the livecd
Enrico Tassi [Thu, 30 Aug 2007 13:09:08 +0000 (13:09 +0000)]
more stuff to reach an intensional definition of finite sets
Enrico Tassi [Thu, 30 Aug 2007 13:08:24 +0000 (13:08 +0000)]
added an utility function
Enrico Tassi [Thu, 30 Aug 2007 13:07:59 +0000 (13:07 +0000)]
0.2.0
Claudio Sacerdoti Coen [Tue, 28 Aug 2007 15:32:32 +0000 (15:32 +0000)]
* definition of implication free propositional formulas
* definition of a classical semantics
* proofs of correctness of some syntactical manipulations to reach
normal forms
* definition of sequent calculus trees
* proof of soundness of sequent calculus derivations
* proof of completeness of sequent calculus derivations (unfinished)
Claudio Sacerdoti Coen [Tue, 28 Aug 2007 15:27:01 +0000 (15:27 +0000)]
A primer for Matita with some easy, medium, difficult and impossible exercises.
Ferruccio Guidi [Sun, 26 Aug 2007 17:32:07 +0000 (17:32 +0000)]
We define proof tree tracks and normal proof tree tracks separately
Ferruccio Guidi [Sun, 26 Aug 2007 16:36:34 +0000 (16:36 +0000)]
refactoring
Ferruccio Guidi [Sun, 26 Aug 2007 16:29:31 +0000 (16:29 +0000)]
proof by "introduction" (impi) implemented in full
Claudio Sacerdoti Coen [Sat, 25 Aug 2007 13:31:11 +0000 (13:31 +0000)]
thread-based interface activated again
Claudio Sacerdoti Coen [Thu, 23 Aug 2007 20:54:05 +0000 (20:54 +0000)]
Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
handled incorrectly (according to the is_top_down flag that should be irrelevant).
Claudio Sacerdoti Coen [Thu, 23 Aug 2007 20:21:35 +0000 (20:21 +0000)]
Bug fixed: the initial metasenv used in the two tactic was empty!
Claudio Sacerdoti Coen [Wed, 22 Aug 2007 09:39:34 +0000 (09:39 +0000)]
Avoid reusing Hbeta several times.
Claudio Sacerdoti Coen [Wed, 22 Aug 2007 08:14:21 +0000 (08:14 +0000)]
select now works correctly even if multiple hypotheses with the same name are
present in the context.
Claudio Sacerdoti Coen [Tue, 21 Aug 2007 10:18:46 +0000 (10:18 +0000)]
Avoid confusion for names of proofs put in the applicative context.
Claudio Sacerdoti Coen [Tue, 21 Aug 2007 09:48:14 +0000 (09:48 +0000)]
"obtain H E1=E2 by proof" is now working
Cristian Armentano [Thu, 16 Aug 2007 18:45:46 +0000 (18:45 +0000)]
little change to theorem eq_gcd_times_times_eqv_times_gcd
Andrea Asperti [Tue, 31 Jul 2007 11:18:35 +0000 (11:18 +0000)]
removed generic_sigma_p since generic_iter_p is the same
Enrico Tassi [Tue, 31 Jul 2007 10:40:30 +0000 (10:40 +0000)]
something was really too slow...
Enrico Tassi [Tue, 31 Jul 2007 10:39:53 +0000 (10:39 +0000)]
default equality stuff filtered out from hint rewrite
Enrico Tassi [Tue, 31 Jul 2007 10:39:31 +0000 (10:39 +0000)]
removed comments in proof presentation
Cristian Armentano [Mon, 30 Jul 2007 15:01:31 +0000 (15:01 +0000)]
renamed generic_sigma_p.ma to generic_iter_p.ma
Enrico Tassi [Mon, 30 Jul 2007 12:00:31 +0000 (12:00 +0000)]
added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.
Ferruccio Guidi [Thu, 26 Jul 2007 14:35:05 +0000 (14:35 +0000)]
We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]
Enrico Tassi [Thu, 26 Jul 2007 13:47:07 +0000 (13:47 +0000)]
added development path normalization, inclusions with '../' in the path should now be handled correclty
Enrico Tassi [Thu, 26 Jul 2007 13:46:07 +0000 (13:46 +0000)]
auto -> autobatch
Wilmer Ricciotti [Thu, 26 Jul 2007 13:06:09 +0000 (13:06 +0000)]
Some notation added
Enrico Tassi [Thu, 26 Jul 2007 10:41:15 +0000 (10:41 +0000)]
more stuff about coercions
Enrico Tassi [Thu, 26 Jul 2007 10:39:38 +0000 (10:39 +0000)]
little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).
Ferruccio Guidi [Thu, 26 Jul 2007 08:58:11 +0000 (08:58 +0000)]
makefiles updated
Ferruccio Guidi [Wed, 25 Jul 2007 19:05:34 +0000 (19:05 +0000)]
makefile updated
Ferruccio Guidi [Wed, 25 Jul 2007 14:39:14 +0000 (14:39 +0000)]
matitac: We do not generate the .moo and .lexicon of a dumped .mma
Base-2 : makefile patched
Enrico Tassi [Wed, 25 Jul 2007 13:55:53 +0000 (13:55 +0000)]
added some notation
Enrico Tassi [Wed, 25 Jul 2007 10:13:55 +0000 (10:13 +0000)]
added another example in which our coercions are powerful
Enrico Tassi [Wed, 25 Jul 2007 09:43:35 +0000 (09:43 +0000)]
used ;try assumption instead of .try assumption
Enrico Tassi [Wed, 25 Jul 2007 09:41:50 +0000 (09:41 +0000)]
; and not . after auto-paramodulation
Enrico Tassi [Wed, 25 Jul 2007 09:40:14 +0000 (09:40 +0000)]
reverted previous fix
Enrico Tassi [Wed, 25 Jul 2007 09:18:36 +0000 (09:18 +0000)]
restored compaction of metas at the end of given_clause
Ferruccio Guidi [Tue, 24 Jul 2007 11:54:28 +0000 (11:54 +0000)]
Makefile missing in previous commit
Ferruccio Guidi [Tue, 24 Jul 2007 11:52:05 +0000 (11:52 +0000)]
New developement LOGIC about the cut elimination of implication for Sambin's basic logic; one of the rules must be corrected (work is in progress)
Enrico Tassi [Tue, 24 Jul 2007 08:58:16 +0000 (08:58 +0000)]
added test about dependent coercions
Claudio Sacerdoti Coen [Mon, 23 Jul 2007 15:14:29 +0000 (15:14 +0000)]
Prototype of min_aux changed.
Now (min_aux off n f) find the smallest i such that
* f i = true or i = n+off
* \forall j, n <= j <= n+off, f j = false
The new function does no longer compute with off. Thus we obtain
for free a great computational speed-up in every function defined
in terms of it.
Ferruccio Guidi [Mon, 23 Jul 2007 13:22:22 +0000 (13:22 +0000)]
auto vs autobatch fixed
Ferruccio Guidi [Mon, 23 Jul 2007 13:12:40 +0000 (13:12 +0000)]
autobatch parameters reajusted
Enrico Tassi [Mon, 23 Jul 2007 09:14:53 +0000 (09:14 +0000)]
fixed makefiles to make it compile cleanly again
Ferruccio Guidi [Sun, 22 Jul 2007 18:33:38 +0000 (18:33 +0000)]
Procedural: the statement body and it inner types must satisfy the Barendregt
convenction on bound variables
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:59:27 +0000 (16:59 +0000)]
Another nicer version.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:53:33 +0000 (16:53 +0000)]
Even nicer script.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 16:20:30 +0000 (16:20 +0000)]
The nicest script obtained so far.
What is left, is a bunch of change/normalize/whd/simplify that are difficult
to control precisely.
Ferruccio Guidi [Fri, 20 Jul 2007 14:48:36 +0000 (14:48 +0000)]
acic_procedural: bug fix:
sometimes whd is not enough, we need normalize ...
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 14:28:55 +0000 (14:28 +0000)]
More simplification due to the new conversion strategy.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 14:26:01 +0000 (14:26 +0000)]
Script simplification due to the new efficient conversion strategy.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 09:58:30 +0000 (09:58 +0000)]
Tentative bug fix for diverging pretty-printing function.
Claudio Sacerdoti Coen [Fri, 20 Jul 2007 09:32:39 +0000 (09:32 +0000)]
Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
(so that ocamlc now works again).
Ferruccio Guidi [Thu, 19 Jul 2007 18:00:55 +0000 (18:00 +0000)]
cicUtil : new test function "is_sober" to test the integrity of a term
now fails when fake applications are detected
acic_procedural: some bug fix
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 17:54:40 +0000 (17:54 +0000)]
Convertibility now converts machines in place of terms.
Actually, the heads of the machines (i.e. everything but the stack) are
still unwinded and converted as terms. Thus there is much space for
improvement.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 12:07:44 +0000 (12:07 +0000)]
map_unicode_to_tex is no longer optional and it always refers to the current
user choice.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 10:19:28 +0000 (10:19 +0000)]
paste_unicode_as_tex is now false by default; moreover the flag is used
everywhere (but in patterns, I do not know why)
Enrico Tassi [Thu, 19 Jul 2007 10:03:42 +0000 (10:03 +0000)]
COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.
Enrico Tassi [Thu, 19 Jul 2007 10:02:11 +0000 (10:02 +0000)]
the cade was escaping the table name and not the uri
Enrico Tassi [Thu, 19 Jul 2007 10:01:40 +0000 (10:01 +0000)]
fixed escaping for sqlite
Enrico Tassi [Thu, 19 Jul 2007 10:01:13 +0000 (10:01 +0000)]
fixed an escaping error, added more infos to the generic error, callback catches and prints exceptions
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 09:17:32 +0000 (09:17 +0000)]
Typo fixed.
Claudio Sacerdoti Coen [Thu, 19 Jul 2007 09:15:31 +0000 (09:15 +0000)]
Super-nice notation for the assembly stuff.
Ferruccio Guidi [Wed, 18 Jul 2007 16:07:11 +0000 (16:07 +0000)]
the predicate for elim was not built correctly when more than one right parameter was found
Enrico Tassi [Wed, 18 Jul 2007 11:17:46 +0000 (11:17 +0000)]
recursive argument in let rec is not printed explicitly.
I let to ferruccio optimize the case in which there is only one argument or the recno is 0 and thus can be omitted
Enrico Tassi [Wed, 18 Jul 2007 10:46:11 +0000 (10:46 +0000)]
fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions
Claudio Sacerdoti Coen [Tue, 17 Jul 2007 11:41:07 +0000 (11:41 +0000)]
added missing parenthesis
Enrico Tassi [Tue, 17 Jul 2007 10:00:30 +0000 (10:00 +0000)]
fixed includes and added notation for bytes
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 22:20:08 +0000 (22:20 +0000)]
More lemmas.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 21:39:13 +0000 (21:39 +0000)]
More daemons closed. A couple left in byte and many in extras.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 20:48:20 +0000 (20:48 +0000)]
More daemons/axioms closed.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 17:51:02 +0000 (17:51 +0000)]
One daemon less.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 17:35:38 +0000 (17:35 +0000)]
More daemons got rid of (and more extra axioms to be proved).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:10:40 +0000 (16:10 +0000)]
Last daemon killed :-)
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:07:42 +0000 (16:07 +0000)]
One less daemon (about "update"s).
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 16:04:05 +0000 (16:04 +0000)]
All sub-proofs about "update" closed.
Claudio Sacerdoti Coen [Mon, 16 Jul 2007 14:51:18 +0000 (14:51 +0000)]
assembly.ma splitted into many files
Stefano Zacchiroli [Mon, 16 Jul 2007 14:34:55 +0000 (14:34 +0000)]
* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:33:30 +0000 (14:33 +0000)]
* NOT RELEASED YET
Stefano Zacchiroli [Mon, 16 Jul 2007 14:30:27 +0000 (14:30 +0000)]
proper path for ps.gz doc
Stefano Zacchiroli [Mon, 16 Jul 2007 14:21:44 +0000 (14:21 +0000)]
texlive-base-bin, texlive-latex-extra
Stefano Zacchiroli [Mon, 16 Jul 2007 14:17:45 +0000 (14:17 +0000)]
- add build-dep for doc generation: graphviz, texlive-latex-recommended,
Stefano Zacchiroli [Mon, 16 Jul 2007 14:12:20 +0000 (14:12 +0000)]
- add build-dep for doc generation: graphviz, texlive-latex-base,
texlive-base-bin
Stefano Zacchiroli [Mon, 16 Jul 2007 14:09:23 +0000 (14:09 +0000)]
* debian/rules
- build ocamldoc documentation at package build time
- add build-dep on graphviz
Stefano Zacchiroli [Mon, 16 Jul 2007 14:05:57 +0000 (14:05 +0000)]
invoke make doc after build to create ocamldoc docs
Stefano Zacchiroli [Mon, 16 Jul 2007 13:59:36 +0000 (13:59 +0000)]
* debian/svn-deblayout
- add repository layout information
Stefano Zacchiroli [Mon, 16 Jul 2007 13:56:27 +0000 (13:56 +0000)]
* rebuild against OCaml 3.10 and ocamlnet 2.2
* add preliminary support for cookies (new "cookies" method added to an
- use ocaml.mk CDBS class
- add build-dep on camlp4, which is now in a separate package
- bump debhelper dep and compatibility level to 5
Stefano Zacchiroli [Mon, 16 Jul 2007 13:49:22 +0000 (13:49 +0000)]
* debian/*.install.in
- do not attempt to instal *.ml files in target lib directory since they
are no longer installed by Makefile
Stefano Zacchiroli [Mon, 16 Jul 2007 13:31:55 +0000 (13:31 +0000)]
* rebuild with OCaml 3.10
* bump debhelper deps and compatibility level to 5
- s/Source-Version/binary:Version
Wilmer Ricciotti [Mon, 16 Jul 2007 13:07:53 +0000 (13:07 +0000)]
corrected axiom mod_plus
Ferruccio Guidi [Sat, 14 Jul 2007 14:37:11 +0000 (14:37 +0000)]
new definitions and new theorems
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 22:04:05 +0000 (22:04 +0000)]
More conjectures closed.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:08:28 +0000 (18:08 +0000)]
1. requires the new pretty printer for natural numbers
2. important properties of plusbyte proved
3. all important conjectures almost proved
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 18:04:35 +0000 (18:04 +0000)]
Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers. Eureka.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 09:56:42 +0000 (09:56 +0000)]
Last crazy commit reverted.
Claudio Sacerdoti Coen [Fri, 13 Jul 2007 08:35:47 +0000 (08:35 +0000)]
Final theorem proved. Many many conjectures left. I am unsure of one of them.
Claudio Sacerdoti Coen [Thu, 12 Jul 2007 18:38:04 +0000 (18:38 +0000)]
The loop invariant I chosed was not correct!
1. statement to be fixed
2. is the new loop invariant strong enough?
3. lot of daemons here and there
4. two conjectures I am not sure of:
plusbytenc (x*n) x = byte_of_nat (x*S n)
plusbytec (x*n) x = plusbytec (x*S n)
Claudio Sacerdoti Coen [Wed, 11 Jul 2007 17:10:26 +0000 (17:10 +0000)]
Getting close to the final result.
The showstopper now is the GtkMathView/Pango bug!
Moreover, unification has become mostly useless (and rewriting with it).