This is the roadmap of the constructive proof of Lebesgue's dominated
convergence theorem in the order theoretic setting. I.e. we speak of
convergence (in terms of liminf and limsup) and not of norms/measures.

The formulation should be fully constructive:
 1. the exceeds relation is used in place of the derived negative notion
    <= for partial orders
 2. strong sup and infs are used in place of the weaker sup and infs
 3. the statement of Lebesgue's dominated converge theorem is just
    extensionality of the functional
      \lambda f. liminf f a_n
    with respect to the apartness relation # over real numbers and the
    exceeds/apartness relation over partial orders.

Interesting points to be noticed:
 a) one lemma used in the proof is Fatou. This lemma can be given in the
    usual negative formulation (i.e. on <=)
 b) another lemma used in the proof is that the liminf is less or equal to
    the limsup. This lemm can be given in the usual negative formulation
    (i.e. on <=). Moreover, we feel that if <= is not defined as
    ~< it is actually impossible to constructively prove it.

CoRN (new version) has been committed by Andrea in library/algebra/CoRN.

Added SetoidInc.m

Some CoRN files.

procedural: added fwd rewrite in arbitrary proofs (not just premises)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.

procedural: buggy ast renderer fixed

attributes now in the proof status: commit 4

attributes now in the proof status: commit 3

attributes now in the proof status: commit 2

attributes now in the proof status: commit 1

Porting of setoids.ma from Coq continued.
The fact that simplification does not work properly slows down the whole
process.

Bug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
two generalizes were done in the wrong order, permuting the arguments and
making every relation change its variance!

- inside dicrimination_tree is now checked the invariant that bad terms are indexed, but this invariant is not always respected, so a 'Dead' representative is used and a warning is printed.
- autoCache (should) not index bad terms

;auto fixed

removed debugging printing

debuggin message improved

add_moo_content does not add a coercion statement twice

Added check for duplicate (convertible) composite coercions,
that are not added anymore.
Nicer api for meets used by unification.

Erroneously declared coercion removed

ready for ocamlnet 2.2

more elegant handling of all/opt building

Notation is finally fully working everywhere.
What a great day!

Debugging code removed.

Riesz_spaces are now seen as lattices + vector spaces + ordered abelian groups.

oder tests

There used to be two minimal joins between an ordered_set and an abelian_group:
ordered_field_ch0 and riesz_space. To avoid the problem without introducing
backtracking in unification I have introduced ordered_abelian_groups.
An ordered_field_ch0 is recast as a field that is also an ordered_abelian_group
and a cotransitively_ordered_set. I still have to recast riesz_spaces as
vector spaces that are also ordered_abelian_groups and lattices.

Same fix of the previous commit, but in a different case.

1. More debugging code
2. "Bug" "fixed": when the pullback of two coercions is computed, only the
   join is returned, but not the two coercions that complete the pullback.
   Thus we need to recompute them and it may happen that we find more than one
   parallel coercions. This "fix" just randomly picks the first one (instead
   of raising an assert false). All this stuff must be handled in a better way.

added oblivion_universe and used it in paxck_coercions

some tests patched

Some more notation can now be used.
However, in integration_algebras.ma there are several situations where
multiple meets are found and notation cannot be used.

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