Zulip Chat Archive

Stream: general

Topic: using recursor to write term


view this post on Zulip Kevin Buzzard (Nov 13 2019 at 13:26):

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?

view this post on Zulip Chris Hughes (Nov 13 2019 at 13:27):

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

view this post on Zulip Chris Hughes (Nov 13 2019 at 13:29):

Also C.rec_on c

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 13:49):

I think I love you. Many thanks!

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 14:13):

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".

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 14:14):

@Ellen Arlt I can write that function now.


Last updated: May 17 2021 at 21:12 UTC