using recursor to write term

Stream: general

[Kevin Buzzard]

I'm trying to be a computer scientist, unsuccessfully. I'm trying to define a function in term mode.

inductive C : Type
| c1 : C
| c2 : C

inductive D : Type
| d1 : D
| d2 : D

def thing1 (c : C) (d : D) : D :=
c.rec
  (_) -- correct "don't know how to synthesize placeholder -- here's a helpful context"
  (_) -- correct

def thing2 (c : C) (d : D) : D :=
c.rec
  (d.rec _ _)
  (_)

/-
type mismatch at application
  C.rec (D.rec ?m_3 ?m_4 d)
term
  D.rec ?m_2 ?m_3 d
has type
  ?m_1 d : Sort ?
but is expected to have type
  ?m_1 C.c1 : Sort ?
  -/

thing1 is where things are going well. I want to use recursion on c and so I write c.rec _ _ and both underscores have nice red underlines, indicating that I'm on the right track.

But then I want to use recursion on d too, so I edit thing1 until it becomes thing2 and instead of having now three nice red underlines under my three underscores, Lean just gives up, flags the c in c.rec as an error. In reality the two inductive types are far more complicated and have parameters etc.

Is there some trick to persuade Lean to start telling me the local context at every underscore? Have I just made some more basic error? It is going to be a royal pain figuring out all the types in my use case (some proofs are involved, I will need to drop into tactic mode at some point to supply all the terms needed).

Am I missing a trick? Have I made an error?

[Chris Hughes]

Try D.rec_on d. I think there's a bug where it doesn't use the elab_as_eliminator when you use projection notation

[Chris Hughes]

Also C.rec_on c

[Kevin Buzzard]

I think I love you. Many thanks!

[Kevin Buzzard]

Works in my real use case too :D I'm sure this has caused me problems on several occasions in the past. It's only now I am confident enough to start saying "I think this should work" rather than just saying "maybe I need to understand things better".

[Kevin Buzzard]

@Ellen Arlt I can write that function now.