]>
matita.cs.unibo.it Git - helm.git/log
Enrico Tassi [Wed, 30 Jun 2010 13:29:50 +0000 (13:29 +0000)]
...
Enrico Tassi [Wed, 30 Jun 2010 09:44:22 +0000 (09:44 +0000)]
....
Enrico Tassi [Tue, 29 Jun 2010 14:03:40 +0000 (14:03 +0000)]
...
Enrico Tassi [Tue, 29 Jun 2010 12:07:37 +0000 (12:07 +0000)]
notation made half decent
Enrico Tassi [Mon, 28 Jun 2010 20:15:28 +0000 (20:15 +0000)]
better notation for oalgebra
Enrico Tassi [Fri, 18 Jun 2010 11:11:43 +0000 (11:11 +0000)]
....
Enrico Tassi [Thu, 17 Jun 2010 21:41:00 +0000 (21:41 +0000)]
off by one fixed
Wilmer Ricciotti [Thu, 10 Jun 2010 18:23:59 +0000 (18:23 +0000)]
Fix for inversion principles of types with a single constructor.
Wilmer Ricciotti [Tue, 8 Jun 2010 16:15:14 +0000 (16:15 +0000)]
Fixed a bug in the undebruijnate function which caused the refiner to produce
Enrico Tassi [Mon, 7 Jun 2010 22:56:03 +0000 (22:56 +0000)]
some stuff on re
Enrico Tassi [Mon, 7 Jun 2010 22:55:47 +0000 (22:55 +0000)]
unify left args of inductive types with left argus of constructors. this allows
Wilmer Ricciotti [Wed, 12 May 2010 18:41:47 +0000 (18:41 +0000)]
Library support files for John Major equality and Russell.
Wilmer Ricciotti [Wed, 12 May 2010 18:39:05 +0000 (18:39 +0000)]
Experimental support for Russell (coercions moving inside lambda & pattern
Andrea Asperti [Tue, 11 May 2010 08:50:33 +0000 (08:50 +0000)]
minimization.ma
Enrico Tassi [Tue, 11 May 2010 07:21:34 +0000 (07:21 +0000)]
little workaround for multiple screens, gdk support not bound by lablgtk2
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
Enrico Tassi [Fri, 7 May 2010 21:21:01 +0000 (21:21 +0000)]
trace generation with "// by _;"
Enrico Tassi [Fri, 7 May 2010 21:20:58 +0000 (21:20 +0000)]
notation
Andrea Asperti [Fri, 7 May 2010 10:04:00 +0000 (10:04 +0000)]
remarks and applyS
Claudio Sacerdoti Coen [Thu, 6 May 2010 22:35:02 +0000 (22:35 +0000)]
Bug fixed: nstatus => status (to undo the changes).
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:52:38 +0000 (15:52 +0000)]
...
Wilmer Ricciotti [Thu, 6 May 2010 15:50:07 +0000 (15:50 +0000)]
Fixing naming scheme for composite coercions.
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:45:35 +0000 (15:45 +0000)]
assert false could happen
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)]
Bug fixed:
Claudio Sacerdoti Coen [Wed, 5 May 2010 15:13:41 +0000 (15:13 +0000)]
coinduction is between us
Claudio Sacerdoti Coen [Wed, 5 May 2010 14:29:57 +0000 (14:29 +0000)]
First tests.
Wilmer Ricciotti [Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)]
* Fixed a couple of glitches in ndestruct
Claudio Sacerdoti Coen [Tue, 4 May 2010 16:40:26 +0000 (16:40 +0000)]
Regular expressions.
Ferruccio Guidi [Wed, 21 Apr 2010 09:00:04 +0000 (09:00 +0000)]
new dependences
From: fguidi <fguidi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Mon, 19 Apr 2010 09:47:02 +0000 (09:47 +0000)]
Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Mon, 19 Apr 2010 09:44:21 +0000 (09:44 +0000)]
alpha_eq instead of pervasives.compare
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 15 Apr 2010 14:02:02 +0000 (14:02 +0000)]
bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 15:47:51 +0000 (15:47 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 14:06:35 +0000 (14:06 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:42:14 +0000 (13:42 +0000)]
Formal points.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:28:53 +0000 (13:28 +0000)]
Some dualization clean-up.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:56:18 +0000 (19:56 +0000)]
fixed makefile
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:55:18 +0000 (19:55 +0000)]
auto destructs while introducing in the context
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:54:23 +0000 (19:54 +0000)]
print nobjects (hack with Obj.magic)
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)]
catch the right exception, avoid uncaught Subst_not_found
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:52:58 +0000 (19:52 +0000)]
same heads different arity -> INCOMPARABLE
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:52:26 +0000 (19:52 +0000)]
some fixes to THF parser
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Tue, 13 Apr 2010 19:51:39 +0000 (19:51 +0000)]
fixed support file for TPTP
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Ferruccio Guidi [Sun, 11 Apr 2010 17:13:56 +0000 (17:13 +0000)]
the edges must be quoted as well (not only the nodes)
From: fguidi <fguidi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Fri, 9 Apr 2010 14:04:08 +0000 (14:04 +0000)]
apply_subst_context on statuses
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:49:30 +0000 (17:49 +0000)]
...
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)]
support axioms
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:33:28 +0000 (17:33 +0000)]
...
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:31:03 +0000 (17:31 +0000)]
thf problems list for tptp 4.0.1
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 17:28:13 +0000 (17:28 +0000)]
fixed compiltion order of lexer/parser
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:38:53 +0000 (16:38 +0000)]
New code (unbranched) to compute all keys by all possible ways of reducing the term.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:37:26 +0000 (16:37 +0000)]
New sets of.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Thu, 8 Apr 2010 14:43:43 +0000 (14:43 +0000)]
THF parser received some care
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 8 Apr 2010 13:02:05 +0000 (13:02 +0000)]
Fixing indexing (commit parziale di Claudio?)
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Enrico Tassi [Wed, 7 Apr 2010 13:34:29 +0000 (13:34 +0000)]
THF parser for TPTP
From: tassi <tassi@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 16:27:56 +0000 (16:27 +0000)]
Not is now inductive.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:53:12 +0000 (14:53 +0000)]
Use the inversion!
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:41:09 +0000 (14:41 +0000)]
Bug fixed: the current equation is not always the last hyp.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:40:34 +0000 (14:40 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:49:43 +0000 (13:49 +0000)]
- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:35:12 +0000 (13:35 +0000)]
More debugging info from print_tac.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:33:55 +0000 (13:33 +0000)]
Implicit and UserInput were printed incorrectly.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:31:23 +0000 (13:31 +0000)]
ninversion
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Wed, 31 Mar 2010 10:29:30 +0000 (10:29 +0000)]
removed boh
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Wilmer Ricciotti [Wed, 31 Mar 2010 09:39:37 +0000 (09:39 +0000)]
Added test file for inversion in ng matita.
From: ricciott <ricciott@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Wed, 31 Mar 2010 09:07:11 +0000 (09:07 +0000)]
Tracing mechanism for auto. Interface changed to solve an ambiguity between
an ampty trace and a missing trace.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 18:14:54 +0000 (18:14 +0000)]
Good definition found.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 17:27:53 +0000 (17:27 +0000)]
(Co)Inductively Generated Formal Topologies (not only basic ones)
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Matthias Puech [Thu, 25 Mar 2010 18:20:15 +0000 (18:20 +0000)]
patched the definition of locate, advances in locate_add; still issues..
From: puech <puech@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Wilmer Ricciotti [Thu, 25 Mar 2010 18:00:49 +0000 (18:00 +0000)]
Z.ma updated to reflect changes in the logical Not operator
From: ricciott <ricciott@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Matthias Puech [Thu, 25 Mar 2010 16:23:10 +0000 (16:23 +0000)]
Automation problem
From: puech <puech@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 14:22:31 +0000 (14:22 +0000)]
More work
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 09:22:23 +0000 (09:22 +0000)]
cosi va (se vi pare).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Thu, 25 Mar 2010 09:12:41 +0000 (09:12 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 08:41:21 +0000 (08:41 +0000)]
Conflict(?).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Thu, 25 Mar 2010 08:36:02 +0000 (08:36 +0000)]
Extension of demod to arbtrary predicates (not just equalities).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:56:32 +0000 (17:56 +0000)]
Nice examples for automation (that fails).
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:48:45 +0000 (17:48 +0000)]
Simplified proof after pattern fix
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:36:05 +0000 (17:36 +0000)]
"Not" is no longer a definition
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:35:24 +0000 (17:35 +0000)]
The precedence of ^-1 has changed.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:33:09 +0000 (17:33 +0000)]
Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:27:01 +0000 (17:27 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:35:57 +0000 (14:35 +0000)]
Axioms were not indexed.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:33:55 +0000 (14:33 +0000)]
Axioms were not indexed.
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:20:39 +0000 (14:20 +0000)]
...
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:19:52 +0000 (14:19 +0000)]
Real numbers as co-inductive streams of digits (overlapping refining intervals).
From: sacerdot <sacerdot@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Wed, 24 Mar 2010 13:04:27 +0000 (13:04 +0000)]
Computation of the trace.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Matthias Puech [Tue, 23 Mar 2010 18:24:49 +0000 (18:24 +0000)]
typo in a proof
From: puech <puech@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 17:50:12 +0000 (17:50 +0000)]
One more case.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 16:31:55 +0000 (16:31 +0000)]
Readded eqf_2.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)]
symmetric_eq -> sym_eq
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 15:52:29 +0000 (15:52 +0000)]
Re-proved an axiom
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 15:51:56 +0000 (15:51 +0000)]
Commented a few lemmas (copies).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 15:48:42 +0000 (15:48 +0000)]
Fixed a few bugs
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 15:45:06 +0000 (15:45 +0000)]
"flat" function (subst unfolding)
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)]
Keeping only lift_aux e subst_aux (renamed to lift and subst).
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Andrea Asperti [Tue, 23 Mar 2010 07:31:12 +0000 (07:31 +0000)]
Moved compare in a different file.
From: asperti <asperti@
c2b2084f -9a08-0410-b176-
e24b037a169a >
Matthias Puech [Thu, 18 Mar 2010 17:44:52 +0000 (17:44 +0000)]
Downgrading level of infix notations involving \sup.
Andrea Asperti [Thu, 18 Mar 2010 11:36:56 +0000 (11:36 +0000)]
Porting alla nuova def. di negazione
Andrea Asperti [Thu, 18 Mar 2010 11:35:44 +0000 (11:35 +0000)]
Nuova versione di not.
projects / helm.git / log