matita.cs.unibo.it Git - helm.git/log

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

preliminary support for hbugs
added to the cicbrowser the CTRL-l binding for highlighting the URL (a-la-firefox)

Up to max (up to a bug).

We begin to play the real game: we have defined real numbers and
constructive connectives (only the disjunction for now) and we are
trying to define the max between two real numbers as the limit of a
particular cauchy sequence. Cool.

Integration_algebras.ma split into 6 different files.

Syntax changed (to be changed back) for left parameters of inductive types.

The OK button of the disambiguation errors interface now adds aliases to the
current script. However, the aliases are used only in passes 1 and 3 :-(

Bug fixed: inductive types were no longer removed from the environment during
a remove_single_obj.

New behaviour of the disambiguation error messages: errors generated without
using coercions are shown only when More is pressed.

TermAcicContent.Interpretation_not_found catched and handled correctly.

Up to integration f-algebras.

Debugging code is now controlled by the debug flag.

library = yes!

remove_obj is now much faster:
1. the code was utterly messy, trying to remove from the DB files and
to remove from disk #xpointer uris.
2. LIKE substituted by =
3. added QUICK and LOW_PRIORITY to the DELETE statement
4. removed unuseful and unused debugging code that used to slow down every
deletion

Level-1/LambdaDelta now compiles fine

Added target preall.opt.

GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
applications of applications (that are forbidden and not handled properly).

Better label for the disambiguation errors window.

New (and much more complex) disambiguation error interface.
Errors are now categorized according to:
  1. location
  2. error message
  3. environment

More timeout added to autos here and there.

1. is_meta_closed should be applied only to terms on which a substitution
   has already been applied. Fixed here and there.
   Note: it is not possible to add a subst parameter to is_meta_closed since
   the function is declared in cic/CicUtil and it is used where the unification
   is not available (e.g. in whelp and library)
2. known (but never verified before) bug fixed: delifting should fail
   (instead of raising Uncertain) iff the local context is not meta_closed.
   The test used to be "does not contain a Meta"

till some patches

the incomplete proofs were axiomatized

some patches. still does not compile properly

Added timeouts to auto here and there.

Added timeout to autos here and there.

1. bug fixed: Unicode characters that are not mapped to TeX macros used to
   be post-fixed with a blank
2. bug fixed: the textual pretty-printer does not implement the same
   spacing politics of GtkMathView. Since that politics is very very complex
   to implement, I try a different solution: we explicitly insert a space
   where we want one. The widget does not seem to be disturbed by this.
   This way the let ... rec and match ... with constructs are now printed
   correctly and they can be read back.
3. syntax change: applicative patterns no longer require parentheses around
   them

/home/fguidi/... => ../../...

we removed about 100 match-with costruction turning them into applications

Added a couple of flags to auto

Our unification used to guess a very complex argument of an apply in
fermat_little_theorem. It does no longer, but the old behaviour seems to be
really lucky. Thus I change the .ma file.

Two lemmas that used to pass no more now pass again. Bug simply because every
tactic argument now requires less question marks :-(

Added unit to rings.