]>
matita.cs.unibo.it Git - helm.git/log
Andrea Asperti [Fri, 6 Jun 2008 09:20:29 +0000 (09:20 +0000)]
Added frac.ma
Andrea Asperti [Fri, 6 Jun 2008 09:03:57 +0000 (09:03 +0000)]
Added Qplus_andrea.ma
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 08:27:51 +0000 (08:27 +0000)]
Reduce reduction tactic got rid of a long time ago.
Claudio Sacerdoti Coen [Thu, 5 Jun 2008 21:16:11 +0000 (21:16 +0000)]
Eratosthene's sieve factorized out of nat/bertrand.ma. Nothing added not
removed.
In theory, sieve.ma ishould not depend on nth_prime.ma and factorization.ma.
In practice, a proof requires factorization that, in turn, depends on
nth_prime.ma. To be investigated.
Enrico Tassi [Thu, 5 Jun 2008 17:11:33 +0000 (17:11 +0000)]
....
Enrico Tassi [Thu, 5 Jun 2008 15:41:15 +0000 (15:41 +0000)]
added order_continuity
Enrico Tassi [Thu, 5 Jun 2008 15:28:56 +0000 (15:28 +0000)]
sandwich is back
Wilmer Ricciotti [Wed, 4 Jun 2008 22:53:08 +0000 (22:53 +0000)]
Proof-irrelevance check for all applications (first version)
Wilmer Ricciotti [Wed, 4 Jun 2008 15:22:50 +0000 (15:22 +0000)]
incomplete irrelevance test commented out
Claudio Sacerdoti Coen [Tue, 3 Jun 2008 22:50:48 +0000 (22:50 +0000)]
Some proofs on enumerator and denominator.
Claudio Sacerdoti Coen [Tue, 3 Jun 2008 21:58:35 +0000 (21:58 +0000)]
More work on rational numbers with unique representations.
Enrico Tassi [Tue, 3 Jun 2008 15:56:51 +0000 (15:56 +0000)]
some work on uniformity
Enrico Tassi [Tue, 3 Jun 2008 12:09:21 +0000 (12:09 +0000)]
end of section 2.2
Enrico Tassi [Tue, 3 Jun 2008 08:12:57 +0000 (08:12 +0000)]
proof refactored
Enrico Tassi [Tue, 3 Jun 2008 08:12:38 +0000 (08:12 +0000)]
xxx
Enrico Tassi [Sun, 1 Jun 2008 15:38:46 +0000 (15:38 +0000)]
more work on supremum
Enrico Tassi [Fri, 30 May 2008 19:28:41 +0000 (19:28 +0000)]
CProp hierarchy is there!
Implications:
- more universes, XML file format changed, please rebuild your stuff
- CProp conclusions are eliminated with _rect and not _rec
- CProp and Types are interleaved, but still comparable, this may (or not)
what you expect: Type_i < CProp_i < Type_i+1 < CProp_i+1
Caveats:
- are_convertible sort CProp may turn to be wrong, since Type_i is convertible (<=) to CProp_i+0.5 and there is no way to set test_equality_only, an
additional parameter may be useful
- CProp goals will be tackled by auto even if they could be cumulated into
Type that is not (by default) take into consideration
Enrico Tassi [Fri, 30 May 2008 19:21:51 +0000 (19:21 +0000)]
irrelevance check half implemented but already impossible to
complete
Enrico Tassi [Fri, 30 May 2008 17:08:26 +0000 (17:08 +0000)]
...
Enrico Tassi [Fri, 30 May 2008 14:28:08 +0000 (14:28 +0000)]
garbage removed
Enrico Tassi [Fri, 30 May 2008 14:27:41 +0000 (14:27 +0000)]
more work on dama
Enrico Tassi [Fri, 30 May 2008 10:28:13 +0000 (10:28 +0000)]
prod moved under lambda-prolog unification case
Enrico Tassi [Fri, 30 May 2008 10:08:22 +0000 (10:08 +0000)]
added CProp
Enrico Tassi [Fri, 30 May 2008 09:17:02 +0000 (09:17 +0000)]
thanks to the fact that we convert well typed term and that
we convert only types, by inversion we know that types of lambdas
source are convertible if in head position
Enrico Tassi [Fri, 30 May 2008 09:12:51 +0000 (09:12 +0000)]
added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now is full whd
Enrico Tassi [Thu, 29 May 2008 16:38:51 +0000 (16:38 +0000)]
relevance check partially implemented but bugged since cic:/matita/nat/compare/eqb.con is not ok!
Enrico Tassi [Thu, 29 May 2008 16:34:08 +0000 (16:34 +0000)]
case not unfilding fixed
Enrico Tassi [Thu, 29 May 2008 16:27:26 +0000 (16:27 +0000)]
CProp, since it was defined in CoRN as a Type, is predicative.
However, it is not Type0, but a moving Type as usual, for example
inductive and (A,B:CProp) : CProp := ...
inductive exists (A:Type) (P:A->CProp) : CProp :=
| ext : \forall x:A. \forall p : P x. exists A P.
does not pass since the sort of x is Type not included in CProp. Putting
exists in Type does not work either, if you want to make a conjuction
involving an existential.
solution, to be implemented:
CProp of CicUniv.universe
where CProp n is meant to be Type (n + 0.5).
Enrico Tassi [Thu, 29 May 2008 14:15:25 +0000 (14:15 +0000)]
0.5.1 released
Enrico Tassi [Thu, 29 May 2008 12:28:32 +0000 (12:28 +0000)]
unused variables removed
Enrico Tassi [Thu, 29 May 2008 11:51:14 +0000 (11:51 +0000)]
ref sync check fixed controlling fix/cofix coherence
Enrico Tassi [Thu, 29 May 2008 11:38:44 +0000 (11:38 +0000)]
...
Enrico Tassi [Thu, 29 May 2008 09:51:22 +0000 (09:51 +0000)]
first page of the new dama proof
Enrico Tassi [Thu, 29 May 2008 09:45:35 +0000 (09:45 +0000)]
...
Enrico Tassi [Thu, 29 May 2008 09:43:47 +0000 (09:43 +0000)]
the type of the match was obtained reducing the outtype
applied to right + matched with whd ~delta:true that
is not what you want. replaced with head_beta_reduce.
Enrico Tassi [Wed, 28 May 2008 12:48:43 +0000 (12:48 +0000)]
...
Enrico Tassi [Wed, 28 May 2008 11:00:26 +0000 (11:00 +0000)]
dama restarted
Enrico Tassi [Wed, 28 May 2008 10:40:54 +0000 (10:40 +0000)]
cleanup
Enrico Tassi [Wed, 28 May 2008 10:39:13 +0000 (10:39 +0000)]
the attempt of completing dama using duality frozen
Enrico Tassi [Wed, 28 May 2008 10:11:11 +0000 (10:11 +0000)]
0.5.1
Enrico Tassi [Tue, 27 May 2008 15:47:54 +0000 (15:47 +0000)]
...
Enrico Tassi [Tue, 27 May 2008 15:42:03 +0000 (15:42 +0000)]
smarter lexer needed by lambda-delta that is splitting "let rec" statements
on multiple lines
Enrico Tassi [Tue, 27 May 2008 10:56:02 +0000 (10:56 +0000)]
...
Enrico Tassi [Tue, 27 May 2008 08:51:59 +0000 (08:51 +0000)]
CoRN moved in contribs
Enrico Tassi [Tue, 27 May 2008 08:47:27 +0000 (08:47 +0000)]
frst step to move away the CoRN stuff
Enrico Tassi [Tue, 27 May 2008 08:46:56 +0000 (08:46 +0000)]
frst step to move away the CoRN stuff
Enrico Tassi [Tue, 27 May 2008 08:36:21 +0000 (08:36 +0000)]
auto calls cleanup\
Enrico Tassi [Mon, 26 May 2008 16:33:07 +0000 (16:33 +0000)]
better description of declarative tactics
Enrico Tassi [Mon, 26 May 2008 14:01:04 +0000 (14:01 +0000)]
new, more rigid syntax, for auto_params affecting the declarative language.
many multi-word constructs (like 'we proved') are now a single token.
all declarative tactics now use auto_params.
syntax of declarative tactics changed.
many camlp5 refactoring to avoid many rule conflics.
Enrico Tassi [Mon, 26 May 2008 13:58:13 +0000 (13:58 +0000)]
Universe.key was not used to index terms, but was used to retrieve them
Ferruccio Guidi [Mon, 26 May 2008 13:43:02 +0000 (13:43 +0000)]
better presentation of lambda-delta
Ferruccio Guidi [Mon, 26 May 2008 12:30:21 +0000 (12:30 +0000)]
- some bugs fixed in the domain-based preorders on environments
- some missing lemmas added
Enrico Tassi [Mon, 26 May 2008 10:43:31 +0000 (10:43 +0000)]
added comment for zack
Enrico Tassi [Mon, 26 May 2008 09:47:12 +0000 (09:47 +0000)]
...
Enrico Tassi [Mon, 26 May 2008 09:46:16 +0000 (09:46 +0000)]
auto syntax updated
Enrico Tassi [Mon, 26 May 2008 09:13:07 +0000 (09:13 +0000)]
...
Enrico Tassi [Sat, 24 May 2008 13:16:12 +0000 (13:16 +0000)]
...
Enrico Tassi [Sat, 24 May 2008 10:32:53 +0000 (10:32 +0000)]
order of goals changes, open ones are preferred to closed ones as in the paper
Enrico Tassi [Wed, 21 May 2008 12:23:53 +0000 (12:23 +0000)]
minimal implementation of left parameters display
Enrico Tassi [Wed, 21 May 2008 10:40:56 +0000 (10:40 +0000)]
0.5.1 should be realased soon, the bug that was affecting fixpoints
disambiguation is nasty
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:42:25 +0000 (23:42 +0000)]
Here is where we should add relevance checks.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:31:44 +0000 (23:31 +0000)]
Bug fixed in computation of leftnos: variables were not considered.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:31:21 +0000 (23:31 +0000)]
Code simplification.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:06:08 +0000 (23:06 +0000)]
Added cprop <= type constraint.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:01:48 +0000 (23:01 +0000)]
We do not need to give cprop a special status yet.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:01:32 +0000 (23:01 +0000)]
...
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:00:11 +0000 (23:00 +0000)]
CProp dropped in favour of a cprop universe exported from NCicEnvironment,
which is just an URI recognized by the pretty printer.
Enrico Tassi [Mon, 19 May 2008 20:58:36 +0000 (20:58 +0000)]
added leftno to references f inductive types and constructors, more unifor names of modules, NCic -> C and NReference Ref everywhere
Enrico Tassi [Mon, 19 May 2008 14:36:16 +0000 (14:36 +0000)]
added aps generation
Claudio Sacerdoti Coen [Mon, 19 May 2008 11:59:37 +0000 (11:59 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Enrico Tassi [Mon, 19 May 2008 11:41:46 +0000 (11:41 +0000)]
...
Enrico Tassi [Mon, 19 May 2008 11:41:21 +0000 (11:41 +0000)]
renamed add_le_constraint to add_constraint since it adds both le and lt constraints
Claudio Sacerdoti Coen [Sun, 18 May 2008 21:29:29 +0000 (21:29 +0000)]
...
Claudio Sacerdoti Coen [Sun, 18 May 2008 21:00:31 +0000 (21:00 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Enrico Tassi [Sun, 18 May 2008 20:51:26 +0000 (20:51 +0000)]
run fsub during night
Claudio Sacerdoti Coen [Sun, 18 May 2008 20:51:15 +0000 (20:51 +0000)]
Bug fixed: when computing the left arguments, I was not doing the right thing.
New check implemented: references should cache data correctly.
Claudio Sacerdoti Coen [Sun, 18 May 2008 20:06:29 +0000 (20:06 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:56:38 +0000 (19:56 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:30:44 +0000 (19:30 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Enrico Tassi [Sun, 18 May 2008 19:29:56 +0000 (19:29 +0000)]
names fixed accoding to the new ones generated after arity of
indtypes is not cleaned for dummy names
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:22:55 +0000 (19:22 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:14:34 +0000 (19:14 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:04:18 +0000 (19:04 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Enrico Tassi [Sun, 18 May 2008 19:03:13 +0000 (19:03 +0000)]
revert last commit, context' -> context (added comment)
Enrico Tassi [Sun, 18 May 2008 18:37:28 +0000 (18:37 +0000)]
using the right names in the context to check match patterns(better error report) and use the refined matched term to compute the type
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:31:45 +0000 (18:31 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:22:24 +0000 (18:22 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:19:39 +0000 (18:19 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:55:16 +0000 (17:55 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:49:57 +0000 (17:49 +0000)]
New missing check implemented: the left parameters of each constructor and
inductive types should be convertible and should have the very same name.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:46:38 +0000 (17:46 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:44:51 +0000 (17:44 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:38:47 +0000 (17:38 +0000)]
Dummy dependent products in inductive types arities are no longer cleaned.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:31:41 +0000 (17:31 +0000)]
This commit avoids cleaning dummy dependent types in the arities of inductive
types. This is an overkilling solution to the problem of avoiding cleaning
dummy dependent types in the left products in the arities of inductive types.
The left products should be _syntactically_ the same as those of the
constructors. Otherwise, error reporting is incorrect.
Claudio Sacerdoti Coen [Sun, 18 May 2008 08:16:55 +0000 (08:16 +0000)]
Implemented translation of inductive types from the new to the old format.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:52:55 +0000 (07:52 +0000)]
Serious bug fixed: the max of two universes was computed using the polymorphic
max function of OCaml instead of append!!!
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:49:20 +0000 (07:49 +0000)]
Synch with the paper.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:42:05 +0000 (07:42 +0000)]
...
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:30:14 +0000 (07:30 +0000)]
Error message improved.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:25:38 +0000 (07:25 +0000)]
More effective optimization: avoid introducing already implied arcs.