more lemmas to prove and a correction in subst

more notation and one more lemma to prove :(

reductions rules and one lemma

more properties of relocation

Multi-user matita: changed the status object to include a ``user'' method
containing an optional string, used to identify associated user.

Fixes bugs in the  Matitaweb UI.

Fix for internet explorer (but still works badly).

Cosmetic changes.

Fixed a bug in the retract command of Matitaweb.

Logo for use in matitaweb.

Removed dependency of Matitaweb from GTK libraries.

- we removed the reduction-related item categorization
- some renaming

Removed hardcoded include paths from matitadaemon.

Some changes in the Makefile for matitaweb.

Fixes record projections (see matita 1.0 branch)

Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd

This can happen: when you use nodelta.

Minor changes because of the new, weaker (but much faster) delift.

Bug fixed: trailing ' in names were not removed when computing the next free
name.

We reintroduce the distinction between binding and non-binding items.
Mon-binding items are now forbidden in environments

Major speed-up:

 1) bug fixed: the fo_unif applied to a metavariable in the subst made a
    recursive call using unify. Thus, in case of failure of the unify
    (after hints, reduction, etc.), fo_unif failed and hints, reduction,
    etc. was tried again. This resulted in an exponential blow-up in the
    worst case.
 2) bug fixed: in the case  ? args == ?pattern, the ?pattern was delifted
    w.r.t. args, but during the delift the special unification case with
    a pattern was considered again. This was costly since reduction was
    used on the first argument of the unification.
 3) semantics of fo_unif "fixed": it is now succesfull on every pair of
    terms whose rigid prefix is equal and whose arguments are unifiable.
    Before it used to fail for example on (x args == x args) where x is
    a Rel.
 4) BEHAVIOUR OF DELIFT CHANGED: it no longer matches terms in the local
    context up to full unification, but only up to fo_unif. Some tactics
    that used to be accepted could now fail and the user needs to change
    the terms by hand before applying the tactic. On the other hand, the
    speed up is really significant.

This update uses XML for client-server communication. For unknown reasons, this
doesn't seem to work well with Firefox (but works ok on Chrome).

We reverted to a single process http daemon because of an annoying bug in
Ocaml Http, causing the daemon to terminate randomly.

- we introduce extended existentials (generated)
- we exploit the tactic "*" to reduce the volume of decompositions

Max width overflows, which cause auto to fail, are now logged as errors.
The message "auto gave up" is not very informative by itself!

Fixed a bug that prevented record projections from being generated. This patch
supersedes a previous one (r11250), which created more problems than those it
solved.

The pretty printer should never fail, even on fake inductive types used in
patterns.

Pretty printing of exceptions escaped from pretty printing of exceptions
improved.

Avoid killing the main gui thread.

Delift used to produce not well typed substitutions. In turn, this
led to tactics that were not failing immediately, but only at Qed.

Fixed by adding the appropriate check to the delift function.

Note:
 - pass the metavariable number (-1) to avoid the check when you know what
   you are doing (e.g. when delift is just used to restrict a term or to
   replace a term with a convertible one). This used to be 0 (not -1).
 - in some cases (algebraic universes and implicits used to stop chains of
   metavariables) the check is relaxed
 - to make the CerCo script pass (in very "reasonable" and "frequent" cases),
   the algorithm needs to solve the following unification problem:
     S (?[n]) == ?[(S n)]
   Our algorithm used to delift S(?[n]) w.r.t. (S n), yielding x |- ? := x.
   By chance, this was the right solution since S (?[n]) becomes (S n) and
   also ?[(S n)] becomes (S n). However, the two solutions were both added
   to the subst (first bug) and they could even be different (second bug).
   We fix this by checking that they are not different.
   However, at the moment, the solution still occurs twice in the subst....

CC2FO_K_cube: soundness of the K interpretation stated

Comment is now up-to-date.

Matita Web: moved the javascript in a separate file. Bugfixes.

subst.ma: some additions
convertibility.ma: non "conv" refers to the correct predicate
CC2FO_K.ma: CC to Fomega: first interpretation: substitution lemma

Print backtrace of exceptions when OCAMLRUNPARAM=b is setted.

assert false removed

Partial implementation of "go to cursor" action.

auto does not work here :(

basics: some additions
lambda: some additions + split of lift and subst

Better indentation.

Partially working table layout of matita web (only on some browsers).

Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.

Name generator for Russell greatly improved.
But maybe we need a longer term solution.

Improved rendering of sequents in matitaweb, including handling of multiple
goals.

Serious bug fixed:
 - in order to look for coercions to sort and funclass, we passed
   types containing implicits and a flag to avoid unification
 - totally avoiding unification, it happened
    1) that we diverged:
       t : A :> B ==> inject t : Sigma x.A :> B ==> eject (inject t): A :> B
    2) that we called unification on types that contained implicits
       (in some cases)

Prod indexed as Dead, that is equal only to itself, instead of Variable that
is equal to anything

Preliminary version of matitaweb handling multiple goals in the sequent view.

Syntax for coercion nocomposites fixed.

Added "nocomposites" to coercions.

- degree: some improvements and the Deg_append lemma
- lambda_notation: the K interpretation (CC to Fomega mapping)

Quick patch to avoid name collisions when passing coercions under let...ins.

Coercions are now propagated under let...ins.

Fixed box pretty printing.

matitaweb: added retract (undo)

degree.ma: we defined the "degree" of a term, which is meaningful in
the lambda-cube

1) interpretation of matches in patterns implemented
2) missing exception added to matitaExcPp

Added support for hyperlinks in the goal view of the web interface.

...

Removed dead code

- we weakened SAT3
- we simplified the specifications of the Cube

want_indent bug fixed

readded function box_of

Compilation fix

Compilation fix

Simplified rendering.

Simplified rendering

Simplified rendering

rm rendering attrs

Removed mathml and proof rendering.

Simplified rendering

Porting to new reduction.

Added matitadaemon.

cube.ma: some pts specifications of the lambda-cube

Porting to the new pts.

Porting to new parametric TJ.

Dummies are blocked.

New version of TJ parametric in the specification of pts.

we added a property

ground: some arithmetical properties added
lift: some properties proved

interim version (added smallLexer)

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).

Partial modifications.

we uncommented R3 and R4 tu be used in lambda-delta

- weight: bugfix + weight-based eliminator axiomatized
- notation: bugfix
- lift: first main property axiomatized

- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(

convertibility.

generatin lemmas and subject reduction (with a lot of axioms).

progress

error in the conversion rule

notation bug fix

- some bug fixes
- we defined the thinning relation

complete reformalization of lambda-delta in matita (initial commit)
first definitions and one lemma

disambiguation of explicit interprettions with arguments now works
i.e. 'eq x y z

...

we added an nmap from NCic.obj to NotationPt.obj (to be continued)

we removed an extra dot from the "include" syntax

we introduced nterm for NotationPt.term

Patch to avoid equations of the form ? -> T (oriented this way) that
can always be applied to later yield non well typed terms.

Moreover, when T is a Leaf and when the goal contains a Leaf, the equation
above is applied breaking one of the "assert (subst=[])" in the code
(since the Leaf is matched by ?).

we proved that the union of two saturated sets is saturated

Keeping track of locations of disambiguated ids and symbols.
Matitac produces disambiguated files, with hyperlinks for ids and § marks
for symbols.
Matita is able to reparse ids with hypelinks.