semantics of induction

Stream: new members

[Aleksei]

Hi guys. Can someone explain semantics of induction n with d hd. I don't get what n, d and hd are. Maybe I can find some docs explaining this commands?

[Johan Commelin]

I moved your message. Please ask new questions in new streams. That way the discussion remains organized.

[Johan Commelin]

n should be the name of a variable in your context. d and hd are names for the variables to be used in the "induction step", the case P d → P (d+1).

[Johan Commelin]

So in that case, hd : P d will be the assumption that "the claim I'm trying to prove is true for d" and your goal will be "prove the claim for d+1"

[Arthur Paulino]

This might help: https://leanprover.github.io/reference/tactics.html#inductive-types
(I'm afraid it might not be very beginner friendly)

[Kevin Buzzard]

Do you understand mathematical induction? Knowing the mathematics behind what's going on will help with understanding what the variables mean.