inductive datatype parameter mismatch

Stream: lean4

[Andrés Goens]

I'm getting a message that I don't quite understand. I have the following inductively-defined proposition:

inductive instantaneousExecution (σ : Reactor ι υ) (ctx : Context ι) : Reactor ι υ → Context ι → Prop
 | refl : instantaneousExecution σ ctx σ ctx
 | trans {σ₁ σ₂: Reactor ι υ} {ctx₁ ctx₂ : Context ι} :
         (σ, ctx) ⇓ᵢ (σ₁, ctx₁) →
         instantaneousExecution σ₁ ctx₁ σ₂ ctx₂ →
         instantaneousExecution σ ctx σ₂ ctx₂

And Lean4 tells me:

inductive datatype parameter mismatch
  σ₁
expected
  σ

But I don't understand why it expects the first parameter (σ) there. I'd assume those are the parameters to the constructor instantaneousExecution, and in the end I am defining an implicit function from the first parameter by the last → instantaneousExecution σ ctx σ₂ ctx₂. What's the flaw in my reasoning here?

If I try to reduce this to a simpler example, looking for a #MWE, then it works fine, e.g. something like:

inductive foo (σ : ℕ) : ℕ → Prop
 | constructor {σ₁ σ₂ : ℕ} : σ₁ = σ₂ → foo σ σ₁

works perfectly fine. Am I not doing the same thing above? Do the type parameters to the type matter (Reactor and Context in the example above)? There's also some (not shown) typeclasses for some of these variables (like υ), but that shouldn't matter either, should it?

Thanks!

[Chris B]

What you're doing is:

inductive foo (σ : ℕ) : ℕ → Prop
 | constructor {σ₁ σ₂ : ℕ} : σ₁ = σ₂ → foo σ σ₁ → foo σ₁ σ₂

You need to make σ an index instead of a parameter (by moving it to the right of the colon in the declaration) if you want it to be able to vary.

[Chris B]

inductive instantaneousExecution : Reactor ι υ →  Context ι →  Reactor ι υ → Context ι → Prop

You can keep the labels like this:

inductive instantaneousExecution : ∀ (σ : Reactor ι υ) (ctx : Context ι), Reactor ι υ → Context ι → Prop

[Chris B]

Fwiw the 'why' is that you get different recursors.

-- indexed
inductive X : Nat → Nat → Prop
| refl : X a a
| step (b : Nat) : X a b -> X a b.succ

#print X.rec
/-
recursor X.rec : ∀ {motive : (a a_1 : ℕ) → X a a_1 → Prop},
  (∀ {a : ℕ}, motive a a (_ : X a a)) →
    (∀ {a : ℕ} (b : ℕ) (a_1 : X a b), motive a b a_1 → motive a (Nat.succ b) (_ : X a (Nat.succ b))) →
      ∀ {a a_1 : ℕ} (t : X a a_1), motive a a_1 t
-/

-- param
inductive Y (a : Nat) : Nat → Prop
| refl : Y a a
| step (b : Nat) : Y a b -> Y a b.succ

#print Y.rec
/-
recursor Y.rec : ∀ {a : ℕ} {motive : (a_1 : ℕ) → Y a a_1 → Prop},
  motive a (_ : Y a a) →
    (∀ (b : ℕ) (a_1 : Y a b), motive b a_1 → motive (Nat.succ b) (_ : Y a (Nat.succ b))) →
      ∀ {a_1 : ℕ} (t : Y a a_1), motive a_1 t
-/