Recursive call on inductive prop error with casesOn

Stream: new members

[Bob Rubbens]

Hello everyone, I've been trying to do a recursive computation on an inductive type that represents a transitive closure. However I'm running into an error from lean 4, at the pattern match in the tryRec function:

tactic 'cases' failed, nested error: tactic 'induction' failed, recursor 'tc.casesOn' can only eliminate into Prop

When I change my inductive type to not be in Prop, the pattern matching works. However, then I cannot do "tc ... ∧ ..." anymore, as "tc ..." is no longer in prop.

For context: my goal is to have the transitive closure of a small-step semantics, and then use a recursive function to walk the trace of states extracted from the transitive closure to prove things about the trace, such as some state is reached such that... For that I'll need to pattern match on the transitive closure, and do a recursive call on the "step" case of the tc type.

Can somebody point me towards a source that explains how to do this, or explain what I'm doing wrong/what a more idiomatic way to do this is? Code snippet reproducing the problem included below. I'm very new to lean so all tips are welcome!

def x : Nat → Nat → Prop
| _, _ => True

-- Pattern matching works when defined as follows, but then tc is not in Prop anymore:
-- inductive tc (α : Sort u) (r: α → α → Prop) : α → α → Sort (max u 1) where

-- Works for ∧, but breaks pattern matching:
inductive tc (α : Sort u) (r: α → α → Prop) : α → α → Prop where

| base (h: r a b) : tc α r a b
| step (hh: r a b) (ht: tc α r b c) : tc α r a c

def tcAnd : tc Nat x 0 1 ∧ True :=
  (And.intro
    (tc.base (True.intro))
    True.intro
  )

def tryRec : (a b : Nat) → tc Nat x a b → Prop
| _, _, (tc.base h) => True
| a, b, (tc.step hh ht) => True

[Bob Rubbens]

I see my question is already discussed on the "Matching on Prop" thread at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matching.20on.20prop . I guess I'll need to read that and think. Sorry for the useless post.