Function application error with domain "witness"

[siddhartha-gadgil]

• This happens, for example, when parsing bool.ff_ne_tt from basic.lean.export
• Domain being a witness is meaningless, but should perhaps be interpreted as "to be ignored"

@ err.func  
res25: Term = (RecDataSym(_) : _) ↦ ($bt : 'q) ↦ rec_{ eq('q)('r) ; _ }(RecDataSym(_))

@ err.arg 
res26: Term = 'u

@ err.argT 
argType
@ err.argType 
res27: Typ[U] = 's('r)(_)

@ err.domOpt 
res28: Option[Typ[u]] = Some(_)

[siddhartha-gadgil]

The problem may be caused by witnesses but is more fundamental, as RecDataSym should never be seen on the outside. Here are more logs.

@ err.recFn 
res18: Term = (RecDataSym(_) : _) ↦ ($ov : 'q) ↦ rec_{ eq('q)('r) ; _ }(RecDataSym(_))

@ err.arg 
argsFmlyTerm 
@ err.argsFmlyTerm  
res19: Vector[Term] = Vector('q, 'r, ('v : 'q) ↦ ∏(_ : eq('q)('r)('v)){ 's('v)(_) })

@ err.indMod 
res20: TermIndMod = IndexedIndMod(Str(, "eq"), eq, Vector(eq.refl), 2, true)

@ err.argsFmlyTerm.map(_.typ)  
res21: Vector[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: Term }] = Vector(
  𝒰 ,
  'q,
  ('q → 𝒰 )
)

See also

@ val h = FormalAppln.unapply(hh).get._1 
h: Term = 's

@ h.typ 
res29: Typ[U] = ∏('s : 'q){ (eq('q)('r)('s) → 𝒰 ) }

[siddhartha-gadgil]

The peculiar witness type comes from proofLift

@ fml 
res45: Term = ('v :  'q) ↦ (_ ~> ((('s) ('v)) (_)))

@ val fmlO = proofLift(indNew.W, fmlRaw).runAsync 
fmlO: monix.execution.CancelableFuture[Term] = monix.execution.CancelableFuture$Pure@6a1c2d84

@ fmlO.value.get.get 
res47: Term = ($we :  'q) ↦ ((_ :  (((eq) ('q)) ('r)) ($we)) ↦ (_))

Note that we do need to deal with proofs differently, for instance here we have a mixed lambda and pi

[siddhartha-gadgil]

The peculiar case was coming because of a function application rule for applying a witness. There is a new error though.

@ exc.error  
res10: Exception = java.lang.IllegalArgumentException: attempting to apply (ind{((eq) ('q)) ('r)('t)}{($ev :  'q) ↦ ((_ :  (((eq) ('q)) ('r)) ($ev)) ↦ ((('s) ($ev)) (_)))}('u)) (_), which is not a function, to _ (and then to List())

This is presumably why the exception was made in the first place.

[siddhartha-gadgil]

Added rule to treat terms as constant functions of propositions. Handles the above error case, but should test many other cases.

[siddhartha-gadgil]

We do have the same error in RecFold, which is easy to correct. Have a different error for complex inductive types such as BinTree, which should be a separate issue.

[siddhartha-gadgil]

Concretely, we should also skip witnesses in the case where we actually have a function but domain does not match with the argument a witness, e.g. nat.pred_le

[siddhartha-gadgil]

This seems to shift the error, perhaps requiring feeding witnesses

provingground.interface.LeanRoutes.parse:205 message: "while parsing nat.pred_le, got provingground.interface.LeanParser$ParseException: provingground.HoTT$ApplnFailException: function (_ :  ((nat.less_than_or_equal) (_)) ((nat.succ) ('n))) \u21a6 (_) with domain(optional) Some(((n
at.less_than_or_equal) (_)) ((nat.succ) ('n))) cannot act on given term ((nat.less_than_or_equal.step) (_)) ('n) with type (((nat.less_than_or_equal) (_)) ('n)) \u2192 (((nat.less_than_or_equal) (_)) ((nat.succ) ('n)))"

[siddhartha-gadgil]

For convenience, should separate errors. It would also be convenient to avoid unicode.

[siddhartha-gadgil]

Example error:

while parsing nat.less_than_or_equal.dcases_on,
  got provingground.interface.LeanParser$ParseException:
    provingground.interface.RecFoldException:
      Failure to fold recursive Function for nat.less_than_or_equal, recursion function
      (_ : (('r) ('q)) (_)) ↦
        ((InducDataSym((nat.less_than_or_equal.step) ('q)) : ($hvi : nat ) ~> ((_ : ((nat.less_than_or_equal) ('q)) ($hvi) ) ~> (((('r) ($hvi)) (_)) → ((('r) ((nat.succ) ($hvi))) (_))))) ↦ (($hru : nat) ↦ (ind{(nat.less_than_or_equal) ('q)($hru)}{($hiz : nat) ↦ ((_ : ((nat.less_than_or_equal) ('q)) ($hiz)) ↦ ((('r) ($hiz)) (_)))}(_)(InducDataSym((nat.less_than_or_equal.step) ('q))))))
    with error provingground.HoTT$ApplnFailException:
      function (InducDataSym((nat.less_than_or_equal.step) ('q)) : ($hvi : nat ) ~> ((_ : ((nat.less_than_or_equal) ('q)) ($hvi) ) ~> (((('r) ($hvi)) (_)) → ((('r) ((nat.succ) ($hvi))) (_))))) ↦ (($hru : nat) ↦ (ind{(nat.less_than_or_equal) ('q)($hru)}{($hiz : nat) ↦ ((_ : ((nat.less_than_or_equal) ('q)) ($hiz)) ↦ ((('r) ($hiz)) (_)))}(_)(InducDataSym((nat.less_than_or_equal.step) ('q)))))
        with domain(optional)
          Some(($hvi : nat ) ~> ((_ : ((nat.less_than_or_equal) ('q)) ($hvi) ) ~> (((('r) ($hvi)) (_)) → ((('r) ((nat.succ) ($hvi))) (_)))))
        cannot act on given term
          ('u : nat) ↦ ((_ : ((nat.less_than_or_equal) ('q)) ('u)) ↦ ((_ : (_ : ((nat.less_than_or_equal) ('q)) ('u) ) ~> ((('r) ('u)) (_))) ↦ ((_ : ((nat.less_than_or_equal) ('q)) ((nat.succ) ('u))) ↦ (_))))
        with type
          ('u : nat ) ~> ((((nat.less_than_or_equal) ('q)) ('u)) → (((_ : ((nat.less_than_or_equal) ('q)) ('u) ) ~> ((('r) ('u)) (_))) → ((((nat.less_than_or_equal) ('q)) ((nat.succ) ('u))) → ((('r) ((nat.succ) ('u))) (_)))))

The mismatch seems to be in lambdas by witnesses, which are part of the argument but can be dropped. We can even try dropping them while paring.

[siddhartha-gadgil]

• After dropping lambda's for witnesses, there is an error of associativity in lambdas, with the argument being passed in fact not correctly formed as it depends on a witness variable.
• Can try to fix by also allowing such shuffles of arguments.

[siddhartha-gadgil]

• The mistake is in indexed induction having the wrong recursion data type, missing some argument terms.

[siddhartha-gadgil]

The reason is a misinterpretation of step as being a constant extension, presumably because of the witness issue

IndexedConstructorSeqDom[_1.SS, Term, _2.Fb, _2.Index, _1.Intros] = Cons(
  _,
  IndexedIdShape(FuncTypFamily(nat, IdTypFamily()), 'q :: HNil),
  Cons(
    (nat.less_than_or_equal.step) ('q),
    IndexedCnstDepFuncConsShape(
      nat,
      provingground.induction.TypFamilyExst$IndexedConstructorShapeExst$$Lambda$2281/505846681@3325a466
    ),
    Empty(nat.less_than_or_equal('q), FuncTypFamily(nat, IdTypFamily()))
  )
)