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

Minor changes.
-This line, and those below, will be ignored--

M    library/nat/ord.ma
M    library/nat/gcd.ma
M    library/nat/factorization.ma
M    library/technicalities/setoids.ma

Simplified version.

Adding CoRN.

removed the impredicativity of falsum

Fixed the infamous bug:
> >/home/sacerdot/miohelm/matita/scripts/crontab.sh: line 70: [: : integer
> >expression expected

helm_registry: added the pair unmarshaller
grafiteAstPp: bug-fixed
transcript: coercion handling improved
CoRN-Decl: regenerated accordingly
--ehis line, and those below, will be ignored--

M    software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma
M    software/matita/contribs/CoRN-Decl/devel/loeb/per/lst2fun.ma
M    software/matita/contribs/CoRN-Decl/devel/loeb/IDA/Ch6.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Zgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Qgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/Qposgroup.ma
M    software/matita/contribs/CoRN-Decl/model/groups/QSposgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/QSposabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Zabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Qabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/abgroups/Qposabgroup.ma
M    software/matita/contribs/CoRN-Decl/model/rings/Zring.ma
M    software/matita/contribs/CoRN-Decl/model/rings/Qring.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Nsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Npossec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Qsec.ma
M    software/matita/contribs/CoRN-Decl/model/structures/Qpossec.ma
M    software/matita/contribs/CoRN-Decl/model/fields/Qfield.ma
M    software/matita/contribs/CoRN-Decl/model/reals/Cauchy_IR.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Nmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Nposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Qmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Qposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/QSposmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/monoids/Zmonoid.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/N_no_group.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_group.ma
M    software/matita/contribs/CoRN-Decl/model/non_examples/Npos_no_monoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Nsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Npossetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Qsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.ma
M    software/matita/contribs/CoRN-Decl/model/setoids/Zsetoid.ma
M    software/matita/contribs/CoRN-Decl/model/ordfields/Qordfield.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Zsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Nsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Npossemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Qsemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/Qpossemigroup.ma
M    software/matita/contribs/CoRN-Decl/model/semigroups/QSpossemigroup.ma
M    software/matita/contribs/CoRN-Decl/metrics/CMetricSpaces.ma
M    software/matita/contribs/CoRN-Decl/metrics/IR_CPMSpace.ma
M    software/matita/contribs/CoRN-Decl/metrics/Equiv.ma
M    software/matita/contribs/CoRN-Decl/metrics/ContFunctions.ma
M    software/matita/contribs/CoRN-Decl/metrics/CPMSTheory.ma
M    software/matita/contribs/CoRN-Decl/metrics/Prod_Sub.ma
M    software/matita/contribs/CoRN-Decl/metrics/CPseudoMSpaces.ma
M    software/matita/contribs/CoRN-Decl/reals/iso_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
M    software/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
M    software/matita/contribs/CoRN-Decl/reals/CReals1.ma
M    software/matita/contribs/CoRN-Decl/reals/Series.ma
M    software/matita/contribs/CoRN-Decl/reals/NRootIR.ma
M    software/matita/contribs/CoRN-Decl/reals/CPoly_Contin.ma
M    software/matita/contribs/CoRN-Decl/reals/IVT.ma
M    software/matita/contribs/CoRN-Decl/reals/RealLists.ma
M    software/matita/contribs/CoRN-Decl/reals/Max_AbsIR.ma
M    software/matita/contribs/CoRN-Decl/reals/Cauchy_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/RealFuncts.ma
M    software/matita/contribs/CoRN-Decl/reals/Intervals.ma
M    software/matita/contribs/CoRN-Decl/reals/OddPolyRootIR.ma
M    software/matita/contribs/CoRN-Decl/reals/CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/CMetricFields.ma
M    software/matita/contribs/CoRN-Decl/reals/Q_dense.ma
M    software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
M    software/matita/contribs/CoRN-Decl/reals/R_morphism.ma
M    software/matita/contribs/CoRN-Decl/reals/CSumsReals.ma
M    software/matita/contribs/CoRN-Decl/reals/Bridges_LUB.ma
M    software/matita/contribs/CoRN-Decl/complex/NRootCC.ma
M    software/matita/contribs/CoRN-Decl/complex/CComplex.ma
M    software/matita/contribs/CoRN-Decl/complex/AbsCC.ma
M    software/matita/contribs/CoRN-Decl/complex/Complex_Exponential.ma
D    software/matita/contribs/CoRN-Decl/CoRN_notation.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Shift.ma
M    software/matita/contribs/CoRN-Decl/fta/KneserLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/KeyLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/CC_Props.ma
M    software/matita/contribs/CoRN-Decl/fta/FTAreg.ma
M    software/matita/contribs/CoRN-Decl/fta/FTA.ma
M    software/matita/contribs/CoRN-Decl/fta/MainLemma.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Contin1.ma
M    software/matita/contribs/CoRN-Decl/fta/CPoly_Rev.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics1.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics2.ma
M    software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma
M    software/matita/contribs/CoRN-Decl/tactics/GroupReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Opaque_algebra.ma
M    software/matita/contribs/CoRN-Decl/tactics/RingReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Step.ma
M    software/matita/contribs/CoRN-Decl/tactics/AlgReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/FieldReflection.ma
M    software/matita/contribs/CoRN-Decl/tactics/Transparent_algebra.ma
M    software/matita/contribs/CoRN-Decl/transc/RealPowers.ma
M    software/matita/contribs/CoRN-Decl/transc/TaylorSeries.ma
M    software/matita/contribs/CoRN-Decl/transc/Trigonometric.ma
M    software/matita/contribs/CoRN-Decl/transc/Exponential.ma
M    software/matita/contribs/CoRN-Decl/transc/PowerSeries.ma
M    software/matita/contribs/CoRN-Decl/transc/Pi.ma
M    software/matita/contribs/CoRN-Decl/transc/InvTrigonom.ma
M    software/matita/contribs/CoRN-Decl/transc/SinCos.ma
M    software/matita/contribs/CoRN-Decl/transc/TrigMon.ma
M    software/matita/contribs/CoRN-Decl/ftc/IntervalFunct.ma
M    software/matita/contribs/CoRN-Decl/ftc/DerivativeOps.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreFunSeries.ma
M    software/matita/contribs/CoRN-Decl/ftc/COrdLemmas.ma
M    software/matita/contribs/CoRN-Decl/ftc/TaylorLemma.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSums.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefLemma.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSeries.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreIntervals.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSeparating.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreFunctions.ma
M    software/matita/contribs/CoRN-Decl/ftc/Partitions.ma
M    software/matita/contribs/CoRN-Decl/ftc/Differentiability.ma
M    software/matita/contribs/CoRN-Decl/ftc/PartFunEquality.ma
M    software/matita/contribs/CoRN-Decl/ftc/StrongIVT.ma
M    software/matita/contribs/CoRN-Decl/ftc/Derivative.ma
M    software/matita/contribs/CoRN-Decl/ftc/Composition.ma
M    software/matita/contribs/CoRN-Decl/ftc/Integral.ma
M    software/matita/contribs/CoRN-Decl/ftc/Continuity.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSeparated.ma
M    software/matita/contribs/CoRN-Decl/ftc/FunctSequence.ma
M    software/matita/contribs/CoRN-Decl/ftc/Taylor.ma
M    software/matita/contribs/CoRN-Decl/ftc/WeakIVT.ma
M    software/matita/contribs/CoRN-Decl/ftc/MoreIntegrals.ma
M    software/matita/contribs/CoRN-Decl/ftc/PartInterval.ma
M    software/matita/contribs/CoRN-Decl/ftc/FTC.ma
M    software/matita/contribs/CoRN-Decl/ftc/NthDerivative.ma
M    software/matita/contribs/CoRN-Decl/ftc/Rolle.ma
M    software/matita/contribs/CoRN-Decl/ftc/RefSepRef.ma
M    software/matita/contribs/CoRN-Decl/ftc/CalculusTheorems.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdCauchy.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoidInc.ma
M    software/matita/contribs/CoRN-Decl/algebra/CAbGroups.ma
M    software/matita/contribs/CoRN-Decl/algebra/CRings.ma
M    software/matita/contribs/CoRN-Decl/algebra/Expon.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSums.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdFields2.ma
M    software/matita/contribs/CoRN-Decl/algebra/CLogic.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_Degree.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_NthCoeff.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma
M    software/matita/contribs/CoRN-Decl/algebra/Cauchy_COF.ma
M    software/matita/contribs/CoRN-Decl/algebra/Basics.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.ma
M    software/matita/contribs/CoRN-Decl/algebra/CPolynomials.ma
M    software/matita/contribs/CoRN-Decl/algebra/CFields.ma
M    software/matita/contribs/CoRN-Decl/algebra/CMonoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdAbs.ma
M    software/matita/contribs/CoRN-Decl/algebra/CSetoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/ListType.ma
M    software/matita/contribs/CoRN-Decl/algebra/COrdFields.ma
M    software/matita/contribs/CoRN-Decl/algebra/CAbMonoids.ma
M    software/matita/contribs/CoRN-Decl/algebra/CVectorSpace.ma
M    software/matita/contribs/CoRN-Decl/algebra/CGroups.ma
A    software/matita/contribs/CoRN-Decl/CoRN.ma
M    software/components/grafite/grafiteAstPp.ml
M    software/components/binaries/transcript/CoRN.conf.xml
M    software/components/binaries/transcript/grafite.ml
M    software/components/binaries/transcript/v8Parser.mly
M    software/components/binaries/transcript/types.ml
M    software/components/binaries/transcript/engine.ml
M    software/components/registry/helm_registry.ml
M    software/components/registry/helm_registry.mli

CoRN-Decl: missing file added

- transcript: patched to generate CoRN_notation.ma instead of CoRN.ma
- CoRN-Decl: regenerated

- transcript: now outputs includes and coercions correctly
- GrafiteAstPp: coercion and inline pretty printing patched
- CoRN-Decl: regenerated: starts to compile :) but inline is broken :(

new CoRN development, generated by transcript

transcript updated

removed prived CoRN configuration file :)

transcript: very alpha version.
parser for Coq V8 works fine on CoRN contribution scripts.

fixed base uri

lt_O_S moved to nat/orders.ma

Added lt_O_S.

&TODO => &TODO;

New: on-line help for declarative tactics (first version).

library=1 in obtain _ = _ by _.

The pretty printers in CicPp now have an optional ~metasenv argument to
show the globally restricted arguments of a metavariable local context as
locally restricted. The pretty printers in CicMetaSubst have the same argument,
but the argument is mandatory.

NLE is now derived fron NPlus rather than being a stand-alone relation

Dama: up to L-spaces and the proof (completed up to properties of the
absolute value) that every complete integration riesz space is an L-space.
Now the plan is to prove the Lebesgue dominated convergence theorem for
L-spaces as Fremlin does and to build a model of them later on as suggested
by Spitters. Note: the proof of the theorem by Spitters is almost trivial
because it really exploits the fact the L0 is the (Cauchy) completion of L1.
The proof by Fremlin is much more general since it does not assume anything
more on L-spaces.

Note: we could also prove that every L-space is archimedean.

More work on groups, real numbers and integration algebras.
Up to a thousand of unproved lemmas, we have the result that the
distance induced by the integral on an integration Riesz space is
a distance. The next step is to axiomatise an L-space (an integration
Riesz space complete w.r.t. the induced distance).

Some clean-up here and there in dama (coercions removed, implicits added, etc.)

Almost every hand-inserted coercion removed since a bug in the coercion
machinery has been fixed.

Bug fixed: the disambiguation domain for a record with left parameters was
not obtained with a pre-visit. The result was that often Failures were detected
later than possible with consequent waste of time.

Critical bug finally found after a long chasing!!!
When looking for a coercion over a non meta closed term, often the case was
not detected and a Failure was raised instead of Uncertain.

Added more typing information to remove a coercion.

Integration f_algebras declassed.
We suppose to prove everything on integration_riesz_spaces.
However, the definition or weak order unit is complex because of the sup
on sequences.

Up to absolute value