when -debug do not catch

when -debug do not catch

replace assert false with AssertFailure

Initial version of the Helena Checker
- For now just parses an automath book (automath grammar by F. Wiedijg)
  the grundlagen is provided as (the only existing) example
- In the future will convert an automath book to a lambda-delta environment
  several lambda-delta extensions will be supported

New lemma
theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

more notation

...

print the name not found in the env

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 :-(

better names in a lemma to increase readability

fixed some regressions

New, much faster implementation of factorize.

gran casino

meta not considered before in outtype

bla bla bla

relevance check for Match

initial qork for models

Added check of relevance lists for inductive types/constructors and
fixpoint definitions.

lebesgue proved

snapshot

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.

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.

Reverting to the previous version some files which weren't intended to be
changed.

more proof irrelevance

initial work on lebesque

exhaustivity completed

exhaustivity, some work

generalize no more required before elim

generalize no more required before elim

generalize no more required before elim

generalize no more required before elim

generalize no more required by elim

Generalize no more required for elim.

generalize no more required before elim

generalize no more useful for elim

Bug fixed: wrong default pattern for generalize.

New: pattern for elim documented.

Hypotheses patterns for elim implemented. No more need to generalize in advance.

exhaustivity defined

proof simplified

Even more Q stuff moved around.

Even more Q stuff classified.

lemma 3.6 subverted

more stuff moved around

More Q stuff organized in a coherent way.

First snapshot at trying to clean up the Q library.

...

A new theorem

cleanup

Cleanup.

sieve.ma now depends only on primes.ma

Added frac.ma

Added Qplus_andrea.ma

Reduce reduction tactic got rid of a long time ago.

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.

....

added order_continuity

sandwich is back

Proof-irrelevance check for all applications (first version)

incomplete irrelevance test commented out

Some proofs on enumerator and denominator.

More work on rational numbers with unique representations.

some work on uniformity

end of section 2.2

proof refactored

xxx

more work on supremum

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

irrelevance check half implemented but already impossible to
complete

...

garbage removed

more work on dama

prod moved under lambda-prolog unification case

added CProp

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

added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now is full whd

relevance check partially implemented but bugged since cic:/matita/nat/compare/eqb.con is not ok!

case not unfilding fixed

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).

0.5.1 released

unused variables removed

ref sync check fixed controlling fix/cofix coherence

...

first page of the new dama proof

...

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.

...

dama restarted

cleanup

the attempt of completing dama using duality frozen

0.5.1

...

smarter lexer needed by lambda-delta that is splitting "let rec" statements
on multiple lines

...

CoRN moved in contribs

frst step to move away the CoRN stuff

frst step to move away the CoRN stuff

auto calls cleanup\

better description of declarative tactics

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.