Simplify induction to Recursion

[siddhartha-gadgil]

• In many cases, especially from lean, a function is defined as inductive depending on a family, e.g. cases_on.
• Subsequently this is applied to a constant family.
• In this case, _.induc should simplify to _.rec

[babu-akhil]

Considering the case of induction on product types,
Given types A,B,C and AxB = ProdTyp(A,B),
indfn = AxB.induc(lmbda(a)(lmbda(b)(C))) and recfn = AxB.rec(C) should be equal
But right now, indfn == recfn gives a casting error.

So if the induc method checks if the family is constant and in that case returns a RecFn rather than InducFn, would that fix the problem?

[siddhartha-gadgil]

• Yes, the induc method should check if the function is constant and in that case return a RecFn.

• In addition though, giving a casting error for indfn == recfn is a bug - please report as an issue with details - and try to fix this :). The method with casting should be wrapped in a Try, i.e. we should use Try(check).getOrElse(false).

[siddhartha-gadgil]

@babu-akhil Okay, the bug where indfn == recfn gave a casting error was deeply nested and has now been fixed. So what remains is, as you said, if family is constant use RecFunc not InducFunc

[babu-akhil]

• recfn == indfn is not giving casting error but indfn == recfn still is. I'll try to fix this.

• I made the following change to induc :
  def induc[W <: Term with Subs[W]](
targetFmly: Func[U, Func[V, Typ[W]]]
) = {
val xy = prod.Var
val (x, y) = (xy.first, xy.second)
val d = (x ~>: (y ~>: targetFmly(x)(y))).Var
if ((targetFmly(x)(y).dependsOn(x)==false) && (targetFmly(x)(y).dependsOn(y)==false))
{val dd = (first ->: second ->: targetFmly(x)(y)).Var
dd :-> (RecFn(targetFmly(x)(y), dd): Func[PairTerm[U,V],W])
}
else {d :-> (InducFn(targetFmly, d): FuncLike[PairTerm[U, V], W])}
}
  But now there is a compilation error in the fileTermPatterns.scala. Here is the error message:
  /home/akhil/Provinground/ProvingGround/core/src/main/scala/provingground/translation/TermPatterns.scala:436:16: type arguments[_1,provingground.HoTT.FuncLike[provingground.HoTT.PairTerm[u,v],provingground.HoTT.Term]] do not conform to trait Func's type parameter bounds [W <: provingground.HoTT.Term with provingground.HoTT.Subs[W],+U <: provingground.HoTT.Term with provingground.HoTT.Subs[U]]
[error] applyAll(Some(pt.induc(fmly)), data)
[error] ^
[error] one error found

[siddhartha-gadgil]

• It seems that the error is because you removed the explicit types description for induc. Try putting it back - either the error will move to where it is clearer or will go away.

• The error is because the infered type fails to be "closed under substitution". This can be avoided by weakening the infered type if this is valid: otherwise the attempt to weaken gives an error.

• I made some more changes, so indfn == recfn may be fixed now. If not please report with full error message (use triple-backticks to enclode this and other longish code blocks).

[babu-akhil]

I put back the explicit type description for induc in ProdTyp and now the error is as follows:

[error] /home/akhil/Provinground/ProvingGround/core/src/main/scala/provingground/HoTT.scala:1111:12: type mismatch;
[error]  found   : provingground.HoTT.Func[provingground.HoTT.Func[U,provingground.HoTT.Func[V,W]],provingground.HoTT.Func[provingground.HoTT.PairTerm[U,V],W]]
[error]  required: provingground.HoTT.Func[provingground.HoTT.FuncLike[U,provingground.HoTT.FuncLike[V,W]],provingground.HoTT.FuncLike[provingground.HoTT.PairTerm[U,V],W]]
[error] Note: provingground.HoTT.Func[U,provingground.HoTT.Func[V,W]] <: provingground.HoTT.FuncLike[U,provingground.HoTT.FuncLike[V,W]], but trait Func is invariant in type W.
[error] You may wish to define W as +W instead. (SLS 4.5)
[error]         dd :-> (RecFn(targetFmly(x)(y), dd): Func[PairTerm[U, V], W])}

Should the definition of Func be changed to make it covariant in W ? I'm not sure if that is a legitimate change.

[siddhartha-gadgil]

No, Functions should not be covariant in their domains, as there is no natural way to make the domain of a function bigger (we can make the domain smaller or the codomain bigger). One has to conceptually figure out the correct definition.

…

On Wed, 12 Jun 2019 at 15:18, babu-akhil ***@***.***> wrote: I put back the explicit type description for induc in ProdTyp and now the error is as follows: [error] /home/akhil/Provinground/ProvingGround/core/src/main/scala/provingground/HoTT.scala:1111:12: type mismatch; [error] found : provingground.HoTT.Func[provingground.HoTT.Func[U,provingground.HoTT.Func[V,W]],provingground.HoTT.Func[provingground.HoTT.PairTerm[U,V],W]] [error] required: provingground.HoTT.Func[provingground.HoTT.FuncLike[U,provingground.HoTT.FuncLike[V,W]],provingground.HoTT.FuncLike[provingground.HoTT.PairTerm[U,V],W]] [error] Note: provingground.HoTT.Func[U,provingground.HoTT.Func[V,W]] <: provingground.HoTT.FuncLike[U,provingground.HoTT.FuncLike[V,W]], but trait Func is invariant in type W. [error] You may wish to define W as +W instead. (SLS 4.5) [error] dd :-> (RecFn(targetFmly(x)(y), dd): Func[PairTerm[U, V], W])} Should the definition of Func be changed to make it covariant in W ? I'm not sure if that is a legitimate change. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#170?email_source=notifications&email_token=AA3K3JDFLYJERAVWNDYMQCLP2DA6JA5CNFSM4EVOG3VKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODXP3TGI#issuecomment-501201305>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AA3K3JHSPK3TGAP75LAVE4LP2DA6JANCNFSM4EVOG3VA> .

* In many cases, especially from lean, a function is defined as inductive depending on a family, e.g. `cases_on`.

* Subsequently this is applied to a constant family.

* In this case, `_.induc` should simplify to `_.rec`

I saw the good first issue tag and would like to contribute.
Is Scala a prerequisite or is this more of a mathematical problem?

[siddhartha-gadgil]

The mathematics is well understood, so it is more a programming exercise (so needs scala).