minlog 4.0.99.20100221-5.2 / usr / share / minlog / src / todo.scm

; $Id: todo.scm 2281 2008-08-11 12:22:55Z schwicht $

; 2008-06-14: Some exioms are only there for convenience.  They could
; be proved if the predicate constants Equal and Total are replaced by
; inductively defined predicates, and pair types are defined.  The
; only axioms unprovable from the intro and elimination axioms are
; finalg-to-=-to-e-1-aconst and finalg-to-=-to-e-2-aconst, and the
; (implicit) axioms stating that the constructors are injective and
; have disjoint ranges.  -- 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).

; 2008-03-13: Fine tune the refined A translation by uniformity.

; 2007-07-12: Change Pvar^' into Pvar.  That is: for pvars ^ (') means
; *no* positive (negative) content.  This is different from the usage
; of ^ for object variables (where x^ is more general than x), but
; seems to be more appropriate for pvars.

; 2006-02-16.  Quantification over type variables and predicate
; variables should be admitted.  We remain predicative, if we restrict
; all-elimination to comprehension terms without predicate and type
; quantifiers (see Takeuti: Two applications of Logic to Mathematics).
; For normalization of proofs via terms, we also need type abstraction
; in terms.  -- One benefit: The lemmata for Dickson can be formulated
; and used in their original generality.

; 2006-01-01.  It would be good to have (admit), which admits the
; present goal by adding a corresponding global assumption.  -- Done.

; 2005-12-28.  pp gives an incorrect result:
(pp (pf "boole & (all unit.boole1 -> boole2) & (all unit.boole1 -> boole2)"))
boole & all unit.boole1 -> boole2 & all unit.boole1 -> boole2
Done.  Moreover, by setting DOT-NOTATION to #t or #f, one can switch.

; 2005-12-04.  pp does not work for types
(type-to-string type) ;"nat yplus unit=>alpha3=>alpha3=>alpha3"
(pp type)
; Error in car: () is not a pair.
Done

; 2005-12-04.  When an algebra is created, one should add a
; computation rule sending (Inhab alg) into the first nullary
; constructor, if there is one.  Otherwise, e.g., for the algebra
; "term", one can add a computation rule (pt "(Inhab term)") --> (pt
; "Var 0").  One can also change the canconical inhabitant.  Example:
; (pt "(Inhab boole)") --> (pt "False"), instead of True.
; type-to-canonical-inhabitant gives for a non-algebra ground type the
; term (pt "(Inhab type)"), which may or not normalize to something
; else.

; This view should simplify add-ids: there is no need to create
; DummyalgAcc etc.

; 2005-12-03.  simphyp does not allow to give names to the newly
; introduced hypotheses.

; 2005-12-03:  There are cases when we need to normalize twice.
; Problem: by beta conversion we get terms where an if-term can be
; eta expanded.  Example, using listrev.scm:

(add-var-name "bc" (py "list(boole@@boole)"))
(add-var-name "pq" (py "boole@@boole"))

(define term
  (pt "([bc]([pq]left pq)map bc)
       (([i][if boole (False@False) (True@True)])fbar k)"))

(pp (nt term))
; ([n0]left[if boole (False@False) (True@True)])fbar k
(pp (nt (nt term)))
; ([n0][if boole False True])fbar k

; -- Done, by correction of normalize-term-pi-with-rec-to-if in term.scm

; 2005-12-03.  Naming conventions should be observed generally.  (1) A
; theorem or global assumptions with computational content sould have
; a valid token string as name.  It should start with a capital, to
; make the prefix "c" (for content) readable.  (2) Type qualifiers
; should be either always in front or always at the end.

; 2005-12-01.  use should be made usable for formulas with type and
; predicate variables of non-null arity.  So allow lists of types and
; strings for variables in the arguments.  Match should then infer the
; comprehension terms.

; 2005-12-01.  (pp (pf "all n ex m.T -> F")) => all n.ex m.T -> F with
; an unnecessary dot.
; Done

; 2005-12-01.
; (inst-with-to "WKL!" (pt "Ext t(Up s)") "?" "?" "?" "ExHyp1") =>
; ? illegal for inst-with-to; use inst-with instead.
; Why not give a name to  the resulting instantiated hypothesis?

; 2005-12-01.
; In a goal whose context is without t, executing
; (inst-with "WKL!" (pt "Ext t(Up s)") "?" "?" "?") 
; (assert (pf "T")) =>
; unexpected free variables
; t
; Problem: we have produced an incorrect context, which is noticed in
; context-and-cvars-and-formula-to-new-goal
; At least a warning should be given.  Better: forbid it.  The 
; drinker formula can be proved using (Inhab alpha)

; Modified x-and-x-list-to-proof-and-new-num-goals-and-maxgoal
; accordingly (In examples/classical/test.scm).  Now tests from
; quant.tac showed problems:

(define all-exca  (pf "all x Q x -> (all x.Q x -> F) -> F"))
(set-goal all-exca)
(assume 1 2)
(use 2 (pt "(Inhab alpha)"))
; attempt to apply all-elim to non-total term
; (Inhab alpha)

(define all-exca  (pf "all x^ Q x^ -> (all x^.Q x^ -> F) -> F"))
(set-goal all-exca)
(assume 1 2)
(use 2 (pt "(Inhab alpha)"))
(use 1)
(dnp)

; However, search finds a proof with a free variable x^ !
(set-goal all-exca)
(search)
(dnp)

; Also cdp thinks that this proof is correct
(cdp (current-proof))

; So both have to be adapted as well.

; 2005-12-01.  Why is boole@@boole not finitary?  Answer: For finitary
; types we have recursion and induction, and this should not be
; duplicated.  Use the tensor algebra instead.