; $Id: log.txt,v 1.86 2010-01-14 23:05:22 logik Exp $

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done locally 2009-12-10

In doc/manual.tex

The role of optional arguments in normalize-goal described.
Description of "use", "use-with", "cut", "split", "ind", "simind",
"elim", "cases", "casedist" updated.  Description of "assert",
"msplit", "gind", "intro-with", "inversion", "by-assume-minimal-with"
added.  "make-gind-aconst", "make-min-pr-aconst",
"make-exc-intro-aconst", "exc-formula-to-exc-intro-aconst" described.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2010-01-14

In grammar.scm

Line (lpar grecguard-op number typelist rpar) : ($2 (cons $3 $4)) added.

In pconst.scm

grecguard-const-for-gind? corrected.  It gave wrong results in case
the value type tau had one argument type.

In axiom.scm

In avar-full=? the test formula=? replaced by classical-formula=?.
Reason: classical-formula=? also tests for equal normal forms.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2009-12-10

In lib/nat.scm

"NatLeLtCases" added:
"all nat1,nat2((nat1<=nat2 -> Pvar) -> (nat2<nat1 -> Pvar) -> Pvar)"

In pp.scm

token-tree-tag-left-assoc? and token-tree-tag-right-assoc? changed:
tensor-op should be right associative

In psym.scm

predconst? corrected (order tsubst - index was wrong)

In axiom.scm

In avar-to-string (+ 1 index) replaced by index.  This allows avars u0
in displays.

In proof.scm

rename-bound-avars replaces all bound avars by new ones with the
same name but a new index.  Properties: (i) rename-bound-avars
transforms a proof satisfying the avar convention w.r.t. its free
avars into a proof satisfying the avar convention completely.  (ii)
In every subproof of the result no free avar occurs (w.r.t. avar=?)
bound as well.  Property (ii) is assumed in proof-substitute-aux.

check-and-display-proof extended by checking the avar convention:
two avars with the same name and index are equal.  This done via
avar-convention-violations .

In proof-substitute-aux we must assume that in every subproof no
free avar occurs bound as well.  This is ensured by a preprocessing
step, using rename-bound-avars.  Example for the need:

(add-var-name "x" (py "alpha"))
(add-pvar-name "Q" (make-arity (py "alpha")))
(define avar (make-avar (pf "Q x") -1 "u"))

(define proof
  (mk-proof-in-elim-form
   (mk-proof-in-intro-form
    (pv "x") avar (make-proof-in-avar-form avar))
   (pt "x") (make-proof-in-avar-form avar)))

(proof-to-expr proof)
; (((lambda (x) (lambda (u) u)) x) u)

(define avar1 (make-avar (pf "Q x") 1 "u"))
(define proof1 (proof-subst proof avar (make-proof-in-avar-form avar1)))

(cdp proof1)
; ....Q x77 by assumption u66
; ...Q x77 -> Q x77 by imp intro u66
; ..all x77(Q x77 -> Q x77) by all intro
; ..x
; .Q x -> Q x by all elim
; .Q x77 by assumption u66

; equal formulas expected
; Q x
; Q x77

In src/list.scm

(duplicates-wrt equality? l) returns a list of two-element sublists
(x x') of equal elements of l whose transitive closure consists of all
such two-element sublists.

In ets.scm

proof-to-extracted-term-aux corrected: atr-x-formula removed

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2009-11-13

In psym.scm

In add-ids clause-test changed: non-computational idpcs are allowed.
Then (except in special cases) the elimination scheme must be
(severely) restricted to n.c. formulas.  Moreover, all clauses must
have non-computational invariant (n.c.i.) parameter and premise
formulas.  This ensures that the soundness theorem continues to hold:
every intro and elim axiom is invariant, i.e., nullterm mr A is the
same as A.

In formula.scm

var-and-vars-to-new-var corrected: in the loop generating new-index
(is relevant-indices (cdr is)) replaced by 
(is relevant-indices (remove i is)).

In proof.scm

proof-substitute-aux corrected in aconst case.  aconst-substitute-aux
corrected: uninst-formula0 is kept.

(decorate proof) corrected: it is first checked whether the proven
formula is c.i.  If so, the given proof is returned.  Otherwise
undec-proof-and-decavars-and-decfla-to-decproof is called.
undec-proof-and-decavars-and-decfla-to-decproof-and-ext-decavars
corrected: test (formula-of-nulltype? (proof-to-formula proof))
removed.

In examples/test.scm

Nullary clauses named Init... rather than Gen... (for instance
"InitEqD" instead of "GenEdQ").  Dialectica extraction for proofs of
formulas with allnc removed, since this is not yet properly covered by
the implementation.

In boole.scm

Discarded code removed.

In pconst.scm

Typos in comments corrected.

In axiom.scm

clause? replaced by cr-idpc-clause? and nc-idpc-clause?
(strictly-positive? formula pvars) changed: the parameter pvars need
not occur.

In etsd.scm

Typos corrected: term-subst -> term-subst-et, term-substitute ->
term-substitute-et.

In term.scm

In normalize-term-pi-with-rec-to-if-aux error corrected: abstract only
as many vars as the corresponding constructor has arguments.  Typo
corrected in term-in-elim-form-to-final-op-and-args .  In
formula-of-nulltypen? typo corrected: pvar-with-positive-content?
replaced by pvar-with-negative-content?

In pproof.scm

simphyp-with simphyp-with-to and simphyp added (were lost).  Dot
notation removed.

In ets.scm

real-and-formula-to-mr-formula-aux corrected in impnc case and
extended in the predicate case.  However, the mr-formulas are still
not written with allnc, impnc as they officially should (but it does
not matter).  mr-invariant?  removed. In proof-to-soundness-proof-aux
mr-invariant? replaced by non-computational-invariant?  In an error
message of animate unnecessary type-to-string removed.

In examples/arith/sqrttwo.scm

Minor cleanup.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done locally 2009-06-30, in the trunk 2009-09-18

In lib/list.scm

Error concerning variable names removed.

In pconst.scm

In add-program-constant message suppressed for cIf.

In term.scm

In normalize-term-pi-with-rec-to-if recursive call added in case of an
unchanged recursion operator with sufficiently many arguments (was
forgotten).

In match match2 match2-for-tsubst optional argument ignore-deco-flag
introduced.  In match-aux match2-aux match2-for-tsubst-aux
additional argument ignore-deco-flag introduced.  In match2-aux typo
corrected: sig-tvars sig-vars replaced by sig-vars sig-pvars

formula-of-nulltypep? formula-of-nulltypen? adapted to possibly
decorated formulas with inductively defined connectives.

DIALECTICA-FLAG is set to #f

In psym.scm

idpredconst-to-string drops the trailing t in exdt, exlt, exrt,
exut.  The information about totality is in the following variable.

add-ids changed: inductively defined predicate constants without
content must be defined by only one (non-recursive) uniform clause.
Examples: EqD, ExU, AndU.  Soundness of the intro and elim axioms
holds if the parameter-cterms in ExU, AndU are invariant.  Then AC, IP
and IQ are not needed.  Construction of et-constr-types simplified,
using the assumption that the clauses are either all with or all
without content.  DummynbeIDPC removed as a constructor in nbeIDPC: it
is not needed because nullary clauses are required.  Assignment of
tokens for idpc-names made more general.  Double definition of
string-and-arity-and-cterms-to-idpc-parse-function removed.

In formula.scm

imp-impnc-all-allnc-form-to-vars-and-premises formula-to-bound added.

exdt, exlt, exrt, exut replaced by exd, exl, exr, exu in displayed
formulas.  The information about totality is in the following
variable.  formula-to-undec-formula extended to exu, exut, andu, oru
and generally to predicate forms with inductively defined predicate
constants.  cterm-to-undec-cterm , idpredconst-to-undec-idpredconst
added.

dec-variants-to-lub and the binary dec-variants-to-lub-aux extended
to the new decorated connectives (ord orl orr oru andd andl andr
andu exd exl exr exu exdt exlt exrt exut) and generally to predicate
forms with inductively defined predicate.  extending-dec-variants?
added.  strengthened-dec-variants? added.

dec-variants? with its auxiliary function dec-variants-aux? and
dec-variants-up-to-pvars? with dec-variants-up-to-pvars-aux? added.
full-dec-variants? removed.

In formula-to-token-tree typo corrected (exu-form?  changed into
exut-form?).

formula=? classical-formula=? cterm=? all now have an optional
argument ignore-deco-flag  (formula=? formula1 formula2 #f) means
(formula=? formula1 formula2) but (formula=? formula1 formula2 #t)
means that decorations are ignored.  formula=-aux? has an extra
argument ignore-deco-flag.

pp-subst added, as an alternative to display-substitutions

Connective andl removed.  Reason: AndL is not accepted, since it is
required (without loss of generality) that impnc-param-prems come
before imp-param-prems.  Use B andr A instead of A andl B.

In boole.scm

Tokens exdt exlt exrt exut removed.  The information about
totality is in the following variable.

In axiom.scm

aconst-to-computed-repro-formulas corrected.  Exnc-Intro and
Exnc-Elim were missing.  Typo corrected: cetrms -> cterms.
avar-full=? now has an optinal argument ignore-deco-flag
intro-aconst-to-computed-repro-data corrected: there must be as many
cterms in idpc as there are param-pvars, but tpinst (in aconst)
might be shortened.  elim-aconst-to-computed-repro-formulas
corrected.  uniform-non-recursive-clause? added.  In check-aconst
typo in error message corrected.  In add-theorem message suppressed
for If.

In proof.scm

proof-in-imp-impnc-all-allnc-intro-form?
proof-in-imp-impnc-all-allnc-intro-form-to-var
proof-in-imp-impnc-all-allnc-intro-form-to-kernel added.

proof-in-intro-from-to-vars computes all (or at most (car x))
abstracted avars and vars of a proof.

proof-in-intro-form-to-final-kernel computes the final kernel (the
kernel after removing at most (car x) abstracted avars and vars) of
a proof.

intro-proof-and-new-kernel-and-depth-to-proof added.

proof-in-exnc-elim-rule-form? added.

We use acproof to mean proof-with-avar-contexts.  An acproof is a
proof in the sense of check-and-display-proof.  It is used to avoid
recomputation of avar-contexts.

make-acproof-in-avar-form make-acproof-in-aconst-form
make-acproof-in-imp-intro-form make-acproof-in-imp-elim-form
make-acproof-in-impnc-intro-form make-acproof-in-impnc-elim-form
make-acproof-in-and-intro-form make-acproof-in-and-elim-left-form
make-acproof-in-and-elim-right-form make-acproof-in-all-intro-form
make-acproof-in-all-elim-form make-acproof-in-allnc-intro-form
make-acproof-in-allnc-elim-form proof-to-acproof added.

nbe-normalize-proof-without-eta and its auxiliaries extended, to
allow for nbe-normalize-proof-without-eta-for-extraction.

proof-to-eta-nf and proof-to-eta-nf-for-extraction both derived from
a general (proof-to-eta-nf-aux proof extraction-flag content-flag).
This is for efficiency reasons: one need not enter parts of the
proof which do not contribute to the extracted term.

proof-to-proof-with-eta-expanded-permutative-aconsts added, modelled
after if-term-to-eta-expansion-and-unfolded-simrecs in term.scm.  It
extends, simplifies and corrects (in impnc-case)
proof-to-proof-with-eta-exp-ex-elims and its auxiliary functions
ex-elim-aconst-to-eta-expanded-proof and
ex-elim-aconst-to-eta-expanded-proof-from-exhyp.  For efficiency
again there is a variant
proof-to-proof-with-eta-expanded-permutative-aconsts-for-extraction

A permutative redex occurs if the conclusion of a permutative
assumption constant (example: Ex-Elim), applied to parameters and
all side premises, is the main premise of an elimination.  We assume
that this conclusion is a prime or existential formula, since this
will be the case when normalize-proof-pi is used in normalize-proof.
Hence the final elimination must be an elimination axiom for an
inductively defined predicate or else Ex-Elim.

permutative-aconst? permutative-redex?  added.

For permutative conversion we use an auxiliary function
(normalize-proof-pi-aux proof extraction-flag content-flag).  The
extraction-flag indicates whether we are interested in extraction
only.  If so, we can disregard (maximal) parts of the proof without
computational content.  The content-flag indicates whether the
formula of the proof has computational content.  This is for
efficiency only, since it avoids recomputation.  When
extraction-flag is #f content-flag is irrelevant.

normalize-proof-pi normalize-proof-pi-for-extraction
(normalize-proof-pi-aux proof extraction-flag content-flag) added.

Added proof-in-permutative-normal-form? and
proof-to-permutative-redexes as test functions to check
normalize-proof-pi .

proof-in-beta-normal-form? rewritten, making use of new functions
proof-in-beta-normal-form-for-extraction?
(proof-in-beta-normal-form-aux? proof extraction-flag content-flag).

Normalization of proofs is made more efficient by allowing to know
whether one is interested in extraction, and if so, disregard parts
of the proof without computational content.  The extraction-flag
indicates whether we are interested in extraction only.  If so, we
can disregard (maximal) parts of the proof without computational
content.  The content-flag indicates whether the formula of the
proof has computational content.  This is for efficiency only, since
it avoids recomputation.  When extraction-flag is #f content-flag is
irrelevant.

This is done by adding -for-extraction and general -aux variants
(taking as additional input an extraction-flag and a content-flag)
of proof-to-eta-nf
proof-to-proof-with-eta-expanded-permutative-aconsts
nbe-normalize-proof-without-eta normalize-proof-pi
proof-in-beta-normal-form .

Added nbe-normalize-proof-for-extraction and the general
(nbe-normalize-proof-aux proof extraction-flag content-flag).

normalize-proof-simp added.  Simplification conversions (Prawitz)
make use of the concept of a permutative aconst.  It is checked
whether one side-proof-kernel has no free occurrence of any avar
bound in this side-proof.  proof-to-proof-without-predecided-avars
added.  It removes dependencies on avars, and in this way helps to
make normalize-proof-simp useful.

Then remove-predecided-if-theorems (special for pruning).  Because
of its usage of term-to-minuend-and-subtrahends and
le-minuend-minus-subtrahends-avar-and-subtrahends-to-proof it is
designed for use in the binpack case study, where the boolean terms
are of the form i<=j--i0--...--in.  It would be better if a more
general decision procedure is used (simplex-algorithm?).

prune added, as a generalization of Prawitz' simplification.  A
problem with prune is that is is slow.  For efficiency the proof is
first turned into an acproof, to avoid recomputation of
avar-contexts when pruning.

undec-proof-and-decavars-and-decfla-to-decproof-and-ext-decavars
corrected in case allnc-intro: if the allnc bound variable decvar in
the decorated fromula is distinct from the variable var used in the
proof it needs to be renamed into var.  In case of an aconst that
can be changed downward we do it, particularly at intro and elim
aconsts for or, ex, and, but also for arbitrary theorems or global
assumptions one of whose less decorated variants suffices.  Example:
L: all n((C n -> F) orr C n) is an extension of another lemma LU:
all n((C n -> F) oru C n).  We assume that in IDS variants appear
in decreasing order (i.e., the more extended ones are introduced
first), that all possible variants do appear and that their clauses
use the same parameter predicate variables.  Search for proofs of
less extended formulas from alternative assumption constants
included.  Proofs of c.i. formulas are not entered by the decoration
algorithm.  Auxiliaries:
op-and-args-and-altop-and-decfla-and-decavars-to-proof assumes that
op applied to args proves an extension of decfla, and that altop
differs from op only in possibly requiring additional premises.  It
is tested whether altop applied to args and some of decavars is
between op applied to args and decfla w.r.t. extension.  If so, a
proof based on altop is returned, else #f.
decfla-and-opname-to-altops returns a list of alternative operators
(assumption constants) possibly usable to prove decfla.

proof-to-expr-with-formulas-aux now uses rename-variables.  This
gives alpha-equal variants of the formula with small indices.

In check-and-display-proof optional argument ignore-deco-flag
provided.  Moreover it was wrongly assumed (in an error message)
that the list produced by nc-violations consists of object variables
only.  check-and-display-proof-aux corrected in case of an Elim
aconst.

In pproof.scm

Adapted to EqD: simp-with-intern simp-with-kernel-aux
simphyp-with-intern compat-at eq-compat-at eq-compat-rev-at
compat-rev-at simphyp-with-intern simphyp-with-kernel-aux.

In fla-and-sig-topvars-and-goal-fla-to-use2-data the call of match2
now has #f (for ignore-deco-flag) as an additional argument.  In
intro-intern usage of aconst-to-inst-formula and free removed.

In ets.scm

proof-to-extracted-term-aux corrected in case of an Elim aconst.  The
result must be an identity for a uniform one-clause defined idpc.

mr-invariant? corrected in impnc case: then both the conclusion and
the premise need to be invariant.

In imp-formulas-to-et-rec-const simplified-relevant-clauses adapted
to impnc (was forgotten).

We initially supply the Cases Lemma If: all boole((boole -> Pvar) ->
((boole -> F) -> Pvar) -> Pvar).  This can be done only here,
because for add-theorem we need formula-to-et-type.

If: all boole((boole -> Pvar) -> ((boole -> F) -> Pvar) -> Pvar) can
be used for case distinctions.  After animation of cIf we have added
the computation rule (cIf alpha4) ->
[boole0,alpha4_1,alpha4_2][if boole0 alpha4_1 alpha4_2]

Inductive definitions of Leibniz equality EqD and of the logical
connectives ExD, ExL, ExR, ExU, ExDT, ExLT, ExRT, ExUT, AndD, AndR,
AndU, OrD, OrL, OrR, OrU added.

We need to define eqd-compat-proof in order to put EqDCompat into
THEOREMS when loading init.  This can be done only in ets.scm, because
for add-theorem we need formula-to-et-type.

In pp.scm

DOT-NOTATION set to #f initially.  token-tree-to-string and
token-tree-to-pp-tree display exdt, exlt, exrt, exut by exd, exl, exr,
exu.  The information about totality is in the following variable.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2009-06-29

In lib/list.scm

A variant ListAppd of ListAppend (with display ++) provided, which
allows rewrite rules with two arguments.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done locally  2009-06-25, in the trunk 2009-09-18

In lib/numbers.scm

allnc and --> used in the (single) add-ids clauses for RealEq
RealNNeg and RealLe.  RatPlus, RatMinus, RatTimes, RatDiv, RatLt,
RatLe exhanced by adding external code.

In examples/analysis/real.scm

allnc and --> used in the (single) add-ids clauses for Cauchy,
Mon and Real.

In examples/analysis/cont.scm

allnc and --> used in the (single) add-ids clauses for Cont and
Corr.

In pproof.scm

Typo corrected: formula-toinst -> formula-subst


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2009-03-19

In proof.scm

In spreading-formula-to-proof-aux typo corrected (parentheses).

In etsd.scm

In proof-to-extracted-d-terms-aux typo corrected: uninst-step-formula
-> uninst-step-fla

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2009-01-23

In etsd.scm

In proof-to-extracted-d-terms-aux , case imp-elim and there
proof-in-ind-rule-form? or proof-in-cases-rule-form? ,
take the correct number of arguments of the step formula
(observed by Trifon Trifonov)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-11-21

In axiom.scm

Exnc-Intro and Exnc-Elim were missing in aconst-to-computed-repro-formulas

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-11-11

In proof.scm

In rm-exc "-" deleted in exc-elim-aconst and exc-intro-aconst names.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-11-06

In proof.scm

In check-and-display-proof-aux in cases all-intro and allnc-intro
the variable condition needs only to consider the variables free in
normalized assumption formulas.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-11-03

In pproof.scm

The optional first argument m of search (i.e., how often assumptions
are to be used) is passed to intro-search, which had used mult-default
before.  Since elim-search calls intro-search, it needs m as an
argument as well.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-10-28

In term.scm

term-to-term-with-let enhanced.
term-to-expr made usable for list recursion.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-09-28

In axiom.scm

General comments on Total, STotal, SE, E and induction.
(1) For induction only STotal is relevant.  It corresponds to the
semantic concept of totality.  (2) Total is useful when working with
pairs: the components of a total pair are total.  (3) Induction for
"all a P a" proves "all a^(Total a^ -> P a^)" which is weaker than
"all a^(STotal a^ -> P a^)", but helpful because total variables
occur.  (4) SE and E are convenient when doing proofs, because of
their rules.  But they are not fundamental, and should not be used
for induction axioms.  They can be brought in later, using

finalg     | sfinalg    | alg      | rho=>sigma
-----------------------------------------------
E      | ^ |            |          |  
SE     | | | SE     | ^ |          |
STotal |   | STotal v | | STotal ^ | STotal
Total  v   | Total      | Total  | | Total

Consequences.  (1) aconst-to-computed-repro-formulas now is able to
produce correct results for "Ind" and "Cases" with partial
variables.  (2) It becomes much clearer what induction axioms are.
(3) all-formulas-to-uninst-imp-formulas-and-tpinst and ind-intern
are simplified.

all-formulas-to-uninst-imp-formulas-and-tpinst
typed-constr-name-to-step-formula
all-formulas-to-uninst-cases-imp-formulas-and-tpinst
typed-constr-name-to-cases-step-formula and
aconst-to-computed-repro-formulas adapted and simplified.

alg-to-total-to-stotal-aconst and check-aconst corrected.

In pproof.scm

ind-intern simplified and text for (ind) adapted.
simind-intern simplified and text for (simind) adapted.
stotal-imp-formula? added.
cases-intern simplified and text for (cases) adapted.
casedist-intern simplified and text for (casedist test) adapted.
dec-cases-proof and dec-stotal-cases-proof rewritten.

In examples/test.scm

Adapted to the new formulation of induction and cases for partial
variables with STotal.

In lib/list.scm

Minor adaptions: premise name [SE] renamed into [STotal].
Next-to-last command in proof of "LhConsn" removed.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-09-25

In lib/nat.scm

AllBNatIntro and AllBNatElim reformulated with a total function
variable.

In lib/list.scm lib/listrev.scm

AllBListIntro and AllBListElim reformulated with a total function
variable.

In pproof.scm

In eq-compat-at "Eq-Compat" is of kind 'axiom, not 'theorem.  In
eq-compat-rev-at the uninst-formula of the "Eq-Compat-Rev" aconst was
formed with a new tvar.  Now it is left unchanged.

In x-and-x-list-to-proof-and-new-num-goals-and-maxgoal in case of an
atomic formula for x, when using the predefined atom-to-imp-proof
and-atom-to-left-proof and-atom-to-right-proof it was not checked
that the boolean arguments are total.

In INITIAL-THEOREMS proof for "InhabTotal" added.

In proof.scm

In proof-substitute-aux make-substitution replaced by
make-substitution-wrt var-term-equal?  In aconst-substitute-aux the
case of an elim-aconst which is allowed to have free variables in its
uninst-formula is taken care of.

In axiom.scm

There was a contradiction of the general description of aconsts -
saying that uninst-formula has no free object variables - and the
way elim-aconsts are formed, where the argument variables xs^ of the
inductively defined predicate are formally free in uninst-formula;
however, they are considered bound as well.

In pconst.scm

In const? token-type constscheme added.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-09-09

In etsd.scm

all-formulas-to-etd-rec-const removed.  Its (only) usage in the
proof-in-imp-elim-form case of proof-to-extracted-d-terms-aux is
replaced by arrow-types-to-rec-consts defined in pconst.scm.
(Work of Trifon Trifonov).

In examples/test.scm

Extended by applying extraction-test-etd to a simple proof by
induction using a weak existential.  (Work of Trifon Trifonov).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-09-01

In atr.scm

atr-min-excl-proof-to-intuit-ex-proof renamed into the more correct
atr-min-excl-proof-to-ex-proof.  Tests and error messages built in.
Error messages in min-excl-proof? improved.  atr-expand-theorems
added.  It expands all non-definite theorems.  This only makes sense
before substituting for bot.

In proof.scm

In undec-proof-and-decavars-and-decfla-to-decproof-and-ext-decavars
typo corrected, in case proof-in-and-intro-form.  Bound for the forced
exit in case proof-in-impnc-elim-form increased to 3.
proof-substitute-aux and aconst-substitute-aux (again) corrected and
simplified in aconst case.  The cases proof-in-aconst-form and
proof-in-allnc-elim-form are treated together.  For proof-substitute
it is required that an aconst is applied to at least as many terms as
there are free variables in its instantiated formula.

In lib/nat.scm

Nat=Comm renamed in Nat=Symm

In examples/test.scm

Tests for search added: all y(all z R y z -> P) -> all y1,y2 R y1 y2 -> P
and drinker all y(((Q y -> F) -> F) -> Q y) -> exca x(Q x -> all y Q y).
Examples for proof-substitute added.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-08-19

In proof.scm

proof-substitute-aux corrected in aconst case: clash of variables
was supposed to be avoided by brutal renaming in all aconsts:
(renamed-free (map rename (formula-to-free inst-formula))). However,
rename does something only for variables whose type is changed by
tsubst.  It is now done where needed only, using var-to-new-var.

In etsd.scm

rm-falsity-log adapted: after the change of proof-substitute-aux one
needs to compare the normal forms of proof-with-F-for-bot (obtained
by proof-subst) and proof.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-08-11

In term.scm

In term-to-eta-nf-with-simplified-simrec-appterms missing recursive
call added.

In axiom.scm

In aconst-to-computed-repro-formulas clause for GInd added.  In
all-formula-to-uninst-gind-formula-and-tpinst all p(p -> Rx) instead
of allnc p(p -> Rx) introduced.  all-formula-to-gind-aconst adapted to
changed formula of gind.  (Work of Trifon Trifonov)

In pproof.scm

In a comment, formula of gind changed.

In ets.scm

proof-to-extracted-term-aux adapted to changed formula of gind.
gind-aconst-to-et-grec-const changed into
gind-aconst-to-et-grecguard-const.

In etsd.scm

proof-to-extracted-d-terms-aux and proof-in-gind-rule-form?  adapted
to changed formula of gind.

In examples/test.scm

Adapted to changed formula of gind.  test.out moved to test.save

In examples/classical/ wftest.out moved to wftest.save


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-08-11

In todo.scm

Comment on provable exioms added, which are only there for
convenience.  Plan to replace the predicate constant Equal by the
inductively defined EqD, define atom p by p eqd True and falsity by
False eqd True (as in examples/test.scm).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-06-13

In term.scm

Some corrections in term-to-expr expr-to-free natrec and posrec.  In
term-to-expr quotient-safe and modulo-safe are used to avoid division
by 0.  (Trifon Trifonov)

term-to-term-without-predecided-ifs added.  It simplifies all if-terms
whose branch is known because we are in a branch of an outer if-term
with the same test term.  tests is an alist assigning to a term of an
algebra type the number of a constructor it is assumed to be built
with.

In formula.scm

In nbe-formula-to-type added support for exnc-form?

In ets.scm

proof-to-extracted-term returns 'eps in case of null type, instead of
raising an error, for consistency with etsd.scm.  (Trifon Trifonov)

In etsd.scm

proof-to-extracted-d-terms-aux-check-result extended by free variables
checking.  Added direct realizer for Efq.  GInd realizer corrected and
simplified.  Now the conclusion formula of the gind-rule is not A, but
allnc b(b -> A) instead.  This approach simplifies the implementation
and also allows extraction from forms of the GInd rule that are not
eta expanded.  (Trifon Trifonov)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-06-06

In typ.scm

type-match-modulo-coercion added

In pconst.scm

arrow-types-to-uninst-paramless-recop-types-and-tsubst corrected in
case of simplified simultaneous recursion.  Comments clarified.

In add-computation-rule and add-rewrite-rule
term-to-term-with-eta-expanded-if-terms replaced by
term-to-term-with-eta-expanded-if-terms-and-unfolded-simrecs

In term.scm

term-in-const-form-to-string corrected in case of simplified
simultaneous recursion.

nbe-normalize-term-without-eta extended to cover simplified
simultaneous recursion.  It first unfolds it to enable nbe, and
folds it again after normalization.
term-to-term-with-eta-expanded-if-terms-and-unfolded-simrecs
includes unfolding of simultaneous recursion operators into
term-to-term-with-eta-expanded-if-terms-and-unfolded-simrecs to
enable nbe-normalize-term-without-eta to work on these.  Conversely,
besides term-to-eta-nf we also need
term-to-eta-nf-with-simplified-simrec-appterms to make the
normalized term as simple as possible.

In psym.scm

string-and-arity-and-cterms-to-idpc-parse-function corrected, using
type-match-modulo-coercion .

remove-idpc-name changed: in case of a simultaneous inductive
definition there now is a comment that each of them is removed.

In formula.scm

ex-exnc-form-to-var ex-exnc-form-to-kernel ex-exnc-form? introduced.

Decoration of formulas: formula-to-undec-formula
formula-to-dec-formula full-dec-variants? defined.

aconst-and-dec-inst-formula-to-extended-tpinst is needed to
correctly decorate an aconst, by extending a given decoration.

aconst-to-undec-aconst changes tpinst, but leaves the uninst-formula
intact.  Then the repro-formulas need to be changed as well.

In axiom.scm

imp-formulas-to-uninst-elim-formulas-etc adapted to simultaneous
inductive definitions, which may be simplified in that only some
"relevant" idpcs are used in imp-formulas.  Moreover, a test is
provided to check that the xs^ in I xs^ are distinct.  Auxiliary
function: clause-to-simplified-clause and replace-final-conclusion.
From an aconst one can compute its repro formulas, using
elim-aconst-to-computed-repro-formulas
intro-aconst-to-computed-repro-data and generally
aconst-to-computed-repro-formulas.  In check-aconst the
repro-formulas present are compared with the computed ones.

To make comparison of assumption variables fast there is an avar
convention: two avars with the same name and index are equal.  The
test avar=? is based on this convention.  To allow checking for
violations of this avar convention avar-full=? is added.

In proof.scm

Automated insertion of uniformities added.  Aim: In a proof without
uniformities, insert as many of them as possible.
proof-to-undec-proof replaces in every formula -> by --> and all by
allnc.  aconsts are replaced by their undecorated form, which leaves
the uninst-formula intact.  However, the formula of the resulting
proof-in-aconst-form is manually changed to be totally undecorated.
The rules for ->, all are replaced by the ones for -->, allnc.

Notice that we work here with proofs violating the avar convention:
if two avars have the same name and index, then they are the same.
Therefore we need avar-full=? instead of avar=?, context-full=?
instead of context=? and context-item-full=? instead of
context-item=?  Also added context-fullminus and  pp-context.
proof-to-free-and-bound-avars-wrt added, which compares avars wrt a
given avar equality.  proof-to-context-wrt added.

Notice that cdp produces an error for the undec-proofs, because a
proof in aconst form has been given a formula which differs from the
one generated by aconst-to-formula.

undec-proof-and-decavars-and-decfla-to-decproof implements: For
every undecorated proof M and every decoration of its sequent we can
find a decoration KInfty of M whose sequent extends the given
decoration of Seq(M), and such that any other decoration K of M
whose sequent extends the given decoration of Seq(M) has the
property that K also extends KInfty.

In proof-in-elim-form-to-final-op-and-args typo corrected: arg
replaced by (list arg).  proof-respects-avar-convention? added.

In make-proof-in-impnc-intro-form typo corrected.

In pproof.scm

Extension and correction of elim-intern: it now incorporates the
former simelim, and works for simultaneously inductively defined
predicates as well.

simplified-inversion for simultaneously inductively defined
predicates does not add imp-formulas J xs -> J xs to form the
elim-aconst.  Then the (new)
imp-formulas-to-uninst-elim-formulas-etc generates simplified
clauses.

In examples/test.scm

Tests for pconst.scm: Tests for constructor-type-to-step-type and
arrow-types-to-uninst-paramless-recop-types-and-tsubst added.

Tests for term.scm: Tests for unfold-simplified-simrec-appterm and
simplify-simrec-appterm

Tests for pproof.scm: Test for elim with a simultaneous inductive
definition.

Tests for simplified-inversion.  Proofs of properties of WN and WNs
adapted to simplified-inversion.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-04-25

In term.scm

Correction of term=-aux?  Tn the abstraction case test added whether
the types of the abstracted variables are equal (before adding them to
the list of variables considered for alpha equivalence).  (Work of
Trifon Trifonov)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-04-23

In proof.scm

(set-goal (pf "all n(n<0 -> n<0)"))
(assume "n")
(ng)
(use "Efq")
fails to normalise: (np (current-proof)) gives an error.  Reason: Efq
is recorded with the normalised formula without free variables.  The
problem is in a "hack" in proof.scm, line 1561.  The line
(proof-to-formula proof) takes the formula from the proof in its
non-normalised form.  It is changed to (aconst-to-formula aconst) to
take the normalised formula from the aconst Efq itself, because this
is what nbe really needs.  (Work of Trifon Trifonov)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-04-18

In psym.scm

In string-and-arity-and-cterms-to-idpc-parse-function (re)introduced
programming error repaired again: the tsubst defined there may be #f
when subst-types is evaluated, but is used with assoc there.  (Work of
Florian Ranzi)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-04-18

In proof.scm

aconst-substitute-aux corrected to yield aconsts with properly
reduced type and predicate substitutions


In psym.scm

In string-and-arity-and-cterms-to-idpc-parse-function coercions
(re)introduced.


In term.scm

In match2-aux creation of a substitution item cds -> [n]cds n
excluded (needed to avoid possible looping)


In formula.scm

Forgoten exnc case added in make-quant quant-form? quant-form-to-quant
quant-form-to-vars quant-form-to-kernel


In examples/quant.scm

Canonical inhabitants introduced

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-04-01

In proof.scm

Correction of arename, done by Trifon Trifonov.  Reason: Consider the
proof lambda n lambda u:n<0 u.  The premise is chosen in a way so that
normalisation causes disappearing of the globally quantified variable.
If we call (ng) between assume and use of the same avar, it is
recorded in the proof with two different formulas - the non-normalised
(when assumed) and the normalised (when used).  Proof substitution
goes inductively on the proof and adds a substitution of n to a fresh
variable while going through the outermost all-intro.  Then, since n
appears freely in the formula of the avar, arename considers that it
is being affected by the substitution (since formula=? is used) and u
is renamed.  However, the other occurrence of the avar with the
normalised (closed) formula is left intact.  The reason is that the
formula=?  check is before the assoc-wrt one.  -- The obvious
correction is to switch the two checks.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-03-31

In typ.scm

Complete test tsubst? for type substitutions added.


In formula.scm

(rename-variables formula) gives an alpha-equal variant of formula
with small indices.  (Work of Simon Huber).


In axiom.scm

check-aconst added: test function for aconsts.  If the argument is not
an aconst, an error is returned.  Complete test psubst? for predicate
substitutions and pinst? for predicate instantiations w.r.t. a type
substitution.

h-deg-violations (parallel to nc-violations) gives the list of names
of aconsts where a pvar whose tvar shows up in the eterm is
substituted by a cterm without computational content.  Reason: this
situation generally produces an error when proof-to-extracted-term is
applied.  Exceptions: the aconsts receiving a special treatment in
proof-to-extracted-term.  add-theorem adapted.


In proof.scm

In check-and-display-proof-aux local test for nc-violations replaced
by a warning.  Test done globally in check-and-display-proof

In an aconst (example: ACNat) substitution of {x|A} for P produces a
warning if tau(P) ne eps but tau(A) = eps.  check-and-display-proof
(which uses check-aconst) at such an aconst gives an error if we are
in a relevant part of the proof.  Reason: cACNat then has argument
type nat=>nat@@alpha66, but its argument has type nat=>nat.


In examples/test

Tests for rename-variables included.


In examples/fan/fanwklu.scm

Directory examples/fan created, and file fanwklu.scm committed.
Contents: Formalization of the equivalence of Fan and a weakened form
of WKL, with EffUniq as an additional hypothesis.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-03-27

psym.scm

In add-ids use of add-algebras-with-parameters for nbe-alg-names
corrected.  Error message improved in case of an inductive definition
not requiring witnesses which has non invariant clauses.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-03-26

etsd.scm

Corrected in case proof-in-ex-elim-rule-form?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2008-03-26

In typ.scm

types-to-embedding applied to pair types returns #f or an error if
no embedding is possible.  (Work of Florian Ranzi)


In grammar.scm

"-->" for impnc.  Token excu added.  prodtype, tensortype and sumtype
made right-associative.


In pconst.scm

In add-rewrite-rule error message improved: arguments in lhs need to
fit the *unsubstituted* type of op


In psym.scm

In add-ids: simultaneously defined idpredconsts are required to be
either all with content or all invariant.  New predicate variables
chosen as general ones, to allow arbitrary substitutions.  Some checks
built in, for instance check for existence of nullary clauses (adapted
from add-algebras-with-parameters by Simon Huber).  Comprehension
terms built with partial variables, to allow substitution of arbitrary
terms.  Totality matters for the abstracted variables of a cterm,
because of the inductively defined existential quantifier.

pvar-to-cterm replaced by the more general predicate-to-cterm

In string-and-arity-and-cterms-to-idpc-parse-function coercions removed.

make-idpredconst checks that in case of a total inductively defined
existential quantifier, that is, ExDT, ExLT, ExRT, ExUT, the
comprehension term has a total variable.  Notice that this property
will not change when a predicate substitution is performed.


In term.scm

make-rename now preserves partiality of variables.  In match-aux and
match2-aux inclusion of cterms in idpredconst was forgotten (work by
Florian Ranzi).

match2-aux needs to build cterms with partial variables.  Hence
type-to-new-var at this place replaced by type-to-new-partial-var.
pvar-to-cterm replaced by the more general predicate-to-cterm


In pp.scm

Adapted to the changes in formula.scm.  token-tree-to-string extended
prod-typeop tensor-typeop sum-typeop made right associative.

To resolve Q'1 vs Q' 1 separator-string treats ' as ^.


In formula.scm

Major changes: addition of impnc.  Binary connectives (bicon) treated
generally.  Inductively defined predicates used to define 
- exd exl exr exu and their variants exdt exlt exrt exut with a total
variable in the clause, and
- andd andl andr andu ord orr orl oru

In make-cterm tests for distinct varsiables added.  We distinguish
{n|A} and {n^|A}, in order to allow the inductively defined
existential quantifier to be restricted to total arguments.

{n|A(n)}r does not give an error if r is not syntactically total.  Its
meaning is Total r & A(r), which is the result after substituting the
cterm {n|A(n)} for Q in Q r.  If r is syntactically total, the result
is A(r).

make-cterm only exceptionally uses total variables.
formula-substitute-aux in case Xr with a predicate variable X and a
cterm {n|A(n)} (with n total) produces Total r & A(r) if r is not
syntactically total, and A(r) otherwise.

Generally we use the abbreviation {n|A(n)} rather than {n^ | Total n^
& A(n^)}.  Therefore cterm-substitute-aux when cterm has the form
{xs^ |P xs^} with a pvar P directly takes the tsubst-value.
(Otherwise the result of P mapsto {xs|A(xs)} would be {xs^ |Total xs^
& A(xs^)}).

Added all-allnc-form-to-final-kernel
imp-impnc-all-allnc-form-to-premises


In axiom.scm

In number-and-idpredconst-to-intro-aconst in case of a total
inductively defined existential quantifier, the param-pvar-cterm is
produced by predicate-to-cterm-with-total-vars .

nc-violations-aux extended by an impnc clause.  

For a clause of an inductively defined predicate we require the form
allnc xs all ys(nc-param-prems --> param-prems -> rec-prems -> P ts)
This is not a heavy rstriction, and it makes some definitions
convenient, for instance, of added-scl-etc-to-proof.

Clauses by default use partial generalized variables.
clause-etc-to-strengthened-clause is changed accordingly.
This does affect proofs involving inductive definitions
(Monika Seisenberger's thesis, work of Klaus Thiel, Freiric Barral,
Stefan Schimanski and Dominik Schlenker), but only in a minor way
(assume needs to be done with partial variables).

Added: clause? strictly-positive?
Changed: imp-formulas-to-uninst-elim-formulas-etc
clause-etc-to-strengthened-clause  

pvar-to-cterm replaced by the more general predicate-to-cterm .
It now uses partial variables

In imp-formulas-to-uninst-elim-formulas-etc pvar-formulas were not
formed correctly.  The fixed pvar associated with I (for ease of
substitution) can have arity (alpha), hence cannot be applied to a
variable of type say boole.  We need a new-var of type alpha.  (Work
of Florian Ranzi)

Axiom InhabTotal added.  Reason: since every algebra is required to
have nullary constructors, every (closed) type rho can be given a
total canonical inhabitant.


In proof.scm

impnc incorporated.  spreading-formula-to-proof
wiping-formula-to-proof isolating-formula-to-proof and
proof-to-goedel-gentzen-translation-aux now use a partial variables to
generate the extra-psubst-gg pvar-to-cterm replaced by the more
general predicate-to-cterm .

In check-and-display-proof-aux inserted check that an elimination
axiom for an invariant idpredconst which is neither special nor
uniform one-clause defined is used with invariant conclusions only.


In pproof.scm

intro-with introduced, with use-with rather than use in case the
arguments cannot be inferred automatically.  elim-intern needs an
additional renaming of vars.  (Work of Florian Ranzi)

casedist-intern compat-at eq-compat-at eq-compat-rev-at compat-rev-at
now build cterm with a new partial variable.
pvar-to-cterm replaced by the more general predicate-to-cterm

Adapted to impnc: assume-intern
fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data

In inversion-intern the instantiated-elim-proof is formed by applying
the generalized elim-formula first to the arguments of the idpredconst
to be inverted, and then to the rest of the free variables in
inst-elim-aconst.  This change is a consequence of necessary
new-var-lists (because of possible type substitutions) in
imp-formulas-to-uninst-elim-formulas-etc

search adapted to impnc.  Postponed: Terminology: clause -> sclause
(for search clause), to distinguish these clauses from those in
idpredconsts.

InhabTotal added to INITIAL-THEOREMS


In ets.scm

In number-and-idpredconst-to-et-constr-term arguments corresponding to
Harrop parameter formulas substituted by Dummy.  Correspondingly, in
proof-to-extracted-term-aux in Intro case make-term-in-const-form
removed.  gind-aconst-to-mr-gind-proof-aux now builds cterm with a
partial test-var

Adapted to impnc: formula-to-et-type idpredconst-to-et-type and others.

mr-invariant? takes invariant-pvars as optional arguments.


In etsd.scm

Corrections (work of Trifon Trifonov).


In lr-dvr.scm

lexer-info adapted to the possibility that taye of variables have
been removed.


In atr.scm

In qf-to-qf-cases-proof cterm built with partial variables


In examples/test.scm

Eqd viewed as a uniform one-clause defined idpredconst, whose
elmination axiom accepts arbitrary formulas.  Tests for EqD as a
uniform one-clause defined idpredconst.  Tests for match2 extended.

Tests for inversion added, also for a simultaneous inductive
definition.  Context: Tait's normalization proof.  Substitutions in
Hancock/Joachimski style, with a trailing number.  Inductive
definition of WN, simultaneously with WNs.

Trifon Trifonov's etsd-test.scm included.


In lib/list.scm

make-cterm used with partial variables only.  ListProjTotal proven,
with axiom InhabTotal.


In lib/listrev.scm

Totality proofs provided, as in lib/list.scm.  ListProjTotal proven,
with axiom InhabTotal.


In examples/bar/bar.scm

Now refers to nat.scm and listrev.scm (rather than the outdated files
nat2.scm and tsil.scm).  (f fbar n) used rather than Init f n.  allnc
in clauses and lemmas only where necessary.  Partial variables used in
clauses.  Totality proofs provided for program constants.


In examples/bar/higman01.scm

Missing universal quantifiers in some clauses of the inductive
definitions for R and TT added.  Now refers to nat.scm and
listrev.scm (rather than the outdated files nat2.scm and tsil.scm).


In examples/bar/higman-finite.scm

Now refers to nat.scm and listrev.scm (rather than the outdated files
nat2.scm and tsil.scm).  allnc in clauses and lemmas only where
necessary.  Partial variables used in clauses.  Totality proofs
provided for program constants.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-12-14

In etsd.scm

An optimization of the extracted Dialectica negative realizer:
do not contract avars foreign to the step proof (done by Trifon Trifonov)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-12-05

In etsd.scm

Treatment of "and" and of "Eq-Compat" added.  pvar-to-var replaced by
pvar-to-d-pvar.  Case distinctions unified.  Treatment of gind is
included, but in this file temporarily disabled.  (Done by Trifon
Trifonov and Simon Huber; their last modification 2007-09-06)

In list.scm

check-all and check-exists added

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-11-29

In proof.scm

Changes concerning aconst substitution fixed bug with incorrect
rename-free calculation (Trifon Trifonov, 28 Nov 2007)

aconst-substitute-aux: Removed unnecessary parameters.  Returns only
the new-aconst as a result

proof-substitute-aux: changes in proof-in-aconst-form and
proof-in-allnc-elim-form

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-11-26

In lib/nat.scm 

Totality proofs added.

In axiom.scm

If a theorem "CTotal" is added with "C" the name of a program
constant, then change-t-deg-to-one is called.

Axiom "Total" formulated with quantifiers with content.  This is
necessary when All-AllPartial is used in totality proofs.

final-substring? added

In examples/fibonacci/fib.scm

Updated.  The graph of the Fibonacci sequence is inductively defined.

In atr.scm

atr-irrel-goal-proof atr-arb-definite-proof now work for arbitrary
prime formulas.  Terminology corrected, and some typos removed.

id.scm

Compatibility and EfEq  theorems added.

boole.scm
Computation rules for AndConst ImpConst OrConst replaced by more
useful overlapping ones

pconst.scm

Warning added in case t-deg-one is stated and totality has not been
proved before.

add-computation-rule now allows overlapping left hand sides, provided
the right hand sides are made equal by the unifier.

Double occurrence of constr-name? removed

proof.scm
Double occurrence removed: proof-in-beta-normal-form?
proof-in-intro-form-to-kernel-and-vars

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-09-18

pproof.scm
(casedist test) replaces the goal A by two new goals
  (atom test) -> A[True/test]
  ((atom test) -> F) -> A[False/test]
and (this is new) if test is not total also
  STotal test
To this end, dec-stotal-cases-proof is added (work done by Simon Huber).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-09-13

pproof.scm
use2-intern corrected.  match2 cannot find a tsubst plus a pinst in
case (Pvar alpha)x is to be a pattern for a formula A.  Therefore the
types of the used formula are considered fixed, and we only rename the
pvars to let match2 work correctly.  (Following proposals of Florian
Ranzi)

For use-with, in its auxiliary function
x-and-x-list-to-proof-and-new-num-goals-and-maxgoal error messages
made more informative.

error messages in use-intern in case of missing terms now refer to the
original variable in the used formula even if such variables had to be
renamed.

term.scm
match-aux and match2-for-tsubst-aux corrected: In the abstraction and
quantifier cases computation of prev should only be attempted if
tsubst-from-types is not #f.

In match2-for-tsubst-aux and match2-aux typo corrected: 
;- 			 (and (equal? pred pred2)
;+ 			 (and (equal? pvar pred2)

(Done by Florian Ranzi).

formula.scm
alpha-equal-formulas-to-renaming added.
formula-to-vars-and-kernel removed.

proof.scm
thm-or-ga-name-to-proof added (simplifies use-intern)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-09-10

pproof.scm axiom.scm ets.scm
tensor ! removed from proofs.  Reason: The tensor is used with
classical existential quantifiers only.  Hence it does not appear in
unfolded formulas, and should not have proof rules.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-09-07

typ.scm
In add-algebras-with-parameters, check for non-emptyness of algebras added

proof.scm
Special treatment for substitution of aconsts in rule form so that
they remain in rule form after substitution.  Needed for Dialectica
extraction (2007-09-03, Trifon Trifonov).  In particular:

proof-substitute-aux adapted to use the aconst-substitute-aux
function.  aconst-substitute-aux is used twice: (1) In aconst in rule
form (i.e., with nc-elims) - perform manual normalization so that the
aconst remains in the same form.  (2) In the other cases of aconst
appearing - kept previous behaviour.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-09-06

modules/atr.scm
Removed.  Should also be removed from TAGS

pe07.scm
Removed.

pconst.scm
display-program-constants rewritten.  It now displays the constants in
the given order.

pproof.scm
unnecessary cvars removed in strip-intern.

numbers.scm 
Missing rewrite rules added (a+0 -> a etc).  Exponents with type
different from int admitted, without a separate treatment of double
association lists (cf. constr-name-and-tsubst-to-constr in pconst.scm).
The name of the Exp-function is determined by the value type.

Degree of totality corrected to t-deg-zero for RatDiv RealDiv CpxDiv
and exponentiation with possibly zero basis and negative exponent
(RatExp RealExp CpxExp).

term-to-t-deg-aux changed in case of division by a non-zero term, or
exponentiation of zero with a negative exponent.

examples/analysis/real.scm
examples/analysis/cont.scm
examples/analysis/extraction.scm
adapted to the changes in numbers.scm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-08-24

In typ.scm
types-to-embedding corrected and cleaned up.

In pconst.scm
Introduced argument comes first in elimination operators 
(changes by Simon Huber)

Changed: rec-const-to-uninst-arrow-types 
arrow-types-to-uninst-paramless-recop-types-and-tsubst
arrow-type-to-uninst-paramless-casesop-type-and-tsubst
rec-at
cases-at
const-substitute

Added: nbe-object-rec-compose

In psym.scm
predicate-to-cterm uses partial variables, for clarity when exi is used
idpredconst-to-string now uses separator-string for exi and exid

In term.scm
In term-in-const-form-to-string, "Cases" alg-type is (car arg-types).
Vector notation for recursion adapted.
rec-op-and-args-to-if-term adapted.

In formula.scm
Added: inductively defined conjunction AndL AndR AndLR AndNC with the
infix notation andl andr andlr andnc (so "and" is for the boolean
and-op)

In boole.scm
Tokens "andl" "andr" "andlr" added

In axiom.scm
Introduced argument comes first in elimination operators.  Adapted
all-formulas-to-uninst-imp-formulas-and-tpinst
all-formula-to-uninst-cases-imp-formula-and-tpinst
imp-formulas-to-uninst-elim-formulas-etc

In proof.scm
Introduced argument comes first in elimination operators.  Adapted
proof-in-ind-rule-form?
proof-in-cases-rule-form?
elim-npterm-and-var-genavar-alist-to-proof
proof-of-stab-at-aux
proof-of-efq-at-aux

In pproof.scm
Introduced argument comes first in elimination operators (changes by
Simon Huber).  Adapted

atom-true-proof
atom-false-proof
efq-atom-proof
stab-atom-proof
imp-to-atom-proof
and-atom-to-left-proof
and-atom-to-right-proof
atom-to-imp-proof
atoms-to-and-atom-proof
ind-intern
cases-intern
dec-cases-proof (with (Pvar boole) instead of (Pvar boole)^)
inversion-intern
make-gind-aconst
make-min-pr-aconst

Added:

pproof-all-intro does an all-intro without changing the maxgoal number
pproof-imp-intro does an imp-intro without changing the maxgoal number

Rewritten:
elim (now accepts an optional idhyp, similar to ind)
elim-intern
simelim
simelim-intern

In pp.scm
separator-string changed

In ets.scm
Introduced argument comes first in elimination operators (changes by
Simon Huber).  Adapted

cases-aconst-to-if-term
imp-formulas-to-et-rec-const
all-formulas-to-mr-ind-proof-aux
all-formula-to-mr-cases-proof-aux

In all-formulas-to-mr-ind-proof-aux definition of mr-step-formulas
corrected.  Similar correction in all-formula-to-mr-cases-proof-aux

Changes in the example files
quant/orevkov.save warshall/warshall.save dijkstra/count.save dijkstra/pick.scm dijkstra/dijkstra.save classical/root.save classical/wftest.scm bar/bar.save bar/higman01.save dc/dc-first.save


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-08-17

In term.scm (changes by Trifon Trifonov)

Missing recursive calls to if-term-to-eta-expansion added.
normalize-term-pi-with-rec-to-if and if-term-to-eta-expansion defined
using generic helper functions.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-30

In pe07.scm

proof-of-stab-at-aux and proof-of-efq-at-aux adapted to new order of
args in cases-aconst

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-28

In list.scm

Insertion sort (from examples/analysis/simpreal.scm, moved here.

In term.scm

Second order matching added.  match2 decides whether there is a
solution.  In the positive case it returns one "most detailed"
solution.  Heuristics: Fit largest rigid arguments first.  Ignore
flexible arguments.  match2 allows to have use2 in addition to use.
use2 tries to automatically infer instances of second order
predicate and object variables.  This is not always what one wants.
For example, match2 with

(define used-formula (pf "as865 m867<=1/2**k866")) 

(define goal-formula (pf "as(M(k+1))<=1/2**(k+1)"))

instantiates the second order variable as865 and gives the result

as865 -> [n868]as(M(k+1)) k866 -> k+1

Forbidden variables removed from (first and second order) matching,
since they are not necessary.

DIALECTICA-FLAG formula-of-nulltypep? and formula-of-nulltypen? added.
We temporarily stipulate that inductively defined predicates have
neither positive nor negative content.

In formula.scm

display-substitutions added.  Displays type-, object- and
predicate-substitutions

In pproof.scm

Argument forb-vars in first-match removed.  use2 added, based on
second order matching.

Extension of use (done by Florian Ranzi).  If first order matching
(done via use-intern) fails, second order matching is tried (via
use2-intern).  Error messages in case of missing terms/cterms improved.

hyp-info-to-leaf made cleaner, by removing the special treatment of
an assumption constant with a nullary predicate variable at the end.

In lnf.scm

proceed adapted to new format of results of
fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data.
Old code removed.

In etsd.scm

formula-of-nulltypep? and formula-of-nulltypen? moved into term.scm.

In prop.scm

prop-intern removed.  Error messages improved.

In id.scm

Adapted to the new notation for pvars

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-27

In atr.scm

Non-definite premises allowed in
atr-min-excl-proof-to-bot-reduced-proof and in
atr-min-excl-proof-to-intuit-ex-proof

In examples/Makefile

Directory dc added again

In examples/dc/dc-dirst.scm

Minor adaptions


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-25

In term.scm

term-to-expr corrected (following a proposal of Trifon Trifonov)

In grammar.scm positive-content, negative-content exchanged with
no-positive-content, no-negative-content.

In psym.scm

Every predicate variable carries a pair h-deg, n-deg.  This
restricts the admitted comprehension term {x|A} as follows.
h-deg  n-deg   tau^+(A)    tau^-(A) 
  0      0     arbitrary   arbitrary 
  1      0     nulltype    arbitrary 
  0      1     arbitrary   nulltype
  1      1     nulltype    nulltype

In add-ids clause-strings-with-hat removed, and general pvars used

In pproof.scm

dec-cases-proof with (Pvar boole) instead of (Pvar boole)^

In proof.scm

Comment for classical logic changes:  Pvar^ replaced by Pvar.
proof-of-efq-at-aux treats existential formulas without Efq

In boole.scm

falsity-log redefined with h-deg-zero and n-deg-zero

In formula.scm

In formula-substitute-aux special treatment of falsity-log removed

In ets.scm

In Efq and Stab global assumptions, id-proof: Pvar^ replaced by Pvar

In axiom.scm

In make-pvar 0 0 replaced by h-deg-zero n-deg-zero

In examples/dijkstra/count.scm

In NatLtSuccElim Pvar^ replaced by Pvar

In examples/dijkstra/wf.scm

Pvar^ replaced by Pvar

In examples/dijkstra/dijkstra.scm

Pvar^ replaced by Pvar

Moved dijkstra.out into dijkstra.save

In atr.scm (moved to src)

allnc and exnc admitted.  atrX removed.

In init.scm

atr.scm moved back into src from modules

In examples/classical/root.scm examples/classical/wftest.scm

Adapted

In lib/nat.scm

Pvar^ replaced by Pvar

In lib/list.scm

(Pvar nat)^ replaced by (Pvar nat)

In lib/minpr.scm

(Pvar alpha)^ replaced by (Pvar alpha).  Arguments of make-pvar adapted

In lib/minpr_gen.scm

Arguments of make-pvar adapted

In lib/exc.scm

Pvar^ replaced by Pvar

In quant/los.scm

bot replaced by F

In examples/Makefile

Directory dc temporarily removed

In examples/analysis/cont.scm

DC, IP, AC formulated with Pvar^ (no positive content)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-17

In pconst.scm

Double definition of constr-name-to-constr removed.  The one using
opt-pvar-to-tvar deleted.

In typ.scm
types-to-embedding extended to types with parameters

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-12

In formula.scm

formula-to-token-tree in case exca, excl needs to keep the list of
variables.

In pp.scm

token-tree-to-string and token-tree-to-varstrings-and-kernel adapted
to exca, excl with list of vars as first arg

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-07-11

In axiom.scm
all-formulas-to-cases-aconst -> all-formula-to-cases-aconst

In pconst.scm
cases-const-to-param-types corrected (as done by Simon Huber)
Comment added:
; Format of type-info-or-repro-formulas: (1) For a rec-const.  (a)
; Ordinary pconst: (k param-type1 ... arrow-type1 ...).  The number k
; indicates how many of the following types are parameter types.  (b)
; From an ind-aconst (while normalizing).  all-formulas.  (c) From an
; elim-aconst (while normalizing).  imp-formulas.  (2) For a
; cases-const.  Here a single arrow-type or all-formula suffices.  (a)
; Ordinary pconst: (param-type1 ... arrow-type).  (b) From a
; cases-aconst (while normalizing).  all-formula.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done locally 2007-03-07

lib/realsimp.scm removed.  
Superseded by examples/analysis/simpreal.scm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-03-07

In examples/arith/sqrttwo.scm

Adapted to the new nat.scm

In axiom.scm

(search-about string) searches in THEOREMS and GLOBAL-ASSUMPTIONS
for all items whose name contains string.

Adapted to the new add-rewrite-rule, which generates a RewriteGA
in case no proof is provided:

examples/dijkstra/count.save
examples/dijkstra/dijkstra.save
examples/dc/dc-first.save
examples/bar/bar.save
examples/bar/higman01.save

In examples/analysis/real.scm 

(Rec real=>pos=>rat)([as2,M3,n4]as2(M3 n4)) now prints as
[x0,n1][if x0 ([as2,M3]as2(M3 n1))]
(was previously in realcorr.scm, which has been removed now).

Change: based on the new (cleaned) nat.scm and numbers.scm, which
allows to work with pos and nat simultaneously.  Cauchy sequences have
type nat=>rat, and Cauchy moduli have type int=>nat.

examples/analysis/cont.scm

Corrected the uniform modulus of continuity for the square function.
Removed unnecessary "Id" theorem (now in src/ets.scm).
ACT, IPT (T for total) renamed into AC, IP
(was previously in contcorr.scm, which has been removed now).

Change: based on the new (cleaned) nat.scm and numbers.scm, which
allows to work with pos and nat simultaneously.  Cauchy sequences have
type nat=>rat, and Cauchy moduli have type int=>nat.

examples/analysis/extraction.scm

Corrected the uniform modulus of continuity for the square function
(was previously in extractioncorr.scm, which has been removed now).
Uses (libload "realsimp.scm") instead of (load "simpreal.scm");
simpreal.scm removed.
less-expr etc removed, because of the new term-to-expr

Change: based on the new (cleaned) nat.scm and numbers.scm, which
allows to work with pos and nat simultaneously.  Cauchy sequences have
type nat=>rat, and Cauchy moduli have type int=>nat.

examples/analysis/simpreal.scm

Temporary file.  provides ord-field-simp-bwd, which should be replaced
by reflection.

alg nat is present.  Cauchy sequences have type nat=>rat, and Cauchy
moduli have type int=>nat.

Some functions previously in numbers.scm are now provided here:
int-term-to-rat-term pos-term-to-rat-term real-numeric-term-to-number
int-numeric-term-to-number rat-numeric-term-to-number
is-rat-numeric-term?  pos-term-to-int-term and similar ones.

In lib/list.scm 

- (token for NatMinus) changed into the new token -- (cut-off minus)

In var.scm

remove-var-name only gives a warning (not an error) if the variable
name does not exist.

In boole.scm

Rewrite rules for the boolean constants commented out.  They should
added as computation rules, once consistent overlaps of computation
rules is implemented.

In numbers.scm (based on examples/analysis/numbersnat.scm)

For reals, the Cauchy sequences "as" "bs" "cs" "ds" have type "nat=>rat"
and the Cauchy moduli "M" "N" have type "int=>nat".

In nat.scm (not yet in lib, but in examples/analysis)

All rewrite rules proved.  Major cleanup, following Klaus Thiel's
version of nat.scm (in exampeles/ordinals).  remove-nat-tokens
enhanced by (partial) removal of display items.

In term.scm

In term-to-expr, terms in numeric form wrt either pos or nat are both
displayed as the corresponding number.  Therefore both
is-numeric-term-wrt-pos? and is-numeric-term-wrt-nat? have been moved
to term.scm, and similarly numeric-term-wrt-pos-to-number and
numeric-term-wrt-nat-to-number.  The function is-pos-numeric-term?  is
replaced by is-numeric-term-wrt-pos?, and is-int-numeric-term? is
changed accordingly.

Scheme definitions of |IntS|, |IntToNat| added (for term-to-expr)

Definition of separator-string moved to pp.scm

Typo in definition of |cDC| corrected.

In pp.scm

Definition of separator-string moved here from term.scm

In typ.scm

Subtype relation generated from pos < nat< int < rat < real < cpx

View pos, nat, int, rat, real and cpx as algebras, with constructors
pos: One SZero SOne 
nat: Zero Succ
int: IntPos IntZero IntNeg
rat: RatConstr (written # infix) and destructors RatN RatD
real: RealConstr and Destructors RealSeq RealMod
cpx: CpxConstr (written ## infix) and destructors RealPart ImagPart

We use a global variable ALGEBRA-EDGE-TO-EMBED-TERM-ALIST
initially set to '().

term-to-original returns the original of a term under possibly
repeated embeddings stored in ALGEBRA-EDGE-TO-EMBED-TERM-ALIST

types-to-coercion renamed into types-to-embedding.  type-leq? renamed
into type-le?

In pproof.scm

In set-goal the argument can be string, to be parsed into a formula
Admit-GA renamed into AdmitGA

In pconst.scm

add-computation-rule now accepts two strings.  add-computation-rules
accepts an even number of arguments.  add-rewrite-rule (with
abbreviation arw) now takes a optional proof argument.  If no proof
is given, a global assumption RewriteGA is generated.

In lib/realsimp.scm

Leq, Less renamed in Le, Lt.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-01-29

In proof.scm

In make-arename classical-formula=? replaced by formula=?
Reason: classical-formula=? checks whether the normal forms are equal.
But in arename we want syntactic equality, i.e., formula=?

In proof-substitute-aux the aconst case has been corrected: new vars
is psubst should not cause renaming.

In examples/classical/gcd/gcd.scm

Adapted to the present atr.scm, which works with proof substitutions

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2007-01-20

init.scm

Code for comments moved to here.

list.scm

alist-to-multivalued-alist-wrt added.  It transforms ((x1 y1) (x2 y2)
...) into ((z1 y11 y12 ...) (z2 y21 y22 ...) ...) with distinct zi's.

list-to-left-associated-list and non-null-list-to-app-expr added:
(list-to-left-associated-list '(0 1 2 3)) => (((0 1) 2) 3)

Code for comments moved to init.scm.

pconst.scm

cases-const-to-param-types needs to take care of the case that
type-info-or-repro-formulas is a type info
add-program-constant gives no comment for "cId"

term.scm

term-to-term-with-let introduced.  It hand optimizes a term by
searching for its longest duplicate subterm, and taking that subterm
out via a let.  term-to-expr rewritten.  Aim: produce a readable
scheme expression that can be evaluated.

examples/bar/higman01.save changed accordingly: ((= a1) a2) -> (= a1 a2)

atr.scm

imp-const and and-const moved into boole.scm
qf-to-term moved to formula.scm

formula.scm

qf-to-term moved here (from atr.scm).
illegal-tensor? replaced by formula-with-illegal-tensor?

boole.scm

imp-const and-const or-const neg-const added

axiom.scm

add-theorem gives no comment for the "Id" theorem

arity-to-new-non-harrop-pvar -> arity-to-new-general-pvar in
all-formulas-to-uninst-imp-formulas-and-tpinst
all-formula-to-uninst-cases-imp-formula-and-tpinst
ex-formula-to-ex-intro-aconst
ex-formula-and-concl-to-ex-elim-aconst
exnc-formula-to-exnc-intro-aconst
exnc-formula-and-concl-to-exnc-elim-aconst

proof.scm

PVAR-TO-TVARP-ALIST  PVAR-TO-TVARP
PVAR-TO-TVARN-ALIST  PVAR-TO-TVARN added.
proof-to-final-imp-elim-op and proof-to-imp-elim-args added
proof-to-final-allnc-elim-op added

Problems with proof-to-expr-with-types: (1) multiple occurrences of
avars displayed many times.  (2) bound avars with no occurrence in the
kernel not shown.  Replaced by proof-to-expr-with-formulas (showing
all aconsts, free avars and bound avars with their formulas), and
proof-to-expr-with-aconsts.

expand-theorems-with-positive-content added
proof-to-proof-parts added
proof-in-ind-rule-form? proof-in-cases-rule-form?
proof-in-ex-elim-rule-form? added

pproof.scm
illegal-tensor? replaced by rewritten formula-with-illegal-tensor?

ets.scm

Id: Pvar^' -> Pvar^' added as initial theorem.

cont.scm

Supply of theorem Id removed.  It now is always a theorem.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-09-16

var.scm

var-to-string made clearer and simplified.  Now "_" is only used where
really necessary.  Examples: In (nat=>nat)7 the 7 is understood as an
argument.  When we want an index, we must use (nat=>nat)_2 7.


examples/dijkstra/dijkstra.save
examples/bar/bar.save
examples/bar/higman01.save

Adapted to the simpler print-strings for variables.

psym.scm

pvar-to-string adapted to possible positive and negative content
(needed to the implementation of the Dialectica interpretation).

formula.scm

Better error messages for make-predicate-formula

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-05-30

pp.scm

We define token-tree-to-string and use this for all display purposes
(for types, terms and formulas).  For line breaks,
token-tree-to-pp-tree and pp-tree-to-string are provided (following
Stefan Schimanski)

Flag DOT-NOTATION introduced; default is #t.  If set to #f, the
display is "all n(A -> B) -> C" instead of "(all n.A -> B) -> C".


axiom.scm ets.scm grammar.scm psym.scm boole.scm formula.scm
pproof.scm atr.scm

Format of pvars changed, to prepare for a treatment of the Dialectica
interpretation.  Instead of the Harrop degree, which could be 0
(general, display "P^") or 1 (Harrop formula, that is, no
computational content, display "P"), we now have two fields: the first
one holding 'positive-content or 'no-positive-content, and the second
one holding 'negative-content or 'no-negative-content.  For example,
"ex n T" has positive-content but no-negative-content, "all n T" has
no-positive-content but negative-content, "ex n all m T" has
positive-content and negative-content.  Display: "P" "P1" in case of
'no-positive-content and 'no-negative-content, "P^" "P^1" in case of
'positive-content and 'no-negative-content, "P'" "P1'" in case of
'no-positive-content and 'negative-content, "P^ '" "P^1'" in case of
'positive-content and 'negative-content.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-05-13

boole.scm unicode.scm

neg-op replaced by prefix-op.

proof.scm

tensor eliminated; it is only used as an abbreviating device for
classical formulas

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-05-09

dijkstra/wf.tac
dijkstra/pick.tac

Comments added with necessary animations, in order to make the
soundness proofs correct.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-05-09

ets.scm 

proof-to-soundness-proof-aux corrected: in case theorem one needs to
bind the free vars in inst-proof.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done locally 2006-04-12

doc/mlcf.tex

Some typos corrected.
instanciate -> instantiate

examples/tait/sn.scm

instanciate -> instantiate

examples/fan/fanequiv.scm

instanciate -> instantiate

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
<<<<<<< log.txt
Done 2006-05-05

term.scm

Problem: (boole1=boole2)=True prints as boole1=boole2=True.  Solution:
In token-tree-to-string and token-tree-to-ppstring, if the operator as
well as an argument has token-type rel-op or relterm, then the
argument needs parentheses.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
=======
Done locally 2006-04-19

lib/nat.scm

Rewrite rule n<n -> False added (courtesy of Monika Seisenberger)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-04-19

pconst.scm

remove-rewrite-rules-for and remove-computation-rules-for corrected.
They now use match (instead of unify) to check whether a lhs of a rule
has the form of the given term.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
>>>>>>> 1.36
Done 2006-04-17

term.scm

mk-term-in-if-form and some associated functions reintroduced;
they are needed for Dan Hernest's implementation of functional 
interpretation


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-04-13

pproof.scm

(undoto n) allows to go back to a previous pproof state whose (top)
goal had number n (code due to Markus Sauermann)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-04-12

formula.scm

make-=-term added, and used for make-=

term.scm

normalize-term-pi-with-rec-to-if corrected.
test-and-gen-args-to-if-nf and all mention of gen-arg removed: obsolete

instanciat -> instantiat

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-02-21

pproof.scm

In by-assume also numbers admitted as labels for hypotheses

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-02-21

examples/classical/dickson.tac
examples/classical/wftest.tac

Adapted to the cleanup concerning classical existential quantifiers,
course-of-values induction and the minimum principle.  No more need to
rerun interactive proofs: the necessary auxiliary theorems are created
silently.  lib/minpr.scm and lib/minpr_gen.scm made obsolete.

pproof.scm

Cleanup concerning classical existential quantifiers, course-of-values
induction and the minimum principle.  No more need to rerun
interactive proofs: the necessary auxiliary theorems are created
silently.  lib/minpr.scm and lib/minpr_gen.scm made obsolete.

Added: make-cvind-aconst.  It takes a positive integer n and returns an
assumption constant for course-of-values induction w.r.t. a measure
function of type alpha1 => ... => alphan => nat.

make-min-pr-aconst.  It takes positive integers m,n and returns an
assumption constant for the minimum principle w.r.t. a measure
function h of type alpha1 => ... => alphan => nat.

make-exc-intro-aconst.  It takes positive integers m,n and returns an
assumption constant for exc-introduction w.r.t. n variables of type
alpha1 to alphan.

make-exc-elim-aconst.  It takes positive integers m,n and returns an
assumption constant for exc-elimination w.r.t. n variables of type
alpha1 to alphan.

In exc-formula-to-exc-intro-aconst and similarly in
exc-formula-and-concl-to-exc-elim-aconst there is no need any more to
rerun the interactive proof.

exc-formula-and-measure-to-min-pr-aconst replaced by
exc-formula-to-min-pr-aconst

by-assume-minimal-wrt rewritten.  Suppose we are proving a goal G from
a classical existential hypothesis ExcHyp: exc x1..xn.A1 !..! Am.
Then by the minimum principle we can assume that we have x1..xn which
are minimal w.r.t. a measure h such that A1..Am are satified.

by-assume (replaces by-assume-with) now works for existential
hypotheses ex x A, exnc x A, exc x1,..,xn.A1!..!Am

Auxiliary functions: make-fixed-tvars, make-fixed-pvar,
make-fixed-pvars, make-fixed-measure-var, make-fixed-vars

display-current-pproof-state now takes an optional proof argument

instanciat -> instantiat

formula.scm

formula-to-string treats tensor as right-associative

pp.scm

tensor-op treated as right-associative

lib/nat.scm

Theorem "NatLtLtSuccTrans" added (used for make-cvind-aconst)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-01-15

proof.scm

Definition of proof-substitute-aux corrected in aconst-case.
instanciate -> instantiate

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-01-09

In examples/classical/dickson.tac

The final test (giving 3@4) now works as it should (after correcting
proof-substitute-aux in proof.scm).  Unnecessary (and meaningless)
free variable n (which showed up in the extracted term) replaced by 0.
Name "DicksonTwo" introduced for the (classical) proof.

In examples/analysis/real.scm

"RatAbsEq" renamed into "RatAbsCompat"

In term.scm

In term-to-expr, Less, Leq replaced by Lt, Le

In proof.scm

Correction of proof-substitute-aux for all-intro, allnc-intro

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2006-01-03

In pproof.scm

fla-and-sig-tvars-and-vars-and-goal-fla-to-fst-match-data corrected:
when computing match-res, in case (predicate-form? used-formula),
(predconst-form? predicate) had to be checked first

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2005-12-08

examples/pruning/align.scm added

In typ.scm

tsubst-match added

In pconst.scm

add-computation-rule simplified (and corrected) in the case of a
nullary pconst.  Remove the entries which are of the form of the
tsubst of the pconst in the lhs in the tsubst-obj-alist for
pconst-name in PROGRAM-CONSTANTS.  Add a new entry with the object for
the rhs.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 2005-12-05

doc/mlcf.tex

In proof-to-soundness-proof for exnc-intro in case tau(A) ne nulltype
parameters for new exnc-intro-axiom corrected.  Similarly for the
cases axiom.

In typ.scm
  type-unify added, by adapting unify (for terms).  Notice that
  extending the treatment in modules/type-inf.scm is no good.  There
  it is assumed that all types are built from type variables by arrow
  and star, hence equal type constants do not unify.

  Error messages in is-used? cleaned up

  make-inhabited removed.  Use add-computation-rule instead.  Example:
  (add-computation-rule (pt "(Inhab boole)") (pt "False"))

  type-to-canonical-inhabitant adapted to "Inhab"

  Global variable TYPES-WITH-CANONICAL-INHABITANTS removed


In term.scm

  In disagreement-pair constants are now compared with const=?, rather
  than only equality of their names.

  Totality constraints now respected by match-aux

In examples/warshall/warshall.tac

COMMENT-FLAG set to #f in the initial loading of nat.scm and list.scm

In examples/classical/root.tac

COMMENT-FLAG set to #f in the initial loading of nat.scm
COMMENT-FLAG set to #f when loading atr.scm

In examples/classical/wftest.tac

COMMENT-FLAG set to #f in the initial loading of nat.scm
COMMENT-FLAG set to #f when loading atr.scm

In examples/dc/dc-first.tac

COMMENT-FLAG set to #f in the initial loading, afterwards 
COMMENT-FLAG set to #f

In lib/minpr.scm

COMMENT-FLAG set to #f in the initial loading of nat.scm.  In the
proof of "Min-Pr-a-1-1" use replaced by use-with, because there is a
clash of tvars.  General variable names used.  Uses theorems in
nat.scm rather than a global assumption.  The name Cv-Ind has been
changed to CVInd (no "-" to allow the parser to read cCVInd)

In lib/nat.scm

Bounded universal quantifier added as a boolean constant.  Rewrite
rules adapted to partial variables.  Cleaned up.  Theorems added.
max and min added.

In lib/list.scm

The proof of LhConsn used Pred(Succ nat1-nat^2) |-> nat1-nat^2 as a
rewrite rule, which (correctly) does not hold for the partial nat^2
any more.

Adapted to introduction of "Inhab", and somewhat extended (parallel
to the new listrev.scm)

In lib/listrev.scm

Initial commit.  Lists written in reverse order.  Intended to replace
tsil.scm (by Monika Seisenberger).  Changes:
:: now is an add-op, hence left-associative.  Display: :0::1::2::3
Notice that tsil.scm and list.scm cannot be loaded together.
Reason: In :0::1::2::3 the ":" is a prefix-op for tsil but a
postfix-op for list.
Hence replace "tsil" -> "list", "snoc" -> cons", "lin" -> "nil"
Theorem "ListNilAppend" proved, and added as rewrite rule
++ replaced by Succ
"ListProj" considered as a partial program constant
"ListMap" used as binary program constant, written infix as map
Lead, Last replaced by Bar, __
Theorems "LhMap" and "MapAppend" added
"ListZip" and "ListUnzip" added as program constants
"ListFzip" and "ListFunzip" added as program constants
Theorem "ListMapFbar" added as rewrite rule

In boole.scm

ImpConst and some boolean proofs transferred from atr.scm here.
OrConst and NegConst added.

Program constant "Inhab" added: a constscheme providing a canonical
inhabitant of an arbitrary type.  It can be given a concrete value.
Example: (add-computation-rule (pt "(Inhab boole)") (pt "False"))

In pconst.scm

"AndConst" replaced by "Inhab" "AndConst" "ImpConst" "OrConst" "NegConst"
to hide noise when loading the system

nbe-pconst-and-tsubst-and-rules-to-object made more general: In case
(zero? arity) pconst can have instantiated tvars.

In add-computation-rule the corresponding test has been changed.  It
now is possible to add the computation rule (pt "(Inhab term)") -->
(pt "Var 0").

In axiom.scm

Error message in add-global-assumption made better: unexpected free
variables are displayed

In modules/atr.scm

ImpConst moved (slightly changed) into boole.scm.
imp-to-atom-proof moved into pproof.scm (it is needed for assume)
atom-to-imp-proof moved into pproof.scm (it is needed for 
x-and-x-list-to-proof-and-new-num-goals-and-maxgoal)


In pproof.scm

In x-and-x-list-to-proof-and-new-num-goals-and-maxgoal the atom case
needs to be extended to andb, impb.
fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data adapted to andb,
impb.  Hence "use-with" and "use" are now applicable for andb, impb
formulas as used formulas.
assume now works for a boolean goal boole1 impb boole2
We could also extend use-with, use, assume to "AllBNat".  However,
it seems easier to use "AllBNatIntro" and "AllBNatElim" instead.

x-and-x-list-to-proof-and-new-num-goals-and-maxgoal corrected: it
now treats types and cterms in x-list by means of simultaneous
substitutions.

use-intern enhanced: it now renames type variables, to let match
work correctly in case of clash of tvars.

eq-compat-at corrected

simp-with-intern corrected: it now looks for nkernel in the
normalized goal formula, as it should

simphyp-with and simphyp added

Cleanup of compat-at, used in simp: it is not necessary to generate
global assumtions.  For every finitary algebra we can prove
compatibility with = from Eq-Compat and =-to-Eq.  This proof is
automatically generated.  Similarly for compat-rev-at, using Eq-Symm

  Global variable TYPES-WITH-CANONICAL-INHABITANTS removed

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-11-17

lr-dvr.dvm

string-reader rewritten in error case, to cooperate with myerror

pproof.scm

eq-compat-at corrected: formula-of-eq-compat-aconst was not defined

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-11-11

axiom.scm

exnc-formula-to-exnc-intro-aconst corrected: it should start with allnc

pproof.scm

In eq-compat-at order of variables corrected

ets.scm

real-and-formula-to-mr-formula-aux corrected in cases exnc, allnc
In proof-to-soundness-proof-aux case for exnc intro introduced:
exnc-formula-to-exnc-intro-mr-proof-aux added

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-11-03

typ.scm

RESERVED-NAMES extended by STotal.

pconst.scm

The argument pvar-to-tvar is removed in all-formulas-to-rec-const and
imp-formulas-to-rec-const; we now refer to the global variable.
Similar: all-formula-to-cases-const.  opt-pvar-to-tvar removed in
constr-name-to-constr and ex-formula-to-ex-intro-const and
number-and-idpredconst-to-intro-const and
ex-formula-and-concl-to-ex-elim-const.  In const-substitute initial
test introduced whether the type substitution is empty.

psym.scm

Format of IDS changed: all clauses now have names (normally provided
by the user, but names like "AccOne" are created if none are given),
and are added as theorems.  add-ids changed accordingly.
predicate-to-tvars added.

formula.scm

formula-to-tvars changed: tvar for cterms of idpcs taken into account.
nbe-formula-to-type needs a procedure associating type variables to
predicate variables, which remembers the assignment done so far.
Therefore it (now) refers to the global variable PVARS-TO-TVARS.  In
formula-substitute-aux it is now checked that for a pvar without cc
(h-deg 1) only a cterm without cc is substituted.

axiom.scm

all-allpartial-aconst renamed into allnc-allncpartial-aconst.
all-allpartial-aconst with all for allnc added.  Similar for
allpartial-all-aconst, and for ex.  In ex-formula-to-ex-intro-aconst
the new pvar for uninst-ex-intro-formula has h-deg 0 if the kernel has
computational content and h-deg 1 otherwise.  Similar for
ex-formula-and-concl-to-ex-elim-aconst and
exnc-formula-to-exnc-intro-aconst and
exnc-formula-and-concl-to-exnc-elim-aconst.
theorem-or-global-assumption-to-pconst now refers to the global
variable PVARS-TO-TVARS.  number-and-idpredconst-to-intro-aconst
adapted to new format of IDS.

proof.scm

make-pvar-to-tvar deleted.  Global PVAR-TO-TVAR used instead.  In
proof-and-genavar-var-alist-to-pterm and proof-to-pterm the argument
pvar-to-tvar is replaced by a reference to the global variable
PVAR-TO-TVAR.  In proof-substitute-aux in case aconst renamining in
case of `clashes' removed: pinst0 is allowed to contain variables
already in uninst-formula0

pproof.scm

use-intern and simp-intern now also work in case COMMENT-FLAG = #f and
the terms provided are too many.

ets.scm

PVAR-TO-TVAR-ALIST, INITIAL-PVAR-TO-TVAR-ALIST and PVAR-TO-TVAR moved
to proof.scm.  Reference to PVARS-TO-TVARS introduced in
formula-to-et-type idpredconst-to-et-type all-formulas-to-et-rec-const
cases-aconst-to-if-term number-and-idpredconst-to-et-constr
imp-formulas-to-et-rec-const make-pvar-to-mr-pvar
real-and-formula-to-mr-formula-aux

modules/atr.scm

Cleanup in atr-proof-to-extracted-term.  Issue: how does it cooperate
with the global PVAR-TO-TVAR.  The update of PVAR-TO-TVAR-ALIST should
happen only once.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-18

pproof.scm

In elim and inversion, generated clauses are proved automatically
whenever this is obvious.  imp-formulas not provided are taken as J xs
-> L xs.  Generated clauses for such J are proved automatically from
the intro axioms (the rec-prems are not needed).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-13

pproof.scm

Adaption of inversion to simultaneous inductive definitions.
Minor polishing in elim-intern

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-12

axiom.scm

imp-formulas-to-uninst-elim-formulas-etc simplified: we can assume
that the arg-lists of the premises are partial variables new wrt 
(map idpredconst-to-free idpcs)

pproof.scm

Further correction of simelim-intern.  From the generalized
variables in the elim-axiom finally used, the ones that were newly
created for the original arguments (of the premises of the
imp-formulas) have to be instantiated by these arguments.

elim-intern and elim removed, and simelim-intern and simelim renamed
into elim-intern and elim


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-12

proof.scm

formula-to-efq-proof added.
Cleaned (comments should not be indented)

pproof.scm

inversion now produces the efq-proofs automatically

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-11

pproof.scm

simelim-intern corrected.

inversion (and hyp-info-to-formula as an auxiliary) added.  Intention:
In (inversion x), x is one of the following:
- A number or string identifying a hypothesis I(rs) form the context.
- The name of a theorem or global assumption stating I(rs)
- A closed proof of I(rs)
- A formula I(rs) with free vars from the context, generating a new goal.
Here I is an inductively defined predicate, with clauses K1 ... Kn
One uses the elim-aconst for I(xs) -> xs=rs -> goal, with ? ... ?
for the clauses, rs for xs and proofs for rs=rs, to obtain the goal.
Then many of the generated goals for the clauses will contain false
premises, coming from substituted equations xs=rs.


id.scm

Proof of "allnc n^.Even n^ -> ex m n^ =m+m" rewritten.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-10

pproof.scm

simelim-intern corrected and error messages improved

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-10

pproof.scm

elim expects a non-simultaneous inducticely defined predicate in the
premise.  Error message provided: Use simelim instead.

simelim added for simultaneous inductive definitions.

axiom.scm

All clauses should use partial generalized variables.  Hence
clause-etc-to-strengthened-clause should be changed accordingly, as
below.  However, this will affect proofs involving inductive
definitions (Monika Seisenberger's thesis, work of Klaus Thiel,
Freiric Barral, Stefan Schimanski and Dominik Schlenker), but only
in a minor way (assume needs to be done with partial variables).
Postponed.

var.scm

var-to-new-partial-var added.  It creates a new partial variable with
the same name and type as the given one.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-10-03

typ.scm

For cleaner code, we use explicit access functions for the
components of a typed-constr-name.

Error messages improved; no display functions in myerror.

var.scm

Cleaner treatment of degrees of totality:  Added t-deg-zero,
t-deg-one, t-deg-zero?, t-deg-one?, t-deg?

var?, mk-var adapted.  type-to-new-partial-var now takes an optional
var argument.

pconst.scm

add-program-constant and const-substitute adapted

psym.scm

STotal added as predicate constant.  predicate-equal? changed:
Equality of predicate constants now only means equality of names,
arities (obtained by carrying out tsubst in uninst-arity) and indices.

term.scm

match-aux adapted to new concept of equality for predicate constants.
Treatment of degrees of totality adapted, in term-to-t-deg-aux.

axiom.scm

In induction it is now possible to induct on stotal objects.  So
either all all-formulas are total, like all ps Q ps, or partial, like
all ps^ .STotal ps^ -> Q ps^.  Changed accordingly:
all-formulas-to-uninst-imp-formulas-and-tpinst
typed-constr-name-to-step-formula
all-formula-to-uninst-cases-imp-formula-and-tpinst
typed-constr-name-to-cases-step-formula

Was:
In induction and cases axioms, the argument variables in the step
formulas (corresponding to parameters in the type) can be partial.
Changed accordingly:
all-formula-to-uninst-cases-imp-formula-and-tpinst
typed-constr-name-to-cases-step-formula

proof.scm

constructor-debug-hook and check-and-display-proof-aux adapted

pproof.scm

assume now also checks that the t-degs of the quanitied and the user
variable are the same

ind-intern, simind-intern, cases-intern adapted to allow goal formulas
all ps^.STotal ps^ -> A

In inst-with-intern new-num-goal (the one that was instantiated) is
put on top of the goal stack, i.e., above (reverse new-num-goals)

Problem: by-assume-minimal-wrt-with does not show all newly
generated goals.  Cure: use display-new-goals

x-and-x-list-to-proof-and-new-num-goals-and-maxgoal
formula-and-elims-to-t-deg-ok? adapted to new concept of t-degs

grammar.scm

Token for predicate constant "STotal" added

warshall.save

Adapted

wftest.tac

Order of commands had to be adapted.  Also by-assume-minimal-wrt-with
used instead of minpr.

dickson.tac

Checked; is ok (only editorial changes).  However, termination of the
extracted program for the particular f,g provided seems to be a
problem.

lib/list.scm

Statement of LhConsn now with STotal pemise

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-08-25

; pproof.scm 

; inst-with corrected: new-num-goal needs to start from new-maxgoal
; instead of maxgoal.

; min-pr simplified, using display-new-goals

; In exc-formula-to-exc-intro-aconst and also in
; exc-formula-and-concl-to-exc-elim-aconst the comments emitted when
; providing the needed exc-intro theorem are suppressed.

; by-assume-minimal-wrt-with-intern provided, as a more usable form of
; min-pr.  It is similar to by-assume-with: If we know a classical
; existence exc x A(x), then we may assume that we have a minimal x
; (wrt a given measure) such that (1) A(x) and (2) for any smaller y,
; A(y) does not hold.

; exc-formula-and-measure-to-min-pr-aconst extended: it now works for
; unfolded exc-formula as well

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-08-17

pproof.scm

In use-with-intern, the warning converning nc-correctness has been
removed when the final proof will be correct (because on the path from
the bottom formula to the present goal there is a formula with no
content).  This is tested by checking that the final proof (obtained
after substituting the present goal by the new proof) still does not
have nc-violations.

examples/tait/dbrealrs.scm

Hat made partial (which it is).  Non-needed assumptions deleted:
TotalOmegaPart, HatSuperTotal

finalg-to-all-allpartial-nonc-aconst added.  Ax3P proved from
Ax3 using this and AxNStrict2.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-07-10

lib/list.scm

Theorem added: "ListAppendNil"

axiom.scm

Typo corrected in finalg-to-expartial-ex-aconst: Expartial -> ExPartial

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-07-09

lib/nat.scm:

++ as prefix operator for Succ removed.
n m k -> nat1 nat2 nat3.  
NatLess -> NatLt, NatLeq -> NatLe
Rewrite rule Pred(Succ nat1-nat2) -> nat1-nat2 added

lib/list.scm

Theorems added: "LhAppend", "ListRefAppendLt", "ListRefAppendGe"
Program constants added: "ListMap"
Theorems added: "LhMap", "MapAppend", "ListRefMap"
Program constants added: "Consn"

var.scm

var-to-string corrected.  (pp (pt "alpha_1")) now gives "alpha_1" and not
the previous "alpha1", which is parsed into a term of type alpha1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-06-04

ets.scm:

All-Allpartial and Expartial-Ex replaced by All-AllPartial and ExPartial-Ex 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-05-06

ets.scm:

In proof-to-extracted-term-aux the axioms all-allpartial and
expartial-ex were forgotten.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-04-19

pproof.scm

get-intern corrected: proof argument was not used.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-04-09

axiom.scm

add-theorem changed: Before saving a finished proof, it is checked
that it is nc-correct.  This uses nc-violations

pproof.scm

typo in use-intern corrected: formula -> used-formula

Correction of inst-with: check for nc inserted, as in use-with:

cvars-error in use-with and inst-with changed into a warning. 

var.scm

default-var? added

term.scm

nbe-extract now uses default-var? instead of numerated-var? (because
the default-var-names are used in normalized terms)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-03-20

Makefile

make clean now includes the directories bar and dc

lib/ref.tex

Typo corrected

pproof.scm

by-exnc-assume-with added (was forgotten).

term.scm

Correction of if-term-to-eta-expansion: recursive calls to
term-to-term-with-eta-expanded-if-terms inserted for alts and used
for test.  Inner call to if-term-to-eta-expansion removed.

Normalization of terms extended by replacing some Rec-terms by if-terms:
(Rec ...)param-args step-args rec-arg val-args is replaced by
[if rec-arg simplified-step-args]val-args.

In pattern? allnc and exnc added

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-03-20

lib/numbers.scm, lib/realsimp.scm

Minor editorial changes

axiom.scm

imp-formulas-to-uninst-elim-formulas-etc corrected: order of pvars
needs to follow the order of imp-formulas.  

Dependence on COMMENT-FLAG inserted

pproof.scm

Comments in interactive proofs are given only if COMMENT-FLAG is #t.
display-num-goal-aux now only does something if COMMENT-FLAG is #t.

prop.scm lnf.scm pconst.scm pp.scm proof.scm

Dependence on COMMENT-FLAG inserted 

list.scm

OLD-COMMENT-FLAG added, for restauring (in add-ids) the old flag value.
display-comment now only does something if COMMENT-FLAG is #t.

psym.scm

In add-ids OLD-COMMENT-FLAG used for restauring the old flag value.
Similarly in remove-idpc-name



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-03-07

pproof.scm

assert-intern corrected

psym.scm

string-and-arity-and-cterms-to-idpc-parse-function corrected:
arguments need to be coerced.

term.scm

Change of the test composed? (used for formula-to-string).  Problem:
We have Real(a) with of the present definition of composed?  Because
of coercions a in this sense *is* composed.

lib/numbers.scm and lib/realsimp.scm added to the repository.
Both are psrt of ~schwicht/wwwpublic/seminars/prosemss04/numbers.scm,v 1.23 
2004/11/02.

examples/arith/sqrttwo.scm and examples/arith/realsqrttwo.scm
added to the repository.  They are provided for Freek Wiedijk's
"stamp collection" of irrationality of sqrt(2) proof formalizations.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-03-03

pproof.scm

x-and-x-list-to-proof-and-new-num-goals-and-maxgoal extended to also
cover a leaf x formed with an AndConst-atom,

get-intern more efficiently implemented

by-assume-with-intern extended: it now works not only for
a hypothesis, but also for a theorem/global assumption/proof and for
an existential formula, which creates a new goal.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-02-25

psym.scm

add-ids changed.  The final add-token now has three cases:
idpredconst-name idpredconstscheme-name idpredconstscheme-name-wit
where wit stands for with inferable types.  idpredconst-to-string
adapted

grammar.scm

Treatment of inductively defined constants corrected and extended

id.scm

Adapted to new treatment of inductively defined constants

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-02-14

pprooof.scm

Change of simp-with-intern.  In case the kernel of the used formula
(or its normal form) is True or False, one does not `simplify'.

xs renamed into x-list (as in use-with), to be consistent with the
fact that x is separate.  Done in simp-intern and in
fla-and-sig-tvars-and-vars-and-goal-fla-to-fst-match-data

fla-and-sig-tvars-and-vars-and-goal-fla-to-fst-match-data adapted to
type matching.  In simp-intern sig-tvars-and-sig-vars introduced.

fla-and-sig-tvars-and-vars-and-goal-fla-to-use-data introduced.  Replaces
formula-and-sig-vars-and-goal-to-subst-and-xs-and-vars

Change of goal-subst, to prevent the final formula (proved by the
present proof) to be normalized (which can happen in simp-with).  In
the definition of goal-subst we make sure that the formula of proof is
not changed (i.e. normalized).  Therefore we do not use
make-proof-in-imp-intro-form etc, but rather its definition and take
the formula always from the given proof.

normalize-goal takes optional arguments.  If there are none, the goal
formula and all hypotheses are normalized.  Otherwise exactly those
among the hypotheses and the goal formula are normalized whose numbers
(or names, or just #t for the goal formula) are listed as additional
arguments.

In simp-intern no error is raised in case the goal does not simplify.

term.scm

match-aux corrected in case predicate with predconst: the types there
may have to be substituted.

lnf.scm

proceed adapted

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-02-07

typ.scm

In type-match-aux, id-vars renamed into sig-tvars and subst renamed
into tsubst.

term.scm

First order matching extended to also cover terms with type variables
in their types.  Changed: match  match-list  match-aux  first-match

pconst.scm

Adapted to different type of match.  Changed:
nbe-pconst-and-tsubst-and-rules-to-object

formula.scm

Obsolete formula-match deleted.  match works for terms and formulas.

mpc.scm

formula-match replaced by match

pproof.scm

Adapted to different type pf match.  Changed:
formula-and-sig-vars-and-goal-to-subst-and-xs-and-vars

lnf.scm

formula renamed into goal-formula

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-01-31

pconst.scm

In an extracted term it may happen that the alternatives in if-terms
would be not eta-expanded, if nt was applied to the extracted term.
Example: Pred: "all n ex b,m.(b -> m=Zero)&((b -> F) -> n=Succ m)"
has [n0][if n0 (True@Zero) ([n1]False@n1)] as normal extracted term.
But the rhs of a rule should have eta expanded if terms, because
this is expected by nbe-normalize-term-without-eta, which is where
these rules are applied.  Therefore in add-computation-rule and
add-rewrite-rule we enforce that each rhs has eta expanded if terms.
Correspondingly, in display-program-constants term-to-eta-nf is
applied to every rhs.

axiom.scm

In total-aconst the free object variables had to be bound.  Minor
corrections (name -> aconst-name) in the definitions of some other
assumption constants.

pp.scm

Typo in error message corrected

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-01-08

pproof.scm

Correction in
formula-and-sig-vars-and-goal-formula-to-first-match-data In match-res
the kernel of a used atomic formula is considered further.  Typo in
simp-with-intern corrected (simp-with-nkernel-aux replaced by
simp-with-kernel-aux)

term.scm

Correction in first-match: test in if-terms not accomodated

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2005-01-07

pp.scm

In token-tree-to-pp-tree , case postfix-op, (string-append op ")")
replaced by (string-append ")" op)

term.scm

first-match added

pproof.scm

simp-with added.  Generally: simp made more applicable:  Here is the text
In the following definition of simp-with x is one of the following.
- A number or string identifying a hypothesis form the context.
- The name of a theorem or global assumption, but not one whose final
  conclusion is a predicate variable.
- A closed proof.
- A formula with free variables from the context, generating a new goal.
Moreover x-list is a list consisting of
- a number or string identifying a hypothesis form the context,
- the name of a theorem or global assumption,
- a closed proof,
- the string "?" (value of DEFAULT-GOAL-NAME), generating a new goal,
- a symbol left or right,
- a term, whose free variables are added to the context,
- a type, which is substituted for the 1st tvar,
- a comprehension term, which is substituted for the 1st pvar.
This generates a used formula, which is to be an atom, a negated
atom or (Equal lhs rhs).  If it as a (negated) atom, check whether
the kernel or its normal form is present in the goal.  If so,
replace it by True (False).  If it is an equality (lhs = rhs) or
(Equal lhs rhs) with lhs or its normal form present in the goal,
replace lhs by rhs.  In case "<-" exchange lhs by rhs.

To avoid duplication of code we introduce auxiliary functions, to be
used in use-with-intern, use-intern, simp-intern and inst-with-intern:

context-and-cvars-and-formula-to-new-goal hyp-info-to-leaf
x-and-x-list-to-proof-and-new-num-goals-and-maxgoal

compat-at eq-compat-at added.

formula.scm

imp-all-allnc-form-to-final-conclusion added.

boole.scm

Rewrite rules for AndConst extended to also cover partial terms.
Infix notation `and' (left associative) for AndConst added.

lib/list.scm

Program constant "ListRef" added (partial!).
Infix notation `thof' for ListRef added.

examples/dijkstra/dijkstra.tac examples/dijkstra/pick.tac
examples/dijkstra/wf.tac

simpeq replaced by simp

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2004-12-31

pconst.scm

=-at and e-at extended to also reduce constructors with more that one
argument.  This requires AndConst, hence the algebra boole.  Therefore
both are moved from here into boole.scm.

boole.scm

=-at and e-at extended to also reduce constructors with more that one
argument.  This requires AndConst, hence the algebra boole.  Therefore
both are moved here from pconst.scm.

pproof.scm

split extended to also work for goals formed with AndConst.  This
requires atoms-to-and-atom-proof : 
all boole1,boole2.boole1 -> boole2 -> AndConst boole1 boole2

init.scm

In error-object-to-string the test type-form? has been replaced by the
full test type?, and var-form? by var?.  This is necessary to avoid
looping in certain error situations.

modules/atr.scm

AndConst and its rules commented out; they have been moved into boole.scm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Done 2004-11-13

gen-app.scm list.scm typ.scm var.scm pconst.scm psym.scm term.scm ets.scm
pproof.scm

For every global variable (e.g., MAXTVARINDEX) its initial value
is assigned to an associated global variable (e.g., INITIAL-MAXTVARINDEX)
to be used for reset.

formula.scm

formula-check-to-string, check-and-display-formula (cdf) and
cterm-check-to-string added

pp.scm

done: pp for types 

Done 2004-11-11

pproof.scm

In auto-intern each time in the search-loop (display-comment) is done.
This gives the user an indication how auto proceeds.  Error messages
improved in cases where an interactive command expects a formula or a
term.

Done 2004-11-08

ets.scm

(mr-invariant? formula) added.  In proof-to-soundness-proof-aux in
case of an assumption constant it is now first checked whether the
formula is mr-invariant.  If so, then the original assumption constant
is used again.

Done 2004-11-02

lnf.scm, axiom.scm, proof.scm, temp.scm, orevkov.tac, quotrem-ex.tac,
warshall.tac

num-goals-and-proof -> pproof-state, with maxgoal as an additional entry

prop.scm, pproof.scm

Changed: num-goals-and-proof -> pproof-state, now with three entries:
num-goals, proof, maxgoal.  The local maxgoal is needed for undo.  The
interactice commads (tactics) are split into an internal part, which
only changes the pproof-state, and an external version, which in
addition displays some comments.  In use-with, using a hypothesis with
a comprehension term is explicitely allowed: it does not make sense in
our predicative (i.e., parametric) view of predicate variables.

Done 04-09-20

term.scm

Better error messages in make-term-in-app-form

In term-in-const-form-to-string for a constscheme with 2 or more
arguments we put parentheses around those types whose string contains
#\space.  Reason: otherwise we cannot parse such constschemes.

We now modify term-to-string and pp to print (cID ..)([x]kernel)arg as
[let x arg kernel] 

New version of term-to-expr.  Goals: (1) Usual syntax for arithmetical
expressions (2) For readablibity, we use (let ((x arg)) kernel) for
(((lambda (x) x) (lambda (x) kernel)) arg) and expr for ((lambda (x)
x) expr).  Moreover we define expr-to-free and
remove-vacuous-beta-redex, for otherwise (term-to-expr QR-neterm)
would have a subterm ((lambda (n2) (cons 0 0)) i1) where cond
expressions are generated.

pconst.scm

Allow for external code in pconsts.  We may keep the distinction
pconst - fixed-rule and allow in a pconst - before it tries
computation and rewrite rules - the use of an external function
working with objects.  It tests the arguments (e.g., whether they are
numerals), and if yes immediately returns the result.  Otherwise the
rules are tried next.  This external function should be optional, and
it is given explicitely by its code.

New error message added to add-computation-rule and add-rewrite-rule
requiring that the type variables used are the uninstantiated ones
from the pconst.

pp.scm

formula-token-tree-to-pp-tree changed in case imp-op and-op tensor-op
to avoid the unneccessary parentheses in T -> (all x.T & F)

psym.scm

pvar-name-to-arity corrected

typ.scm

type-leq?  increasing-types-to-coercion etc should be independent of
int rat real

type-leq? should be transitive, but is not for the present one.
Counterexample:
(type-leq? pos int) ;#t
(type-leq? int (py "ytriple (ytriple pos unit pos) unit pos")) ;#t
(type-leq? pos (py "ytriple (ytriple pos unit pos) unit pos")) ;#f

Cure: View pos, int, rat and real as algebras, with constructors
pos: One SZero SOne 
int: IntPos IntZero IntNeg
rat: RatConstr (written # infix) and Destructors RatN RatD
real: RealConstr and Destructors RealSeq RealMod

Advantages: cleaner, also better display of types.  type-leq? then
clearly is transitive.  (increasing-types-to-coercion type1 type2)
uses a global variable INCREASING-ALGEBRAS-TO-COERCION-ALIST initially
set to '().

Given type1 and type2 and tvar.  Want: interval, that is
(type-leq-lb type1 type2 tvar) and (type-leq-ub type1 type2 tvar)
such that the types in between are exactly those with (type-subst
type1 tvar type) <= (type-subst type2 tvar type)

type-leq? now accounts for monotonicity of tensor and ytriple in its
arguments.  It should be extended to other parametrized algebras
monotone in their arguments.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-05-04

tensor.scm

term-in-tensor-form? term-in-tensor-form-to-fst term-in-tensor-form-to-snd
added

typ.scm

Correction of increasing-types-to-coercion in tensor case

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-04-25

ets.scm

Correction of ex-formula-and-concl-to-ex-elim-mr-proof-aux in the case
where content is everywhere: mk-kernel should not use pair-var

In proof-to-extracted-term-aux assign the identity term to compat
axioms and global assumptions.  Because of the nc quantifiers the
previous type-to-canonical-compat-term is not needed (and in fact
can be wrong).

Correction of eq-compat-aconst-to-mr-eq-compat-proof :
nc-quantifiers need to be used.  Moreover, the procedure is
generalized to work with eq-compat-rev, compat, compat-rev as well

Corresponding change in proof-to-soundness-proof-aux

In all-formula-to-mr-cases-proof-aux replace (append free real-vars)
by (formula-to-free mr-all-formula)

pproof.scm

Correction of casedist : dec-cases-proof now proves - as it should - 
(formula-to-string (pf "all boole.(boole -> (Pvar boole)^True) -> 
                              ((boole -> F) -> (Pvar boole)^False) -> 
                              (Pvar boole)^boole"))

typ.scm

make-inhabited changed: it now only has a side effect and does not
return a term.  type-to-canonical-inhabitant adapted.

term.scm

Pretty printing of terms provided: (pp term).

In if-terms the type is to be determined as the lub of the types of
the alts (notice: parameter types may be present).

Subtype relation generated from pos < int < rat < real introduced.
Need types-to-coercion, increasing-types-to-coercion, types-lub,
types-lub-aux, types-glb-aux.

check-and-display-term provided: (cdt term)

axiom.scm

changed add-computation-rule: optional arity of the added program
constant provided


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-03-29
grammar.scm

For to allow
(type-to-string (py "ytriple pos unit pos@@ytriple pos unit pos"))
(which is the display string) instead of 
(type-to-string (py "(ytriple pos unit pos)@@(ytriple pos unit pos)"))
another production had to be added (as for terms):

        (prodtype prod-typeop apptype) : ($2 $1 $3)

axiom.scm

remove-theorem and remove-global-assumption extended to also remove
added program constants.

term.scm

Corrected term-to-eta-nf, for pair terms.  Correction of
constant-alts? and constants-alts-to-const-term.

proof.scm

proof-of-stab-at-aux, proof-of-efq-at-aux, proof-of-stab-log-at-aux,
proof-of-efq-log-at-aux corrected in case (atom predicate ex exnc),
when there are free parameters.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-02-29
typ.scm

We want to coerce a sequence of naturals (or integers) into a sequence
of rationals.  Therefore increasing-types-to-coercion has been
extended accordingly.  types-lub  extended to reals.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-02-17
ets.scm

proof-to-soundness-proof-aux corrected (typo in allnc case)
all-formulas-to-mr-ind-proof-aux corrected: (1) mr-ind-aconst now applied
to free variables read off from mr-inst-formula.  In the previous
(append free real-vars) the order might be incorrect.  (2) var-lists
corrected in case there are no step formulas.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-01-29

list.scm

Cleanup concerning comments.  

comment yields complete one-line comments composed from multiple
strings, beginning with COMMENT-STRING and ending with a newline
command.  Complete comments can be switched off using COMMENT-FLAG.

display-comment is used for building complex displays with
COMMENT-STRING inserted in front, e.g. to display goals or proofs.

pproof.scm

(comment "Proof finished.")  replaced by
(begin (display-comment "Proof finished.") (newline))

psym.scm

In add-ids COMMENT-FLAG set to #f, to suppress unnecessary comments.
remove-idpc-name added.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-01-19

typ.scm

types-lub types-to-coercion and increasing-types-to-coercion added,
to enable overloading and coercion when working with rationals.

term.scm

make-term-in-app-form changed, to enable overloading and coercion when
working with rationals.

The possibility to change display of say n#0 to n makes is necessary
to adapt the notion of being composed, used for diplay of predicate
formulas.  uncomposed? introduced, and composed? defined from it.
Reverted again 04-01-16.

formula.scm

make-predicate-formula changed, to enable overloading and coercion when
working with rationals.

In predicate-form-to-string, for x+y===y+x instead of (x+y)===(y+x):
Composed arguments get no parentheses in case of an infix predconst.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 04-01-08

mlcf.tex
Correction concerning Huet projections inserted.

ref.tex
remove-computation-rule replaced by remove-computation-rules-for
remove-rewrite-rule replaced by remove-rewrite-rules-for

grammar.scm
To enable coercions for equality, the predefined token "=" now forms
the =-term with the lub of the two argument types

minlog/lib/tensor.scm
Initial commit.  This is an attempt to build integers and rationals by
means of a parametrized free algebra tensor.

axiom.scm
new-global-assumption-name added to axiom.scm.  Takes a string, and
tests all indices i whether string*i-string already is a name of a
global assumption.

pproof.scm
In search and search-ex test included, whether theorems and global
assumptions have positive multiplicities.

In intro-search an atomic goal is normalized.

auto added: A new front end to the search engine, which does iterated
search automatically.  Its arguments (possibly empty) consist of a
multiplicity and theorem or global assumption names, each with its
individual multiplicity (a positive integer).  From these and the
local context clauses are determined, and with these intro-search is
called.  If it returns #f, the automated search terminates and the
unsolved goal is displayed.  If it returns a true value, the global
variables NUM-GOALS-AND-PROOF and NUM-GOALS-AND-PROOF-HISTORY are
updated accordingly and a new search is started, with the same
multiplicity and given leaves.

term.scm
Correction of pattern-unify-rigid-rigid.  Terms in pair form and terms
in component form were forgotten

huet-unifiers-match corrected: not all projections are correct, but
only those where the final value type of xi is the (ground) type of
the rigid term.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-12-08
pproof.scm

In elim-search we now use
		(new-leaf (proof-substitute-and-beta0-nf leaf phi))
instead of
 		(new-leaf (proof-substitute leaf phi))
Reason: proof-substitute causes a renaming of avars, which does not
fit to the rest of the proof construction.

In search
 	 (context (goal-to-context goal))
instead of
 	 (context (reverse (goal-to-context goal)))
Reason: In (search m '(name1 m1) '(name2 m2) ...) in case name1 name2 ...
are numbers they ought to refer to the hypotheses with the same numbers

proof.scm 

Change of proof-to-expr: for avars use avar-to-string.  This makes the
indices of avars in the proof expressions the same as the numbers of
hypothesis in the proof display.  Moreover, it avoids occurrence of
unnamed assumption variables

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-11-14: 
pconst.scm

In nbe-pconst-and-tsubst-and-rules-to-object in case of a rewrite rule
term-to-eta-nf applied to the extracted-terms of the present
arguments, because the latter are in long normal form:
(extracted-terms (map term-to-eta-nf (map nbe-extract reified-objs)))

Added: (remove-rewrite-rules-for lhs): removes all rewrite rules
unifying with lhs.  (Was forgotten)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Not yet Done 03-10-22: examples/tutorial.scm

Prepared for inclusion in the distribution (load -> mload etc)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-09-11: modules/type-inf.scm

Cleaned up.

tvartest.scm

Deleted.  The examples for add-algs transferred to id.scm

id.scm

Cleaned up; examples for add-algs included (from tvartest.scm)

ref.tex

Comparison with Coq and Isabelle added

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-09-10: ets.scm

formula-to-et-type corrected in case of idpredconsts.  Added
idpredconst-to-et-type

number-and-idpredconst-to-et-constr corrected

imp-formulas-to-et-rec-const corrected: in simplified-relevant-clauses
the test (zero? (pvar-to-h-deg pred)) is used

grammar.scm

idpredconst-name-and-types-and-cterms-to-idpredconst used instead of
make-idpredconst 
Reason: involves some tests.

psym.scm

Error messages in idpredconst-name-and-types-and-cterms-to-idpredconst
made clearer.

add-ids corrected and simplified, concerning the algebra of realizers.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-09-03: id.scm
allnc-all-quantifiers admitted in inductive definitions

formula.scm

atomic formula -> prime formula
typo corrected in exid-form-to-kernel

Basic function for exi added (inductively defined existential
quantifier where the kernel does not have computational content)

formula-to-beta-nf added

pproof.scm

In select use huet-unifiers in addition to pattern-unify.  It yields
a list of all unifiers found for the given MATCH-TREE-BOUND.

Ext -> Eq-Ext

ets.scm

INITIAL-PVAR-TO-TVAR-ALIST added (for reset)
formula-to-et-type corrected in case (idpredconst-form? pred)
imp-formulas-to-et-rec-const adapted to allnc-all-quantifiers in ind defs
number-and-idpredconst-to-et-constr corrected

proof.scm

Error message for cdp made clearer: `in imp elim formulas do not fit'
both A -> B and the non-fitting A' are displayed.

axiom.scm

clause-etc-to-strengthened-clause clause pvars uninst-idpcs)
adapted to allnc-all-quantifiers in ind defs

The procedure clause-and-cterm-pvars-and-idpc-pvars-to-strengthened-clause
has been adapted, but also deleted from axiom.scm : not needed

psym.scm

add-ids adapted to allnc-all-quantifiers in ind defs
idpredconst-to-string extended by exi

boole.scm

Line added:
(add-token "exi" 'quantor (lambda (v k) (apply mk-exi (append v (list k)))))


term.scm:  

Corrections in pattern-unify-xi and pattern-unify-rigid-rigid
concerning nc-quantifiers and predicate constants

Huets unification algorithm added

typ.scm

type-to-canonical-term and type-to-final-groundtypes added
(needed for Huets unification algorithm)

nat.scm

Program constants <=, Pred, - added (from nat2.scm)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-08-23: term.scm

Description of substitution clarified.  It is merely assumed that
subst only affects those vars whose type is not changed by tsubst.

Some procedures added (useful for debugging):
term-in-rec-normal-form?
term-to-length
term-to-consts-with-repetitions
term-to-consts
term-in-intro-form-to-final-kernels
term-in-elim-form-to-final-op-and-args
term-in-app-form-to-final-op-and-args
term-to-parts-of-level-one
(term-to-subterms term . opt-level)
term-to-depth

formula.scm

For display, p-substitution-to-string added.  Description of
substitution clarified.

axiom.scm

aconst-to-inst-formula simplified.  Description of aconsts clarified.

proof.scm

Description of substitution clarified.  
Some procedures added (useful for debugging):

proof-in-intro-form-to-kernel-and-vars
proof-in-intro-form-to-final-kernels
proof-in-elim-form-to-final-op-and-args
proof-to-parts-of-level-one
(proof-to-parts proof . opt-level)
proof-to-depth
proof-to-one-step-beta-reduct
proof-in-beta-normal-form?
proof-to-beta-nf
proof-to-beta-pi-eta-nf
bpe-np
proof-to-length

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-08-21: axiom.scm 

aconst-substitute-aux corrected: there was a clash between variables
free in psubst and variables free in the pinst of the aconst.  Example:
Induction all n A(f,n,X) has form all f. A(f,0 X) -> ...
After psubst X -> {|B(f)} this f gets catched.

proof.scm

Moreover, aconst-substitute-aux was deleted, or better transferred
into proof-substitute-aux where it is needed (and essentially only
there).  Its uses in proof-of-stab-at-aux etc replaced by uses of
proof-substitute-aux.

dickson.tac In the proof check procedures, allnc added.
Moved into minlog/examples/classical/debug.scm
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 03-08-19: ets.scm In eq-compat-aconst-to-mr-eq-compat-proof
(pinst (list-transform-positive tpinst pvar-form?))
replaced by
(pinst (list-transform-positive tpinst
		  (lambda (x) (pvar-form? (car x)))))

and also (new-cterm (make-cterm vars mr-fla)) replaced by
(vars (cterm-to-vars cterm))
(var (if (pair? vars)
         (car vars) 
         (myerror
	  "eq-compat-aconst-to-mr-eq-compat-proof: var expected in cterm"
          (cterm-to-string cterm))))
(new-cterm (make-cterm var mr-fla))

proof-to-soundness-proof-aux corrected in case of efq global assumptions.
To this end, efq-ga-to-mr-efq-ga-proof addad.

Discarded code eliminated.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-10-30
ets.scm
In formula-to-et-type-aux
all-form-to-kernel replaced by allnc-form-to-kernel
ex-form-to-kernel replaced by exnc-form-to-kernel

formula-of-nulltype? added
(nulltype? (formula-to-et-type-aux formula pvar-to-tvar)) replaced by
(formula-of-nulltype? formula)

proof.scm pproof.scm atr.scm
(nulltype? (formula-to-et-type formula)) replaced by
(formula-of-nulltype? formula)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-10-23
typ.scm
TYPES-WITH-CANONICAL-INHABITANTS new global variable
make-inhabited implemented.
type-to-canonical-inhabitant adapted; it now works for types
involving type variables as well

ref.tex
In inst-with explanation of x-list corrected

pproof.scm
In inst-with explanation of x-list corrected
In use-with and inst-with error message inserted:
expected order of arguments is types - cterms - rest

proof.scm
In proof-of-stab-at-aux proof-of-stab-log-at-aux
proof-of-efq-at-aux proof-of-efq-log-at-aux
now allnc-form-to-vars used

term.scm
arrow-types-to-rec-const replaced by type-info-to-rec-const
separator-string now adds space between Q^ and a numeric character,
to distinguish an argument from an index

pconst.scm
pconsts of arity zero now normalize as well

psym.scm
enforce nullary constructors in generated algebras for IDs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-09-30
list.scm

(index-of-first-occurrence x l) added

pconst.scm

constr-name-to-constr adapted to constructor with name "Intro"

imp-formulas-to-rec-const adapted to new
imp-formulas-to-uninst-elim-formulas-etc

ex-formula-to-ex-intro-const simplifies, without set-cdr!

number-and-idpredconst-to-intro-const added

rec-at adapted to the more complex phenomena concerning
free parameters in terms in Elim and Intro axioms.

const-substitute adapted to constructor with name "Intro"

psym.scm

idpredconst-name-and-types-and-cterms-to-idpredconst added

idpredconst-to-pinst simplified

idpredconst-name-to-nbe-alg-name added

idpredconst-name-to-param-pvars added

Change add-ids: use e.g. nbeAcc as alg-name for nbe.  Also, for clause
Zero we use ZeroAcc and OneAcc as constructor names for Acc.  In
addition, there is an optional alg-name (default: the old one with
prefix et) indicating computational content of the idpredconst, for
term extraction.  If it is present, then all clauses with this
idpredconst as conclusion generate constructors; default-name
e.g. EtZeroAcc, EtOneAcc.

number-to-alphabetic-string and alphabetic-string-to-number added
constructor-name-to-i-and-idpredconst-name added
formula-to-nbe-tvars added

formula.scm

nbe-formula-to-type adapted to nbe for idpcs

grammar.scm

When parsing an idpredconst, it should be checked whether the types
and the cterms are correct.  Therefore instead of the constructor
make-idpredconst use idpredconst-name-and-types-and-cterms-to-idpredconst
in grammar

axiom.scm

imp-formulas-to-uninst-elim-formulas-etc changed: allnc xs^ in front
removed.  Reason: nbe needs to ignore these in the rec-at types.  In
aconst-to-formula allnc xs^ is added anyway.

clause-etc-to-strengthened-clause added

number-and-idpredconst-to-intro-aconst changed: no more pinst for idpc-pvars

proof.scm

proof-and-genavar-var-alist-to-pterm and
elim-npterm-and-var-genavar-alist-to-proof adapted

Correction of proof-to-eta-nf in all-intro and allnc-intro cases: the
abstracted variable of the proof term (not the generalized variable of
the proved formula) must be compared.

imp-formulas-to-rec-const adapted t- nbe for ids

pproof.scm

intro slightly simplified
elim adapted and thereby simplified

ets.scm

imp-formulas-to-et-rec-const adapted to new
imp-formulas-to-uninst-elim-formulas-etc


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-30
axiom.scm

aconst-substitute-aux adapted to intro-aconsts with repro-data i idpredconst
(plan: rename repro-formulas into repro-data)

ets.scm

imp-formulas-to-et-rec-const changed: Rec now with arrow-types instead
of imp-formulas.  Reason: parameters are not present in ets any more

pproof.scm

In use-with another proof-to-cvars-aux replaced by proof-to-potential-cvars
intro formulated with use instead of use-with
compat-rev-at eq-compat-rev-at adapted to Eq-Compat-Rev-At with allnc

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-29
typ.scm

(nulltype? x) introduced, to replace (equal? (make-tconst "nulltype") x)

ets.scm

cases-aconst-to-if-term adapted to allnc in parameters of cases-aconst
proof-to-extracted-term-aux adapted to allnc in parameters of theorems
proof-to-soundness-proof-aux adapted to allnc case
real-and-formula-to-mr-formula-aux adapted to allnc case


pproof.scm

use-with corrected: When interactively developing a partial proof, a
goal v x_1...x_n is replaced by another partial proof, whose context
may contain (1) items from x_1...x_n (i.e. the context of the goal
with v removed), (2) object variables newly introduced at this moment
and (3) new goal variables.

goal-to-admitted-cvars replaced by goal-to-ncvars

context-and-cvars-and-formula-to-formula corrected


proof.scm

proof-to-cvars-aux corrected
proof-to-potential-cvars added, for use-with

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-27
ets.scm

all-formulas-to-et-rec-const changed: Rec now with arrow-types instead
of all-formulas.  Reason: parameters are not present in ets any more

number-and-idpredconst-to-et-constr added

pconst.scm

imp-formulas-to-rec-const added, for normalization.  It solves

imp-formulas-to-rec-const       all-formulas-to-rec-const
----------------------------  = ----------------------------
imp-formulas-to-et-rec-const    all-formulas-to-et-rec-const

number-and-idpredconst-to-intro-const added, for normalization.

formula.scm

allnc and exnc added
nbe-formula-to-type adapted to param-cterms in idpredconsts

grammar.scm

     ("allnc" quantor . (lambda (v k) (apply mk-allnc (append v (list k)))))
     ("exnc" quantor . (lambda (v k) (apply mk-exnc (append v (list k)))))
added

axiom.scm

aconst-to-string adapted to intro-aconsts
aconst-to-formula formulated with allnc (i.e., universally generalized
variables in an assumption constant generally have no computational
content).

proof.scm

allnc and exnc added.  proof-to-cvars added
Format of proofs changed: If the optional context is present,
then also the list of computational variables

pproof.scm

computational variables added to proofs

display-num-goal-aux puts braces around non-computational variables

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-12
psym.scm (to be renamed into pred.scm)

Inductively defined predicate constants added, from id.scm

Generalities for all kinds of predicated added:
predicate-to-arity predicate-to-cterm predicate-equal?

pconst.scm

rec-const-to-param-types adapted to idpredconsts

typ.scm

RESERVED-NAMES extended by "or" "OrID" "ExID" "EqID".  is-used? adapted

axiom.scm

clause-and-cterm-pvars-and-idpc-pvars-to-strengthened-clause
idpredconst-to-intro-aconst
imp-formulas-to-uninst-elim-formulas-etc
imp-formulas-to-uninst-elim-formula-etc
imp-formulas-to-elim-aconst
added

pproof.scm

(intro i . terms) (elim . opt-terms) added

grammar.scm

idpredconst-name-and-types-and-cterms-to-idpredconst replaced by
make-idpredconst

formula.scm

make-predicate-formula
predicate-form-to-predicate
predicate-form-to-string added

imp-form-to-premises computes the first (car x) premises of a formula.

imp-form-to-final-conclusion computes the final conclusion (conclusion
after removing the first (car x) premises) of a formula. 

all-form-to-vars computes the first (car x) vars of a formula.
all-form-to-final-kernel computes the final kernel (kernel
after removing the first (car x) vars) of a formula. 

or and exid added via inductively defined predicates

formula-to-pvars nbe-formula-to-type formula-substitute-aux 
pvar-cterm-equal? adapted

For parsing and display tokens "or "eqid" "exid" and idpredconst-display
"EqID" added.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-09
id.scm

imp-formulas-to-et-rec-const implemented
Interface for IDS cleaned up.
formula-to-et-type-aux corrected for idpredconsts

formula-to-et-type-aux replaced by id-formula-to-et-type-aux
proof-to-extracted-term-aux replaced by id-proof-to-extracted-term-aux
Idea: In a context with inductive definitions, the all quantifier
has no computational content.  Then ind cannot be used any more,
but must be replaced by elim with respect to an inductively defined
predicate e.g. Nat.  Also all quantifiers with computational content
must be replaced by relativizations to Nat.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-06
id.scm

Provided as preparation for normalization and program extraction:

allimp-formulas-to-uninst-imp-formulas-and-tpinst
allimp-formulas-to-uninst-imp-formula-and-tpinst
allimp-formulas-to-elim-aconst

Format of idpredconsts changed to ('idpredconst name types cterms)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-05
proof.scm

proof-to-eta-nf corrected in case 

          all n^ P n^  n
          --------------
                P n
             ---------
             all n P n

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-02

id.scm

Extended to inductive definitions without computational content

grammar.scm

Renamed: pvar -> pred
         pvar-infix -> pred-infix
         predconst -> pred
         predconst-infix -> pred-infix
and similarly for idpredconst.   This leads to some simplifications
in the rules for atomic-formula

formula.scm lnf.tac quant.tac hofmann.tac

predconst-infix -> pred-infix

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-08-01
id.scm

add-ids changed to also allow inductively defined predicate constants
without computational content.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-07-31
pconst.scm

ex-formula-and-concl-to-ex-elim-const reimplemented in a cleaner form
(using two simultaneously defined auxiliary functions, instead of
(set-car! (cdr const) obj))

axiom.scm

In aconst-substitute-aux the final composed-pinst is reduced

ets.scm

Correction of proof-to-extracted-term-aux in cases Stab-Log and Efq-Log

Change of formula-to-et-type-aux : excl and exca initiate a recursive call
on the unfolded formula.

formula.scm

Change of formula-substitute-aux : excl initiates a recursive call
on the unfolded formula provided falsity-log-pvar appears in the domain

proof.scm

proof-to-global-assumptions-with-repetitions and also
proof-to-global-assumptions added.  They completely collect all
used global assumptions, entering recursively into proofs.

atr.scm

Removed the tests on Stab-Log and Efq-Log in min-excl-proof?

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-07-29
pproof.scm

More general use-with and inst-with: it now substitutes also for type
variables and predicate variables.

ets.scm

In proof-to-extracted-term-aux the global assumptions Stab-Log and
Efq-Log are first replaced by their proofs, whenever possible.

In min-excl-proof? formula=? used for comparison with falsity-log

atr.scm

Extraction of a program from a classical proof presupposes
(1) the global assumptions Stab-Log, Efq-Log are not used
(2) there are no predicates exept bot and atom
(3) there are no (constructive) existential quantifiers
(4) there is no conjunction &

Ad (1).  In proof-to-extracted-term-aux Stab-Log and Efq-Log are
removed before program extraction is done.  Ad (2)-(4).  It is the
responsibility of the user to only use such proofs.  Error messages
are provided.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-07-24
atr.scm
atr-min-excl-proof-to-structured-extracted-term admits more than one 
existential quantifier

Test min-excl-proof? provided

term.scm
term-to-eta-nf extended to if-terms as well (recall: For a full
normalization of terms, including permutative conversions, we defined
a preprocessing step that eta expands the alternatives of all
if-terms.  The result contains if-terms with ground type alternatives
only.)

Alternative to nbe, if no rewrite rules are applicable.  Uses
term-to-one-step-beta-reduct
term-in-beta-normal-form?
term-to-beta-nf
term-to-beta-pi-eta-nf
bpe-nt

proof.scm
proof-to-aconsts-with-repetitions and proof-to-aconsts provided.
Similarly proof-to-aconsts-without-rules-aux and proof-to-aconsts-without-rules

dickson.tac
Major cleanup.  Contains Berger's variant of nbe-reify, and
preliminary test functions for debugging, e.g.
term-in-rec-normal-form?
term-to-length
term-to-consts-with-repetitions
term-to-consts

term-in-intro-form-to-final-kernels
term-in-elim-form-to-final-op-and-args
term-in-app-form-to-final-op-and-args
term-to-parts-of-level-one
term-to-subterms
term-to-depth

proof-in-intro-form-to-kernel-and-vars
proof-in-intro-form-to-final-kernels
proof-in-elim-form-to-final-op-and-args
proof-to-parts-of-level-one
proof-to-parts
proof-to-depth
proof-to-one-step-beta-reduct
proof-in-beta-normal-form? 
proof-to-beta-nf 
proof-to-beta-pi-eta-nf
bpe-np
proof-to-length

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-07-19
term.scm
Term families reimplemented, with constructor and destructors

pconst.scm
Term families reimplemented, with constructor and destructors

Change of rec-at in reproduction case: build term family from 
application term starting with rec-term

Change of rec-at and alg-name-etc-to-rec-const: additional arguments
uninst-recop-type, inst-recop-type for efficiency reasons

Changed all occurrences of rec-at and alg-name-etc-to-rec-const in
type-info-to-rec-consts all-formulas-to-rec-const const-substitute

[ex-formula-and-concl-to-ex-elim-const cleaned up (with simultaneous letrec))]
Does not yet work

ets.scm
Changed all occurrences of rec-at and alg-name-etc-to-rec-const in
all-formulas-to-et-rec-const
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-06-17
axiom.scm

In all-formula-to-uninst-cases-imp-formula-and-tpinst typo corrected
all-formula -> uninst-all-formula

ets.scm

all-formula-to-mr-cases-proof-aux corrected (and simplified):
all-formula-to-cases-aconst used to construct cases-step-formulas

proof-to-soundness-proof-aux corrected: the given proof is only
reproduced in case on an axiom asserting a formula without
computational content.

all-formulas-to-mr-ind-proof-aux corrected: prem-vars-lists 
(i.e. list of lists of vec{x}'s) must be formed using the number of
argument types of the y-variables

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-06-12
term.scm

term-in-const-form-to-string adapted to type-infos

pconst.scm

arrow-types-or-repro-formulas replaced by type-info-or-repro-formulas
where type-info is a list of f (a positive integer), f parameter types
and then the arrow types.  If there are no parameter types, then
type-info is a list of parameter types.  In case of all-formulas, f is
the total number of their free variables and the parameter types are
their types.

For a cases constant type-info is a list of parameter types followed
by an arrow-type.  Reason: for cases a singla arrow-type or all-formula
is sufficient.

adapted: make-const etc,
nbe-pconst-and-tsubst-and-rules-to-object rec-const-to-param-types
arrow-types-to-rec-consts type-info-to-rec-const
type-info-to-rec-consts alg-name-etc-to-rec-const rec-at
arrow-type-to-uninst-paramless-casesop-type-and-tsubst
arrow-type-to-cases-const param-types-and-arrow-type-to-cases-const

alg-name-etc-to-cases-const cases-at all-formula-to-cases-const
cases-const-to-param-types
const-substitute

grammar.scm

Rec case adapted

axiom.scm

adapted: all-formula-to-cases-aconst
all-formula-to-uninst-cases-imp-formula-and-tpinst
typed-constr-name-to-cases-step-formula

proof.scm

adapted: proof-and-genavar-var-alist-to-pterm
elim-npterm-and-var-genavar-alist-to-proof proof-of-stab-at-aux
proof-of-efq-at-aux 

pproof.scm

inst-with-to  error message inserted in case ? is an argument

adapted: atom-true-proof atom-false-proof efq-atom-proof stab-atom-proof
cases casedist

ets.scm

adapted: all-formulas-to-mr-ind-proof-aux
all-formula-to-mr-cases-proof-aux
proof-to-soundness-proof-aux

mpc.scm

mpc-cases-check adapted

atr.scm

all-formulas-to-c replaced by all-formula-to-c

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done
ets.scm  
type-to-canonical-compat-term corrected
Compat renamed into Eq-Compat
proof-to-extracted-term-aux corrected for Compat and Eq-Compat

pproof.scm  
=-compat-rev-at restricted to finitary algebras.
compat-rev-at	renamed into	 eq-compat-rev-at
=-compat-rev-at	renamed into	 compat-rev-at

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-05-28 
ets.scm  compat-aconst-to-mr-compat-proof implemented
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-05-27
atr.scm  avar-or-aconst... renamed into avar-or-ga...

ets.scm  Implementation of soundness added.
avar-or-aconst... renamed into avar-or-ga...

formula.scm  ex-free-formula? added

pconst.scm  In arrow-types-to-cases-const warning introduced in case it
is applied to more than one arrow-type.

axiom.scm  In all-formulas-to-uninst-imp-formula-and-tpinst error
message concerning `formulas missing for' removed

In all-formulas-to-cases-aconst warning introduced
in case it is applied to more than one all-formula.

In all-formulas-to-uninst-cases-imp-formula-and-tpinst error
message concerning `no flas for' removed

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Done 02-05-24
term.scm:  term-in-const-form-to-string adapted to new treatment
of Rec and Cases

list.scm: zip included
(zip '(1 3 5 ) '(2 4 6 )) => (1 2 3 4 5 6)

pconst.scm: 
arrow-types-to-rec-consts, param-and-arrow-types-to-rec-consts and
arrow-types-to-uninst-paramless-recop-types-and-tsubst (plural instead
of singular) introduced.

In arrow-types-to-uninst-paramless-recop-types-and-tsubst
error message "arrow types missing for" removed.  Reason: Simplified
type of recursion operator (in case of simultaneous recursion) allowed.

; New for Cases (as for Rec)
arrow-types-to-uninst-paramless-casesop-types-and-tsubst
constructor-type-to-cases-step-type (no change)
arrow-types-to-cases-const
arrow-types-to-cases-consts
param-and-arrow-types-to-cases-const
param-and-arrow-types-to-cases-consts
uninst-casesop-type-etc-to-cases-const (no change)
cases-at (no change)
all-formulas-to-cases-const (no change)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
proof.scm: proof-substitute-aux corrected: extend-subst replaced by
compose-o-substitutions, to do overwriting (in case all-intro) as
intended.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
done 02-05-07
axiom.scm

In assumption constants: type and predicate variables considered to be
bound.  aconst-to-inst-formula simplified: the internal type
substitution is not applied to the cterms.

aconst-substitute-aux and theorem-aconst-to-inst-proof generalized
accordingly.

psubst renamed into pinst (e.g. in 
all-formulas-to-uninst-cases-imp-formula-and-tpinst

ets.scm

ind-aconst-to-et-rec-const cases-aconst-to-if-term adapted
Initial steps towards giving an internal proof of correctness.

pconst.scm

  all-formulas-to-rec-const changed accordingly

pproof.scm

  aconst-substitute-aux replaced by explicit pinst in
  exc-formula-and-measure-to-min-pr-aconst
  exc-formula-to-exc-intro-aconst
  exc-formula-and-concl-to-exc-elim-aconst

  compat-rev-at and simpeq corrected

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
pconst.scm

  pconst-name-and-tsubst-to-object changed: if tsubst in unknown to pconst,
  this is not an error, but pconst is updated using const-substitute

~/minlog/lib/list.scm

  lh replaced by Lh (pconst names should be capitalized)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
count.tac 
  
  use of simp corrected

wf.tac  

  Now uses by-assume-with intead of ex-elim

pproof.scm 

  by-assume-with added, to make the use of existential hypotheses more
  intuitive.

  simp corrected: test (term-in-const-form? op) added

proof.scm 

  permutative conversions for Ex-Elim added

term.scm 

  permutative conversions for if-terms added

  typo in match-aux corrected: args -> alts

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
done 02-03-18:

log root.save root.tac adapted

log wftest.tac adapted

log axiom.scm
Corrected form of aconst-to-formula, which now applies 
formula-substitute-aux without violating the condition that psubst
should not concern pvars whose type is affected by tsubst.
To construct the formula associated with an aconst, it is useful to
separate the instantiated formula from the variables to be
generalized.  The latter can be obtained as free variables in
inst-formula.

log ets.scm  proof-to-extracted-term-aux corrected in theorem case

log axiom.scm theorem-aconst-to-inst-proof added

log formula.scm formula-substitute-aux changed in quantifier case

log term.scm term-substitute-aux changed in var and abstr case

For a full normalization of terms, including permutative conversions,
we define a preprocessing step that eta expands the alternatives of
all if-terms.  The result contains if-terme with ground type
alternatives only.

log proof.scm proof-substitute-aux corrected

reduce-efq-and-stab aconst case corrected

(expand-theorems proof) expands all theorems recursively.
(expand-theorems proof name-test?) expands (non-recursively) the
theorems passing the test by instances of their saved proofs.

context-item=? added.  proof-to-context corrected

proof-to-eta-nf in all-elim term-to-eta-nf for arg inserted

proof-to-aconsts added

For a full normalization of proofs, including permutative conversions,
we define a preprocessing step that eta expands each ex-elim axiom
such that the conclusion is atomic or existential.

Section 10-7. Existence elimination added.  In case of an ex-formulas
ex xs1 A1 ... ex xsn An and conclusion B we recursively construct a
proof of

ex xs1 A1 -> ... -> ex xsn An -> (all xs1,...,xsn.A1 -> ... -> An -> B) -> B.

Call a formula E essentially existential, if it can be transformed
into an existential form.  Inductive definition:

E ::= ex x A | A & E | E & A | decidable -> E (postponed)

We want to replace an implication with an essentially existential
premise by a formula with one existential quantifier less.
Application: search.  Given a formula A, reduce it to A* by
eliminationg as many existential quantifiers as possible.  Then search
for a proof of A*.  Since a proof of A* -> A can be contructed easily,
one obtains a proof of A.

log pproof.scm To simplify search when existential formulas are
present, we may use searchex, involving the procedures
formula-to-ex-red-formula and
formula-to-proof-of-ex-red-formula-imp-formula

log minpr.scm (theorem-name-to-proof "Cv-Ind") replaced by
(make-proof-in-aconst-form (theorem-name-to-aconst "Cv-Ind"))

log tvartest.scm  
Tests related to the (integrated) searchex.scm added, written 02-02 (Luminy)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

proof.scm
  proof-to-eta-nf: oversight corrected in all-elim case
  expand-theorems: in aconst case free variables (after subst) generalized
  cdp: check of types and t-degs in case all-elim added

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
done 02-02-24

axiom.scm
  typos corrected
  Optional eterms in theorems and global assumptions removed

ets.scm
  proof-to-extracted-term-aux: theorem case corrected.  There is no more
  need to store extracted terms of theorems.  Their type variables are
  difficult to handle, and it is much easier to use proof-subst.

  Global assumptions are handled as if they were assumption variables.
  Via make-avar-or-aconst-to-var we assign object variables to them.

lnf.scm
  extended to quantifier logic: proceed

lnf.tac
  now contains tests for proceed

pproof.scm 
  use corrected.  It now employs the auxiliary function
  formula-and-sig-vars-and-goal-to-subst-and-x-list-and-vars.  Change
  of formula-and-sig-vars-and-goal-to-subst-and-x-list-and-vars into
  formula-and-sig-vars-and-goal-to-subst-and-xs-and-vars, which now
  carries along the given x as its first argument.

  Change of use, use-with and inst-with.  Also in case of theorems
  (and not only global assumptions) whose final conclusion is a
  nullary predicate variable distinct from bot (e.g. Efq-Log or
  Stab-Log), this predicate variable is substituted by the goal
  formula.

  inst-with-to expects a string as its last argument, which is used (via
  name-hyp) to name the newly introduced instantiated hypothesis.

term.scm
  match corrected in case of different predicate symbols

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
done 02-02-20
axiom.scm
  avar=? made more efficient.
  formula-to-new-avar now has the name as an optional argument

proof.scm 
  optional context entry allowed in proofs (for efficiency reasons 
    when dealing with goals)
  In proof-to-eta-nf:
    (member avar context) replaced by (member-wrt avar=? avar context)
  formula-and-flex-and-goal-to-subst-and-x-list renamed into
    formula-and-sig-vars-and-goal-to-subst-and-x-list.  It now uses match
    instead of pattern-unify
  proof-to-expr uses avar names and indices
  DEFAULT-AVAR-NAME changed from "Hyp" to "u"
  A very primitive form check-and-display-proof added: only checks whether
    imp-elims are applied with correct formulas

pproof.scm
  use: formulas are tried in original as well as in normalized form.
  set-goal, assume, split now use formula-to-new-avar to guarantee new avars
  goals must contain the context now (for efficiency reasons).
    Changed accordingly: assume, use-with, inst-with, split,
    normalize-goal
  add-hypname-info corrected
  In cases: error message in case the argument is a string

typ.scm 
  type-match corrected

term.scm  
  match corrected and extended
  pattern-unify extended to if-terms
  In match-aux the application clause is corrected

  nbe-term-to-object corrected and extended.  We now have
  (term-to-string (nt (pt "[if boole True False]")))
  ; "boole"
  (term-to-string (nt (pt "[if nat 0 Succ]")))
  ; "nat"
  (term-to-string (nt (pt "[if nat 0 ([m]Succ m]"))))
  ; "nat"
  (term-to-string (nt (pt "[if nat 0 ([m]0)]")))
  ; 0

tvartest.scm  tests for type-match and match included

examples/dijkstra/count.tac added.  Proves (10) and (11) in [BS99].

Still to do:

inst-with sollte ein optionales Argument hyp-name bekommen

In search: preprocessing to eliminate superfluous existential quantifiers