A primer for Matita with some easy, medium, difficult and impossible exercises.

We define proof tree tracks and normal proof tree tracks separately

refactoring

proof by "introduction" (impi) implemented in full

thread-based interface activated again

Bug fixed: RewriteLR were not recognized correctly. Moreover they were also
handled incorrectly (according to the is_top_down flag that should be irrelevant).

Bug fixed: the initial metasenv used in the two tactic was empty!

Avoid reusing Hbeta several times.

select now works correctly even if multiple hypotheses with the same name are
present in the context.

Avoid confusion for names of proofs put in the applicative context.

"obtain H E1=E2 by proof" is now working

little change to theorem eq_gcd_times_times_eqv_times_gcd

removed generic_sigma_p since generic_iter_p is the same

something was really too slow...

default equality stuff filtered out from hint rewrite

removed comments in proof presentation

renamed generic_sigma_p.ma to generic_iter_p.ma

added 'rewrite' option to the the hint macro. a cicBrowser with all library
objects that may rewrite the goal is displayed.

We add a binary for computing the "heights" of helm objects
[this is related to the height of the dependece tree]

added development path normalization, inclusions with '../' in the path should now be handled correclty

auto -> autobatch

Some notation added

more stuff about coercions

little bug in coercion generation found. it use to create more coercions that expected (luckily convertible).

makefiles updated

makefile updated

matitac: We do not generate the .moo and .lexicon of a dumped .mma
Base-2 : makefile patched

added some notation

added another example in which our coercions are powerful

used ;try assumption instead of .try assumption

; and not . after auto-paramodulation

reverted previous fix

restored compaction of metas at the end of given_clause

Makefile missing in previous commit

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)

added test about dependent coercions

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.

auto vs autobatch fixed

autobatch parameters reajusted

fixed makefiles to make it compile cleanly again

Procedural: the statement body and it inner types must satisfy the Barendregt
            convenction on bound variables

Another nicer version.

Even nicer script.

The nicest script obtained so far.
What is left, is a bunch of change/normalize/whd/simplify that are difficult
to control precisely.

acic_procedural: bug fix:
                 sometimes whd is not enough, we need normalize ...

More simplification due to the new conversion strategy.

Script simplification due to the new efficient conversion strategy.

Tentative bug fix for diverging pretty-printing function.

Initialization of matita.map_unicode_to_tex moved from matitaGui to matitaInit
(so that ocamlc now works again).

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

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.

map_unicode_to_tex is no longer optional and it always refers to the current
user choice.

paste_unicode_as_tex is now false by default; moreover the flag is used
everywhere (but in patterns, I do not know why)

COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.

the cade was escaping the table name and not the uri

fixed escaping for sqlite

fixed an escaping error, added more infos to the generic error, callback catches and prints exceptions

Typo fixed.

Super-nice notation for the assembly stuff.

the predicate for elim was not built correctly when more than one right parameter was found

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

fixed coercion graph print, moved coercion graph and auto gui to the view menu, added a mini test about coercions

added missing parenthesis

fixed includes and added notation for bytes

More lemmas.

More daemons closed. A couple left in byte and many in extras.

More daemons/axioms closed.

One daemon less.

More daemons got rid of (and more extra axioms to be proved).

Last daemon killed :-)

One less daemon (about "update"s).

All sub-proofs about "update" closed.

assembly.ma splitted into many files

* NOT RELEASED YET

* NOT RELEASED YET

proper path for ps.gz doc

texlive-base-bin, texlive-latex-extra

  - add build-dep for doc generation: graphviz, texlive-latex-recommended,

  - add build-dep for doc generation: graphviz, texlive-latex-base,
    texlive-base-bin

* debian/rules
  - build ocamldoc documentation at package build time
  - add build-dep on graphviz

invoke make doc after build to create ocamldoc docs

* debian/svn-deblayout
  - add repository layout information

* 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

* debian/*.install.in
  - do not attempt to instal *.ml files in target lib directory since they
    are no longer installed by Makefile

* rebuild with OCaml 3.10
* bump debhelper deps and compatibility level to 5
  - s/Source-Version/binary:Version

corrected axiom mod_plus

new definitions and new theorems

More conjectures closed.

1. requires the new pretty printer for natural numbers
2. important properties of plusbyte proved
3. all important conjectures almost proved

Dirty patch by Zack: natural numbers of Matita are now pretty-printed as numbers. Eureka.

Last crazy commit reverted.

Final theorem proved. Many many conjectures left. I am unsure of one of them.

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)

Getting close to the final result.
The showstopper now is the GtkMathView/Pango bug!
Moreover, unification has become mostly useless (and rewriting with it).

1. loop invariant stated, but not proved
2. final theorem stated and proved

native dependences fixed

1. status factorized out in tick
2. 0*0=0, 0*2=0, x*1=x, x*2=x+x proved
3. still way too slow!

auto new => autobatch

auto new => autobatch

0. less nice solution by Enrico reverted
1. some bug fixes in assembly code
2. test program simplified
3. reduction now works as expected, thanks to the new reduction strategy
4. BIG BUG SOMEWHERE: (270 \mod 256) reduces to 14 instead of 4!!!
5. requires primitive addition over exadecimal numbers and bytes to
   avoid representing 0+x as byte_of_nat (nat_of_byte x) that does not
   reduce