Design pattern for further constraining inductive predicate

Stream: new members

[pandaman]

Hello. I have an inductive predicate that represents a reflexive transitive closure of a relation:

inductive Closure (R : Nat → Nat → Prop) : Nat → Nat → Prop where
  | refl : Closure R a a
  | cons : R a b → Closure R b c → Closure R a c

I'd like to define another predicate that restricts the left hand side of each step using a predicate P. One way to do this is to embed the predicate like this:

inductive RestrictedClosure (R : Nat → Nat → Prop) (P : Nat → Prop) : Nat → Nat → Prop where
  | refl : RestrictedClosure R P a a
  | cons : P a → R a b → RestrictedClosure R P b c → RestrictedClosure R P a c

However, it's a bit annoying that we need to define a new predicate. Alternative way is to define Closure as Type and attach a predicate like this

inductive Closure' (R : Nat → Nat → Prop) : Nat → Nat → Type where
  | refl : Closure' R a a
  | cons : R a b → Closure' R b c → Closure' R a c

def Closure'.Restricted (P : Nat → Prop) : Closure' R a b → Prop
  | .refl => True
  | .cons _ cls => P a ∧ cls.Restricted P

This way, we don't need to define a separate predicate, but Closure' is no longer a subsingleton and I'm not sure how that affects my proofs using Closure. Does anyone have ideas for simplifying the set up like this?

To give a bit of context, my project involves an NFA and I'd like to define a predicate like "we have a path where each state satisfies some condition". Currently, I'm embedding the condition in the definition (example), but wondering if there is another way.

[pandaman]

#new members > What do propositional types do for us? answers some questions about Prop vs Type.

[Chris Bailey]

Can you just declare the more complicated one first and define the simpler one with it?

inductive RestrictedClosure (R : Nat → Nat → Prop) (P : Nat → Prop) : Nat → Nat → Prop where
  | refl : RestrictedClosure R P a a
  | cons : P a → R a b → RestrictedClosure R P b c → RestrictedClosure R P a c

-- potentially want to make this reducible/an abbrev
def Closure (R) := RestrictedClosure R (fun _ => True)

[pandaman]

Well, it doesn't cover the case like when I want to constrain both side. Maybe I should just include both in P to make it maximally generic

[Chris Bailey]

Can you elaborate on what you mean by constraining both sides?

[pandaman]

-- We might need to define another predicate if I want to allow P to look at both a and b.
-- That being said, this is more general than RestrictedClosure so it's enough to have this.
inductive RestrictedClosure' (R : Nat → Nat → Prop) (P : Nat → Nat → Prop) : Nat → Nat → Prop where
  | refl : RestrictedClosure R P a a
  | cons : P a b → R a b → RestrictedClosure R P b c → RestrictedClosure R P a c

[Daniel Weber]

Can't you just apply Closure to P \and R?