]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoNew lemma
Claudio Sacerdoti Coen [Fri, 13 Jun 2008 09:07:16 +0000 (09:07 +0000)]
New lemma
theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

16 years agomore notation
Enrico Tassi [Fri, 13 Jun 2008 07:14:52 +0000 (07:14 +0000)]
more notation

16 years ago...
Enrico Tassi [Fri, 13 Jun 2008 07:14:40 +0000 (07:14 +0000)]
...

16 years agoprint the name not found in the env
Enrico Tassi [Fri, 13 Jun 2008 07:14:30 +0000 (07:14 +0000)]
print the name not found in the env

16 years agoTesting some performance tricks by caching the list of the first n primes and
Enrico Tassi [Thu, 12 Jun 2008 15:52:34 +0000 (15:52 +0000)]
Testing some performance tricks by caching the list of the first n primes and
showing that they are good either with nth_prime (sloooooooooowww) or with
sieve (slooooow and not proved correct yet). With sieve we are currently able
to verify the list of the first 103 primes in a sort of reasonable time.
The 103rd prime is only 593 :-(

16 years agobetter names in a lemma to increase readability
Enrico Tassi [Thu, 12 Jun 2008 08:53:45 +0000 (08:53 +0000)]
better names in a lemma to increase readability

16 years agofixed some regressions
Enrico Tassi [Thu, 12 Jun 2008 08:40:06 +0000 (08:40 +0000)]
fixed some regressions

16 years agoNew, much faster implementation of factorize.
Claudio Sacerdoti Coen [Wed, 11 Jun 2008 18:00:20 +0000 (18:00 +0000)]
New, much faster implementation of factorize.

16 years agogran casino
Enrico Tassi [Wed, 11 Jun 2008 16:58:16 +0000 (16:58 +0000)]
gran casino

16 years agometa not considered before in outtype
Enrico Tassi [Wed, 11 Jun 2008 09:24:08 +0000 (09:24 +0000)]
meta not considered before in outtype

16 years agobla bla bla
Enrico Tassi [Tue, 10 Jun 2008 15:58:54 +0000 (15:58 +0000)]
bla bla bla

16 years agorelevance check for Match
Wilmer Ricciotti [Tue, 10 Jun 2008 15:32:22 +0000 (15:32 +0000)]
relevance check for Match

16 years agoinitial qork for models
Enrico Tassi [Tue, 10 Jun 2008 13:26:13 +0000 (13:26 +0000)]
initial qork for models

16 years agoAdded check of relevance lists for inductive types/constructors and
Wilmer Ricciotti [Tue, 10 Jun 2008 13:15:21 +0000 (13:15 +0000)]
Added check of relevance lists for inductive types/constructors and
fixpoint definitions.

16 years agolebesgue proved
Enrico Tassi [Tue, 10 Jun 2008 11:23:59 +0000 (11:23 +0000)]
lebesgue proved

16 years agosnapshot
Enrico Tassi [Tue, 10 Jun 2008 07:24:46 +0000 (07:24 +0000)]
snapshot

16 years agoMost of the time, URIs can now be replaced with identifiers in "interpretation".
Claudio Sacerdoti Coen [Mon, 9 Jun 2008 20:19:41 +0000 (20:19 +0000)]
Most of the time, URIs can now be replaced with identifiers in "interpretation".
Warning: identifiers are mapped to URIs according to the last declared
alias.

16 years agoIt is now possible to use identifiers in place of URI in "interpreation".
Claudio Sacerdoti Coen [Mon, 9 Jun 2008 20:17:20 +0000 (20:17 +0000)]
It is now possible to use identifiers in place of URI in "interpreation".
The identifier is mapped to an URI according to the last declared alias.

16 years agoReverting to the previous version some files which weren't intended to be
Wilmer Ricciotti [Mon, 9 Jun 2008 16:12:10 +0000 (16:12 +0000)]
Reverting to the previous version some files which weren't intended to be
changed.

16 years agomore proof irrelevance
Wilmer Ricciotti [Mon, 9 Jun 2008 16:02:24 +0000 (16:02 +0000)]
more proof irrelevance

16 years agoinitial work on lebesque
Enrico Tassi [Mon, 9 Jun 2008 14:11:17 +0000 (14:11 +0000)]
initial work on lebesque

16 years agoexhaustivity completed
Enrico Tassi [Mon, 9 Jun 2008 10:24:09 +0000 (10:24 +0000)]
exhaustivity completed

16 years agoexhaustivity, some work
Enrico Tassi [Mon, 9 Jun 2008 08:24:27 +0000 (08:24 +0000)]
exhaustivity, some work

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 18:48:45 +0000 (18:48 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 18:20:20 +0000 (18:20 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:56:36 +0000 (17:56 +0000)]
generalize no more required before elim

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:42:05 +0000 (17:42 +0000)]
generalize no more required before elim

16 years agogeneralize no more required by elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:14:43 +0000 (17:14 +0000)]
generalize no more required by elim

16 years agoGeneralize no more required for elim.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:12:43 +0000 (17:12 +0000)]
Generalize no more required for elim.

16 years agogeneralize no more required before elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 17:06:02 +0000 (17:06 +0000)]
generalize no more required before elim

16 years agogeneralize no more useful for elim
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 14:08:51 +0000 (14:08 +0000)]
generalize no more useful for elim

16 years agoBug fixed: wrong default pattern for generalize.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 14:00:37 +0000 (14:00 +0000)]
Bug fixed: wrong default pattern for generalize.

16 years agoNew: pattern for elim documented.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 13:48:58 +0000 (13:48 +0000)]
New: pattern for elim documented.

16 years agoHypotheses patterns for elim implemented. No more need to generalize in advance.
Claudio Sacerdoti Coen [Sun, 8 Jun 2008 13:44:20 +0000 (13:44 +0000)]
Hypotheses patterns for elim implemented. No more need to generalize in advance.

16 years agoexhaustivity defined
Enrico Tassi [Sat, 7 Jun 2008 16:25:03 +0000 (16:25 +0000)]
exhaustivity defined

16 years agoproof simplified
Enrico Tassi [Sat, 7 Jun 2008 09:57:28 +0000 (09:57 +0000)]
proof simplified

16 years agoEven more Q stuff moved around.
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 18:02:15 +0000 (18:02 +0000)]
Even more Q stuff moved around.

16 years agoEven more Q stuff classified.
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 16:48:01 +0000 (16:48 +0000)]
Even more Q stuff classified.

16 years agolemma 3.6 subverted
Enrico Tassi [Fri, 6 Jun 2008 15:56:00 +0000 (15:56 +0000)]
lemma 3.6 subverted

16 years agomore stuff moved around
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 13:45:38 +0000 (13:45 +0000)]
more stuff moved around

16 years agoMore Q stuff organized in a coherent way.
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 13:26:27 +0000 (13:26 +0000)]
More Q stuff organized in a coherent way.

16 years agoFirst snapshot at trying to clean up the Q library.
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 12:53:35 +0000 (12:53 +0000)]
First snapshot at trying to clean up the Q library.

16 years ago...
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 11:17:53 +0000 (11:17 +0000)]
...

16 years agoA new theorem
Andrea Asperti [Fri, 6 Jun 2008 10:35:16 +0000 (10:35 +0000)]
A new theorem

16 years agocleanup
Andrea Asperti [Fri, 6 Jun 2008 10:21:53 +0000 (10:21 +0000)]
cleanup

16 years agoCleanup.
Andrea Asperti [Fri, 6 Jun 2008 10:21:15 +0000 (10:21 +0000)]
Cleanup.

16 years agosieve.ma now depends only on primes.ma
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 10:07:22 +0000 (10:07 +0000)]
sieve.ma now depends only on primes.ma

16 years agoAdded frac.ma
Andrea Asperti [Fri, 6 Jun 2008 09:20:29 +0000 (09:20 +0000)]
Added frac.ma

16 years agoAdded Qplus_andrea.ma
Andrea Asperti [Fri, 6 Jun 2008 09:03:57 +0000 (09:03 +0000)]
Added Qplus_andrea.ma

16 years agoReduce reduction tactic got rid of a long time ago.
Claudio Sacerdoti Coen [Fri, 6 Jun 2008 08:27:51 +0000 (08:27 +0000)]
Reduce reduction tactic got rid of a long time ago.

16 years agoEratosthene's sieve factorized out of nat/bertrand.ma. Nothing added not
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.

16 years ago....
Enrico Tassi [Thu, 5 Jun 2008 17:11:33 +0000 (17:11 +0000)]
....

16 years agoadded order_continuity
Enrico Tassi [Thu, 5 Jun 2008 15:41:15 +0000 (15:41 +0000)]
added order_continuity

16 years agosandwich is back
Enrico Tassi [Thu, 5 Jun 2008 15:28:56 +0000 (15:28 +0000)]
sandwich is back

16 years agoProof-irrelevance check for all applications (first version)
Wilmer Ricciotti [Wed, 4 Jun 2008 22:53:08 +0000 (22:53 +0000)]
Proof-irrelevance check for all applications (first version)

16 years agoincomplete irrelevance test commented out
Wilmer Ricciotti [Wed, 4 Jun 2008 15:22:50 +0000 (15:22 +0000)]
incomplete irrelevance test commented out

16 years agoSome proofs on enumerator and denominator.
Claudio Sacerdoti Coen [Tue, 3 Jun 2008 22:50:48 +0000 (22:50 +0000)]
Some proofs on enumerator and denominator.

16 years agoMore work on rational numbers with unique representations.
Claudio Sacerdoti Coen [Tue, 3 Jun 2008 21:58:35 +0000 (21:58 +0000)]
More work on rational numbers with unique representations.

16 years agosome work on uniformity
Enrico Tassi [Tue, 3 Jun 2008 15:56:51 +0000 (15:56 +0000)]
some work on uniformity

16 years agoend of section 2.2
Enrico Tassi [Tue, 3 Jun 2008 12:09:21 +0000 (12:09 +0000)]
end of section 2.2

16 years agoproof refactored
Enrico Tassi [Tue, 3 Jun 2008 08:12:57 +0000 (08:12 +0000)]
proof refactored

16 years agoxxx
Enrico Tassi [Tue, 3 Jun 2008 08:12:38 +0000 (08:12 +0000)]
xxx

16 years agomore work on supremum
Enrico Tassi [Sun, 1 Jun 2008 15:38:46 +0000 (15:38 +0000)]
more work on supremum

16 years agoCProp hierarchy is there!
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

16 years agoirrelevance check half implemented but already impossible to
Enrico Tassi [Fri, 30 May 2008 19:21:51 +0000 (19:21 +0000)]
irrelevance check half implemented but already impossible to
complete

16 years ago...
Enrico Tassi [Fri, 30 May 2008 17:08:26 +0000 (17:08 +0000)]
...

16 years agogarbage removed
Enrico Tassi [Fri, 30 May 2008 14:28:08 +0000 (14:28 +0000)]
garbage removed

16 years agomore work on dama
Enrico Tassi [Fri, 30 May 2008 14:27:41 +0000 (14:27 +0000)]
more work on dama

16 years agoprod moved under lambda-prolog unification case
Enrico Tassi [Fri, 30 May 2008 10:28:13 +0000 (10:28 +0000)]
prod moved under lambda-prolog unification case

16 years agoadded CProp
Enrico Tassi [Fri, 30 May 2008 10:08:22 +0000 (10:08 +0000)]
added CProp

16 years agothanks to the fact that we convert well typed term and that
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

16 years agoadded a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now...
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

16 years agorelevance check partially implemented but bugged since cic:/matita/nat/compare/eqb...
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!

16 years agocase not unfilding fixed
Enrico Tassi [Thu, 29 May 2008 16:34:08 +0000 (16:34 +0000)]
case not unfilding fixed

16 years agoCProp, since it was defined in CoRN as a Type, is predicative.
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).

16 years ago0.5.1 released
Enrico Tassi [Thu, 29 May 2008 14:15:25 +0000 (14:15 +0000)]
0.5.1 released

16 years agounused variables removed
Enrico Tassi [Thu, 29 May 2008 12:28:32 +0000 (12:28 +0000)]
unused variables removed

16 years agoref sync check fixed controlling fix/cofix coherence
Enrico Tassi [Thu, 29 May 2008 11:51:14 +0000 (11:51 +0000)]
ref sync check fixed controlling fix/cofix coherence

16 years ago...
Enrico Tassi [Thu, 29 May 2008 11:38:44 +0000 (11:38 +0000)]
...

16 years agofirst page of the new dama proof
Enrico Tassi [Thu, 29 May 2008 09:51:22 +0000 (09:51 +0000)]
first page of the new dama proof

16 years ago...
Enrico Tassi [Thu, 29 May 2008 09:45:35 +0000 (09:45 +0000)]
...

16 years agothe type of the match was obtained reducing the outtype
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.

16 years ago...
Enrico Tassi [Wed, 28 May 2008 12:48:43 +0000 (12:48 +0000)]
...

16 years agodama restarted
Enrico Tassi [Wed, 28 May 2008 11:00:26 +0000 (11:00 +0000)]
dama restarted

16 years agocleanup
Enrico Tassi [Wed, 28 May 2008 10:40:54 +0000 (10:40 +0000)]
cleanup

16 years agothe attempt of completing dama using duality frozen
Enrico Tassi [Wed, 28 May 2008 10:39:13 +0000 (10:39 +0000)]
the attempt of completing dama using duality frozen

16 years ago0.5.1
Enrico Tassi [Wed, 28 May 2008 10:11:11 +0000 (10:11 +0000)]
0.5.1

16 years ago...
Enrico Tassi [Tue, 27 May 2008 15:47:54 +0000 (15:47 +0000)]
...

16 years agosmarter lexer needed by lambda-delta that is splitting "let rec" statements
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

16 years ago...
Enrico Tassi [Tue, 27 May 2008 10:56:02 +0000 (10:56 +0000)]
...

16 years agoCoRN moved in contribs
Enrico Tassi [Tue, 27 May 2008 08:51:59 +0000 (08:51 +0000)]
CoRN moved in contribs

16 years agofrst step to move away the CoRN stuff
Enrico Tassi [Tue, 27 May 2008 08:47:27 +0000 (08:47 +0000)]
frst step to move away the CoRN stuff

16 years agofrst 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

16 years agoauto calls cleanup\
Enrico Tassi [Tue, 27 May 2008 08:36:21 +0000 (08:36 +0000)]
auto calls cleanup\

16 years agobetter description of declarative tactics
Enrico Tassi [Mon, 26 May 2008 16:33:07 +0000 (16:33 +0000)]
better description of declarative tactics

16 years agonew, more rigid syntax, for auto_params affecting the declarative language.
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.

16 years agoUniverse.key was not used to index terms, but was used to retrieve them
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

16 years agobetter presentation of lambda-delta
Ferruccio Guidi [Mon, 26 May 2008 13:43:02 +0000 (13:43 +0000)]
better presentation of lambda-delta

16 years ago- some bugs fixed in the domain-based preorders on environments
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

16 years agoadded comment for zack
Enrico Tassi [Mon, 26 May 2008 10:43:31 +0000 (10:43 +0000)]
added comment for zack