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
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).
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.
Enrico Zoli [Fri, 15 Dec 2006 18:59:00 +0000 (18:59 +0000)]
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.
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).
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).
Ferruccio Guidi [Wed, 13 Dec 2006 19:50:03 +0000 (19:50 +0000)]
- transcript: patched to generate aliases instead of inlined variables
- CoRN-Decl: regenerated with aliases instead of inlined variables
- content2Procedural: improved but not working yet
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.
Ferruccio Guidi [Thu, 7 Dec 2006 15:43:42 +0000 (15:43 +0000)]
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.
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
Ferruccio Guidi [Tue, 5 Dec 2006 15:44:54 +0000 (15:44 +0000)]
- components: composed coercions mus be generated with current base uri
- transcript: fixed to handle coercions from constructors
- CoRN-Decl: regenerated. CoRN.ma now compiles!
projects / helm.git / log