completed lemma 17

...

re 16.4 almost done

big mess of notation

more notation

moved formal_topology into library"

some notation for map_arrows2

...

Some important proofs/definitions were (and are still) commented out and
do not compile.

Added the notion of functor1 to state the main theorem.

Proof simplified.

Proof simplified (??).

...

...

...

...

....

...

notation made half decent

better notation for oalgebra

....

off by one fixed

Fix for inversion principles of types with a single constructor.

Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

some stuff on re

unify left args of inductive types with left argus of constructors. this allows
to put ? in every left arg of every constructor of an inductive type.

Library support files for John Major equality and Russell.

Experimental support for Russell (coercions moving inside lambda & pattern
matching etc.) added to the refiner.

minimization.ma

little workaround for multiple screens, gdk support not bound by lablgtk2

new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

trace generation with "// by _;"

notation

remarks and applyS

Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

...

Fixing naming scheme for composite coercions.

assert false could happen

Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

coinduction is between us

First tests.

* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

Regular expressions.

new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

same heads different arity -> INCOMPARABLE

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

some fixes to THF parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed support file for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

the edges must be quoted as well (not only the nodes)

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

apply_subst_context on statuses

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

thf problems list for tptp 4.0.1

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

fixed compiltion order of lexer/parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

New code (unbranched) to compute all keys by all possible ways of reducing the term.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

THF parser received some care

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

THF parser for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

Not is now inductive.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Use the inversion!

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Bug fixed: the current equation is not always the last hyp.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

More debugging info from print_tac.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Implicit and UserInput were printed incorrectly.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

ninversion

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

Added test file for inversion in ng matita.

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

Tracing mechanism for auto. Interface changed to solve an ambiguity between
an ampty trace and a missing trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

Good definition found.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

(Co)Inductively Generated Formal Topologies (not only basic ones)

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

patched the definition of locate, advances in locate_add; still issues..

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

Z.ma updated to reflect changes in the logical Not operator

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

Automation problem

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

More work

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

cosi va (se vi pare).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Conflict(?).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

Extension of demod to arbtrary predicates (not just equalities).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

Nice examples for automation (that fails).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Simplified proof after pattern fix

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

"Not" is no longer a definition

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

The precedence of ^-1 has changed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

Real numbers as co-inductive streams of digits (overlapping refining intervals).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>