le x y ==> x \leq y  (now possible because of a bug fix in coercion
serialization in .moo files)

Serious bug fixed: arities of coercions in the .moo files were not computed
correctly. Thus including another file a bugged coercion graph was produced,
with randomic effects quite hard to understand. (Examples in dama where
it was not possible to use <= in place of le here and there because of a
coercion with the wrong arity).

 dependence to legacy/coq.ma fixed

now we try two distinct depend files for compilation in byte and native code

Record with simulated manifest types are now used everywhere in
integration_algebras.ma. They seem to work really very well (up to missing
but due syntactic sugar).

First attempt at using/simulating records with manifest types to encode
mathematical structures that form a DAG. So far it works quite well,
but the generation of the "coerced" projection should be automated.
Something to write a paper on.

eq_ind' generalized to eq_rect'

- tactics:
  rename tactic enabled,
  rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
  now starts directly from acic bypassing the content level,
  the script for the use case proof in matita/contribs/prova.ma is reconstructed  completely now and is correctly parsed and typechecked

Yet another localization error in eat_prods fixed.
However, the fix is very very ugly (it uses unsharing) and clearly shows
a source of inefficiency (and possibly also divergence, I would say).

.depends committed to fix non-compilation errors

some depend files

legacy development created

- sc3/props.ma sc3/arity.ma: dependences fixed
- csubc/arity.ma csubc/csuba.ma: reverted as no fix was needed

Add_moo_content modified to avoid repetitions of index command during inclusion.

Minor change.

Collapse_head_metas transforms all terms "not-recongnized" into a
meta.

In the let-in case we compute the type and add it to the context.
Before it was computed every time

The function uri_of_term now works also if the explciit substitution list
is not empty.

Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.

added some missing includes

New declarative tactic "we proceed by cases on t to prove t'".
Very unsatisfactory since it already introduces the hypothesis in advance,
actually ignoring the following "case S (n:nat)" declarative command.
I do not see any easy solution at all.

Bug fixed in cases (it did not produced the right number of lambdas for the
outtype of dependent inductive types).

Tactic cases documented

New tactic cases (still to be documented).
It is necessary for the declarative language and it is useful anyway.

Procedural: method "Apply" ok in forward style

Procedural:   "ByInduction" method ok
GrafiteAstPp: letin tactic now works

An idea to implement manifest record fields:
record r : R := { c1 : T1 ; c2 : T2 with f c1 = g c2 }.

Only the syntactic sugar is actually missing!

Procedural: some improvements

M    logic/coimplication.ma

Renamed iterative into map_iter_p and moved around a few theorems.

Proof of Euler theorem.

Up to definition of limsup as liminf computed on the reverse ordering.
However, I am no longer sure that this is the best way to proceed since
the lemmas to be proved are a lot and the typing is difficult. However,
this work should be done anyway to state limsup f x = - liminf f (-x)
that we need anyway.

Fatou lemma achieved (up to a few more axioms here and there...)

Huge DAMA update:
 1. up to Fatou lemma (almost there)
 2. requires the new unification procedure for coercions to enable
    multiple coercion paths between two nodes
 3. it stresses CicUniv.mere_ugraphs. To compile the new DAMA file quickly
    you have to disable that function :-(

Bugged code patched, but not in the optimal way.
The problem is that in two different interpretations a symbol id can be
interpreted as dsc in different locations. Using the previous code it
happened that every interpretation was pruned out since a symbol id occurred
twice (in different locations) in an/every interpretation. Now the couples
(loc,id) are considered for disambiguating between the two interpretations.
However, this way we hide information to the user (what other occurrences of
the same symbol are given the same interpretation).

Debugging code commented out.

...

...

...

content2Procedural.ml: "Intros+LetTac" ok

Huge commit:

 1. coercGraph.ml* moved from library to cic_unification (where it should
    have been put in the first place). A few functions that must remain in
   library moved to coercDb.ml* (where they should have been put in the first
   place)
 2. ProofEngineHelpers.saturate_term moved from tactic to cic_unification.
 3. Bug fixed in saturate_term: the newmeta returned by the function was not
    correct in some cases
 4. CoercGraph.look_for_coercion* used to saturate the coercion with implicit
    arguments (thus requirin a refinement pass later on). Now the same
    functions saturate the term with metas. The return type has changed
    accordingly.
 5. the horrible hack to break composite coercions during unification has been
    replaced by a nice implementation of unification towards the join of the
    two coercions (called meet by Enrico I do not know why :-).
    This solves many many problems found using multiple coercion pathes from
    a source to a destination. (This is the case in DAMA that I am going to
    commit soon).

- transcript: patched to generate aliases instead of inlined variables
- CoRN-Decl: regenerated with aliases instead of inlined variables
- content2Procedural: improved but not working yet

we parametrized CicNotationPt.obj on 'term

we started the infrastructure for the procedural rendering of proofs

we exported some inversors from coq

EXPERIMENTAL:
 1. the disambiguation domain is now a tree that partially reflects the
    applicative structure of the term
 2. disambiguation now classifies errors according to the following criterium:
    an error E is considered not significant when it belongs to the set A of
    results (obtained interpreting a symbol and its subterms in every possible
    way) and there exists at least a result in A that is either OK or Uncertain.
    A "subterm" is implicitly defined by the tree structure of the
    disambiguation domain.
 3. WARNING: there used to be an (important ????) optimization that has not
    been ported (yet ???): if the next item in the disambiguation domain can
    be interpreted in just one way, we skip the current refinement step.
    According to tests on my laptop the optimization does not seem to be
    really so significant (sometimes it even slow down???). We will decide
    on monday whether porting it or not. Porting it is not very simple because
    of the new data structures involved.

Disambiguation errors in phase 3 that are not present in phase 4 are filtered
out. Explanation: if they are only in phase 3, it means that in phase 4 they
are not significative. Thus we conclude that phase 3 is not significative.
There is a drawback: equality over errors is not very well defined because
of Metas in error messages. Thus it could be the case that we remove the error
in phase 3 when the same error is still there in phase 4.

new makefiles

reverted error committed by mistake

avoid Failure "nth" when only one disambiguation pass is enabled

new theorems added. does not comile well yet :(( problems found in
- csubc/csuba.ml (exception "List.nth" raised by matitaGui.ml at line 244)
- ty3/pr3.ml (matitac.opt returns with exit code 3 without evident error)
- sn3/props.ma (assertion failure raised by discrimination_tree.ml at line 62)

Experimental: cycles in proofs generated by paramodulation are now detected
and removed.
However, letins that become useless after this operation are not simplified.
Simplifying them (when they became linear) could introduce more cycles that
require a second simplification and so on.

More simplification using better notation.

interactive and bad_tests grepped out before insertion in the DB

experimental classification of disambiguation error, so that supposedly non significant errors can be hidden to the user
ATM an error is non significant if obtained interpretating a symbol that can be interpreted in an error-free way

- components: composed coercions mus be generated with current base uri
- transcript: fixed to handle coercions from constructors
- CoRN-Decl: regenerated. CoRN.ma now compiles!

do not share the db connection among children, should fix the "server has gone away" error

prova.ma: baseuri fixed
Unified: flat contexts added

some uris fixed

Even if automatically generated, I prefer to commit the quickref help files
since they require some ad-hoc programs to be generated.

Notation \middot used everywhere in place of *.

I have changed the nice notation for derivatives a little bit to always pick
'x' as the default variable. This is the only reasonable choice since we already
always pick 'x' for polynoms.

Added a demo for Matita: two slightly different proofs in declarative language
that the derivative of x^n is n*x^(n-1). The real numbers, the definition of
derivative and some basic properties of derivatives are axiomatized. Two
alternative notations are proposed for the derivatives. (The somehow nicer
one is currently bugged.)

Syntax of a declarative rewritinstep changed.

library/Fsub: minor fix

library: added solution to POPLMark challenge part 1a (transitivity of Fsub subtyping)

New syntax and semantics for the rewriting steps that make the pretty-printed
proof similar to the input proof.

Syntax:

((obtain id | conclude) lhs) = rhs done?

Semantics:
use conclude when working top-down and obtain to work bottom-up.
done means that this was the last step.

The auto parameters that can be given to a declarative rewritingstep must now
be put in parenthesis (to avoid "eating" the "done" token).

The rewritingstep declarative command now takes also a list of arguments
that are passed to paramodulation (after adding paramodulation=1 and
timeout=3 if these parameters are not already forced by the user).

- new library/logic/coimplication.ma uses new decompose tactic
- matitaScript.ml: new parameter of inline tactic now ignored
- CoRN-Decl: regenerated with local objects handled correctly

- decompose tactic: decomposable constants are now allowed (they are unfolded)
- inline macro: now accepts an optional name prefix for disambiguation purposes
- transcript: now handles local objects correctly

Demodulate_tac now depends on the universe

Added a clear to rewritestep to speed up auto (by removing an hypothesis
that must NOT be used again).

Changed an ahstable into an association list.

"the thesis becomes" now always performs a change.

Fixed bug in notation: when a notation is applied to more arguments than expected this is not necessarily a problem: I just create a new application on the fly.

Added in_eq_uris.

Fix_proof should recursively work on explicit substs.
For the moment this is done for constants.

Declarative language ported to new auto (with Universes).

Removed a couple of assertions.

Commented an assertion.

Commented an assertion.

Commented a few assertions.

Variant are not indexed.

Only modified for taking unfold into account.
Assertion made only in case of debug.

Matita's default equality has changed
-This line, and those below, will be ignored--

M    library/logic/equality.ma

Small changes

auto new => auto new library in those tests that use Coq's library

fix

patch to calculate meets of a pair of carriers

added assertion (that is a TODO) in case non-considered exceptions are raised when tring to apply coercions

added a test for the pullback stuff and the possibility to get the coercion graph printed without closures

Command index added to disambiguate.
-This line, and those below, will be ignored--

M    grafite_parser/grafiteDisambiguate.ml

Added a new command "index" for the indexing terms in the "universe".

Set of Set of uri added.

Modifications to auto due to the introduction of the universe in
the status.

Universe is a discrimination-tree structure.

The status has been extended with a "universe", that is a
discrimination-tree structure indexing all defined objects.
The universe is functional (hope so).

Fixed a call to auto, and commented the remaining part.

paramodulation removed