Subtype and cases

Stream: general

[Fabrizio Montesi]

In #computer science > CCS behavioural theory, we're trying to use Subtype to exclude some cases of an inductive:

inductive Act : Type u where
  | name (a : Name)
  | coname (a : Name)
  | τ

/-- An action is visible if it a name or a coname. -/
def Act.IsVisible (μ : Act Name) : Prop :=
  match μ with
  | name _ => True
  | coname _ => True
  | τ => False

/-- The type of visible actions. -/
abbrev VisibleAct := { μ : Act Name // μ.IsVisible } -- Tried both abbrev and def, no big difference

That works well, and match seems smart at detecting that when we deal directly with values of that subtype.

But when we try to do cases on another inductive with a constructor that uses the subtype, like this

inductive Tr : Process Name Constant → Act Name → Process Name Constant → Prop where
  ...
  | com {μ : VisibleAct Name} :
    Tr p μ p' → Tr q μ.co q' → Tr (par p q) Act.τ (par p' q')
  ...

we get into trouble with dependent elimination. To solve that, we gotta do cases on the subtype value first, which is annoying: https://github.com/leanprover/cslib/blob/2f5aa093f3facb49d51dbac76087f781d1f89406/Cslib/Languages/CCS/BehaviouralTheory.lean#L140

Perhaps this has been discussed in general terms already?

[Eric Wieser]

Does defining the predicate as an inductive type help?

[Fabrizio Montesi]

You mean IsVisible? I'll try, it might!

[Fabrizio Montesi]

It doesn't, unfortunately. I've hacked a bit at the Coe instance for the subtype, and making one manually using match reveals that cases on a Tr tries to do this:

Dependent elimination failed: Failed to solve equation
  (match μ.co with
    | ⟨name a, property⟩ => name a
    | ⟨coname a, property⟩ => coname a) =
    τ

[Fabrizio Montesi]

(Lean is able to see that the match is complete, btw.)

[Edward van de Meent]

is there a chance that something like fun_cases or fun_induction is a tactic that does what you want?

[Edward van de Meent]

alternatively, you could try to write your own inductive principle for the cases/match/induction you want (where you do the cases on the subtype first), then set that to the default (if that is something you want) or manually supply that whenever you need to do this kind of matching by supplying a using argument

[Edward van de Meent]

finally, if neither of those work, you could consider passing around the proof as a separate argument, rather than working with Subtype

[Fabrizio Montesi]

I've tried these options. The second was the most promising, but the issue is that I'm doing cases on Tr, which has a constructor using the subtype in question. That's where it fails. If I try a using, it complains that the recursor is for VisibleAct instead of Tr.

What's cases doing when it deals with Tr.com? I feel like it's blindly (but understandably) applying the recursor for Act, because that's what the subtype is upcast to in Tr.com. Is there any way to control this?

[Edward van de Meent]

what i meant is write a custom inductor for Tr which you supply with using (or set to default)

[Fabrizio Montesi]

Ah, that'd of course be an option, but it'd also mean renouncing modularity, as the details of how I implemented VisibleAct end up affecting all the types that use it. If I had defined VisibleAct as a normal inductive copy-pasting the constructors from Act, I wouldn't have this problem, I expect. (Edit: actually, maybe I would, because I'd still have the upcast in Tr.com? Will check.)
I'm trying to find a way that avoids this copy-paste.