* 'default "equality"' command changed to consider also
eq_rec, eq_rec_r, eq_rect, eq_rect_r
* rewrite tactic changed to rewrite also in goals of type Set and Type
* more progress in technicalities/setoids.ma
Important commit:
from now on the pretty printer CicMetaSubst.ppterm_in_context is substituted
with a reference to an high level pretty-printer (now defined in
matita/applyTransformation.ml). In the debug menu there is a switch to turn
it off and get back the old pretty-printer.
Ferruccio Guidi [Tue, 6 Feb 2007 19:36:05 +0000 (19:36 +0000)]
- Procedural: moved in a directory on its own
- ApplyTransofrmation: now handles inline macro expansion
- GrafiteParser MatitaEngine MatitacLib: added a callback in each
- tests/letrecand.ma: changed baseuri
Serious bug fixed: the types of a real mutual fix definition were not lifted
as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).
Enrico Tassi [Thu, 1 Feb 2007 14:48:05 +0000 (14:48 +0000)]
reverted a commented substitution in build_newgoal, added an euristic to
order the lambdas of a proof abstracted in a letin such that dependency betwwen the types of the lambdas is inferrable by the refiner
Ferruccio Guidi [Wed, 31 Jan 2007 19:54:01 +0000 (19:54 +0000)]
methods eos, goto, advance and retract now catch Invalid_argument "Array.make"
that is raised when the script is too big to be handled (this makes quit work!)
Several bugs fixed:
1. mutual definitions were not generated correctly
(e.g. let rec even ... and odd in even actually resulted in a
definition of odd!)
2. a top-level mutual definition now generates two constants (as it
should have always been)
Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now
processed from right to left to make the cases tactic open goals in the
expected order.
Some changes:
1. error messages are now in HTML (they used to be in plain text + vt100 colour
scheme)
2. commands are now expected to be in a fragment of the pgip protocol.
Supported commands are:
<pgip><doitem>...</doitem></pgip>
<pgip><undoitem>...</undoitem></pgip>
3. the terminator sent back is now preceded by either -1 (command not
successful) or n (an integer to be sent for undoing)
4. undoing is now supported
Just a few lines test to understand with Cezary Kalinsky how much effort is
required to integrate Matita in his generic AJAX based interface.
matitawiki is an executable that reads from stdin and prints output and error on
stdout/stderr (both followed by (Char.chr 249) after each command).
All the interactive commands (thus also "undo") are not supported.
1. buf fixed in eval_from_stream when first_statemente_only=true:
the last computed states were lost
2. added a new watcher function to eval_from_stream.
The function is called after the execution of each command.
Enrico Zoli [Wed, 17 Jan 2007 17:59:59 +0000 (17:59 +0000)]
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.
Ferruccio Guidi [Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)]
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.
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!
Enrico Tassi [Sat, 6 Jan 2007 16:16:40 +0000 (16:16 +0000)]
- 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
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.
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.
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.
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).
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.
Ferruccio Guidi [Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)]
- 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
projects / helm.git / log