Confusing induction motive error message

Stream: new members

[aron]

I get error message:

Expected resulting type of eliminator to be an application of one of its parameters (the motive), but found
  ∃ resolvedCtx, ResolveCtx resultCtx resolvedCtx

when I try to do induction this way:

theorem UnifyConcs.can_make_ResolveCtx (hwas : CtxAllResolved ctx) (h : UnifyConcs a b ctx unif resultCtx) : ∃ resolvedCtx, ResolveCtx resultCtx resolvedCtx := by
  induction h using UnifyConcs.rec (motive_1 := λ (a b : Ty) (ctx : Ctx) (resultTy : Ty) (resultCtx : Ctx) (h : UnifyConcs a b ctx resultTy resultCtx) ↦ ∃ resolvedCtx, ResolveCtx resultCtx resolvedCtx)

I don't understand what this error message means. As far as I can tell I am trying to return the exact same prop that the theorem expects.

When I do induction h using UnifyConcs.rec (motive_1 := _) the error goes away and the hole is inferred to be (a b : Ty) → (ctx : Ctx) → (resultTy : Ty) → (resultCtx : Ctx) → UnifyConcs a b ctx resultTy resultCtx → Prop which as far as I can tell exactly matches what I'm trying to do?

I'd like to make a #mwe but there are >5000 lines of preceding context to this and I have no idea which parts of it are key to triggering this error

[Kenny Lau]

why are you providing your own motive and why does your motive not change the goal at all (that's what the error means)

[Kenny Lau]

usually if you induction n where n : Nat then the goal will change to P 0 and P (n + 1)

[Kenny Lau]

and can you post the output of #print UnifyConcs

[aron]

Kenny Lau said:

why are you providing your own motive

I need to provide my own motive because UnifyConcs is mutually recursive with UnifyIndices, and all the UnifyIndices cases have a goal like ?m.38 i✝ i✝ ctx✝ (Ty.uniVar i✝) ctx✝ ⋯ otherwise

[aron]

Kenny Lau said:

and can you post the output of #print UnifyConcs

Ok but there is a lot going on :grimacing:

inductive UnifyConcs : Ty → Ty → Ctx → Ty → Ctx → Prop
number of parameters: 0
constructors:
UnifyConcs.prims : ∀ {p : PrimTy} {ctx : Ctx},
UnifyConcs (Ty.shape (TyInner.prim p)) (Ty.shape (TyInner.prim p)) ctx (Ty.shape (TyInner.prim p)) ctx
UnifyConcs.pairs : ∀ {fstA fstB : Ty} {ctx : Ctx} {fstUnif : Ty} {resultCtx1 : Ctx} {sndA sndB sndUnif : Ty}
{resultCtx2 : Ctx},
UnifyConcs fstA fstB ctx fstUnif resultCtx1 →
UnifyConcs sndA sndB resultCtx1 sndUnif resultCtx2 →
UnifyConcs (Ty.shape (TyInner.pair fstA sndA)) (Ty.shape (TyInner.pair fstB sndB)) ctx
(Ty.shape (TyInner.pair fstUnif sndUnif)) resultCtx2
UnifyConcs.arrows : ∀ {fstA fstB : Ty} {ctx : Ctx} {fstUnif : Ty} {resultCtx1 : Ctx} {sndA sndB sndUnif : Ty}
{resultCtx2 : Ctx},
UnifyConcs fstA fstB ctx fstUnif resultCtx1 →
UnifyConcs sndA sndB resultCtx1 sndUnif resultCtx2 →
UnifyConcs (Ty.shape (TyInner.arrow fstA sndA)) (Ty.shape (TyInner.arrow fstB sndB)) ctx
(Ty.shape (TyInner.arrow fstUnif sndUnif)) resultCtx2
UnifyConcs.uniVars : ∀ {a b : ℕ} {ctx : Ctx} {unif : Ty} {resultCtx : Ctx},
UnifyIndices a b ctx unif resultCtx → UnifyConcs (Ty.uniVar a) (Ty.uniVar b) ctx unif resultCtx
UnifyConcs.concUniVar : ∀ {resA a : TyInner} {ctx : Ctx} {hrange : TyUvsInRange ctx (Ty.shape a)} {i : ℕ}
{tyAtIndex unif : Ty} {resultCtx : Ctx},
Ty.shape resA = (Ty.shape a).resolveUniVars ctx hrange →
IsAtRevIndex i ctx (TyMaybe.conc tyAtIndex) →
UnifyConcs (Ty.shape resA) tyAtIndex ctx unif resultCtx → UnifyConcs (Ty.shape a) (Ty.uniVar i) ctx unif resultCtx
UnifyConcs.uniVarConc : ∀ {resB b : TyInner} {ctx : Ctx} {hrange : TyUvsInRange ctx (Ty.shape b)} {i : ℕ}
{tyAtIndex unif : Ty} {resultCtx : Ctx},
Ty.shape resB = (Ty.shape b).resolveUniVars ctx hrange →
IsAtRevIndex i ctx (TyMaybe.conc tyAtIndex) →
UnifyConcs tyAtIndex (Ty.shape b) ctx unif resultCtx → UnifyConcs (Ty.uniVar i) (Ty.shape b) ctx unif resultCtx
UnifyConcs.unspecUniVar : ∀ {i : ℕ} {ctx resultCtx : List TyMaybe} {resolvedResultCtx : Ctx} {b : TyInner},
IsAtRevIndex i ctx TyMaybe.unspec →
SetAtRevIndex i ctx (TyMaybe.conc (Ty.shape b)) resultCtx →
ResolveCtx resultCtx resolvedResultCtx → UnifyConcs (Ty.uniVar i) (Ty.shape b) ctx (Ty.shape b) resolvedResultCtx
UnifyConcs.uniVarUnspec : ∀ {i : ℕ} {ctx resultCtx : List TyMaybe} {resolvedResultCtx : Ctx} {a : TyInner},
IsAtRevIndex i ctx TyMaybe.unspec →
SetAtRevIndex i ctx (TyMaybe.conc (Ty.shape a)) resultCtx →
ResolveCtx resultCtx resolvedResultCtx → UnifyConcs (Ty.shape a) (Ty.uniVar i) ctx (Ty.shape a) resolvedResultCtx

[aron]

Kenny Lau said:

and why does your motive not change the goal at all (that's what the error means)

oh what. is that all the error means? why would that be an error?

[Aaron Liu]

aron said:

When I do induction h using UnifyConcs.rec (motive_1 := _) the error goes away and the hole is inferred to be (a b : Ty) → (ctx : Ctx) → (resultTy : Ty) → (resultCtx : Ctx) → UnifyConcs a b ctx resultTy resultCtx → Prop which as far as I can tell exactly matches what I'm trying to do?

Look carefully, it's not the same

[aron]

but actually yeah I think that helps, because I think I was wrongly specifying motive_1. motive_2 is what I need to specify, because it's for motive 2 that the goals look like ?m.38 a✝⁴ b✝ ctx✝ (Ty.uniVar b✝) resultCtx✝ ⋯.

And looks like... yeah when I specify only motive_2 the error goes away :tada:

theorem UnifyConcs.can_make_ResolveCtx (h : UnifyConcs a b ctx unif resultCtx) (hwas : CtxAllResolved ctx) : ∃ resolvedCtx, ResolveCtx resultCtx resolvedCtx := by
  induction h using UnifyConcs.rec
    (motive_2 := λ {a b : Nat} {ctx : Ctx} {unif : Ty} {resultCtx : Ctx} (h : UnifyIndices a b ctx unif resultCtx) ↦ (hwas : CtxAllResolved ctx) → ∃ resolvedCtx, ResolveCtx resultCtx resolvedCtx)

[Aaron Liu]

oh is the problem resolved?

[aron]

yeah I think so!

[aron]

Aaron Liu said:

same

uhh is it not? what's the difference?

[Aaron Liu]

one is the type of the other oh it might be how the hovers work

[Kenny Lau]

how do you keep up with all this complexity

[Aaron Liu]

sometimes the hovers display the term and sometimes they display the type of the term

[aron]

Kenny Lau said:

how do you keep up with all this complexity

sigh. dude. it's been a rough journey.

[Kenny Lau]

i mean, I assume you're following a paper, how does the paper do it, does it have more notations (check my zulip status)

[aron]

uhh I'm not following any paper

I'm just, like, doing my own thing :tear:

[aron]

(trying to, anyway)

[Aaron Liu]

curious, what are you doing? looks like some sort of unifcation or something?

[aron]

lol yup that's exactly what I'm doing. currently working on an implementation (formalisation?) of a simple monomorphic type system with unification

[aron]

unification has been... very difficult. i'm only now getting close to the end (i hope)

[aron]

implementing a simple monomorphic type inference/checking took me a few months but a big part of that was learning how lean works, how to prove things, tactics, how to represent things, and so on. adding unification on top of that has taken me about 4 months so far

[aron]

implementing the occurs check when you need to prove termination is rough. so is proving things about a unification variable context when you're "mutating" that context in the process of unifying types