Understanding shadowing in an inductive family

Stream: general

[Markus de Medeiros]

Hopefully this is a basic question but I've been scratching my head about it. Why is it that in the first case of this inductive type β is shadowed, while in the second case it is not? How would you write an inductive type like this one where the types are never shadowed, ie the arguments to f always have the same types as the arguments to Ty?

inductive Ty : Type _ → Type _ → Type _ where
| C1 : (f : α → β → Prop) → Ty α β
| C2 : (f : α → Prop) → Ty α α

def F {α β : Type _} (t : Ty α β) : Unit :=
  match t with
  | Ty.C1 f =>
      /- α β : Type u_1
         t : Ty α β
         β : Type u_1            -- β is shadowed
         f : α → β → Prop
         ⊢ Unit -/
      sorry
  | Ty.C2 f =>
     /- α β : Type u_1
       t : Ty α β
       f : α → Prop
       ⊢ Unit -/
     sorry

[Shreyas Srinivas]

It has something to do with the way \alpha and \beta are implicitly inferred for the constructors

[Shreyas Srinivas]

See below

inductive Ty : Type u → Type u → Type (u + 1) where
| C1 {α β : Type u} : (f : α → β → Prop) → Ty α β
| C2 {α β : Type u}: (f : α → Prop) → Ty α α

def F {α β : Type _} (t : Ty α β) : Unit :=
  match t with
  | Ty.C1 f => by
      /-
        α β✝ : Type ?u.710
        t : Ty α β✝
        β : Type ?u.710
        f : α → β → Prop
        ⊢ Unit -/
      sorry
  | Ty.C2 f => by
     /- α β : Type ?u.710
        t : Ty α β
        β✝ : Type ?u.710
        f : α → Prop-/
     sorry

[Shreyas Srinivas]

Then if you change the type of the second constructor to Ty α β the shadowing behaviour disappears

[Markus de Medeiros]

Hm, thanks. This is still quite counterintuitive to me even with α and β made explicit. Unfortunately I do want to avoid the shadowing and I can't change the type of my second constructor, I wonder if there's some way to do this.

[Shreyas Srinivas]

By making the constructors explicit

[Shreyas Srinivas]

inductive Ty : Type _ → Type _ → Type _ where
| C1 : (f : α → β → Prop) → Ty α β
| C2 : (f : α → Prop) → Ty α α

def F {α β : Type _} (t : Ty α β) : Unit :=
  match t with
  | @Ty.C1 α β f =>by
      sorry
  | @Ty.C2 α f => by
     sorry

[Shreyas Srinivas]

Oh wait that should have worked

[Shreyas Srinivas]

Sorry I take that back

[Shreyas Srinivas]

Okay I have a bad workaround:

inductive Ty : Type _ → Type _ → Type _ where
| C1 {α β} : (f : α → β → Prop) → Ty α β
| C2 {α} : (f : α → Prop) → Ty α α

def F {α β : Type _} (t : @Ty α β) : Unit :=
  match h1: t with
  | @Ty.C1 α β f =>by
      expose_names
      let t' := h ▸ t
      /-
        1 goal
        α β✝ : Type ?u.577
        t : Ty α β✝
        β : Type ?u.577
        f : α → β → Prop
        h✝ : β✝ = β -- note this
        h : HEq t (Ty.C1 f)
        ⊢ Unit
        All Messages (1)
      -/
      sorry
  | @Ty.C2 α f => by
     sorry

[Shreyas Srinivas]

I was able to get match to give me the equality between the shadowed and non shadowed \beta

[Shreyas Srinivas]

and then get a t' that I can work with

[Shreyas Srinivas]

You can restrict the scope of tactic mode by putting it inside the let declaration

[Shreyas Srinivas]

inductive Ty : Type _ → Type _ → Type _ where
| C1 {α β} : (f : α → β → Prop) → Ty α β
| C2 {α} : (f : α → Prop) → Ty α α

def F {α β : Type _} (t : @Ty α β) : Unit :=
  match h1: t with
  | @Ty.C1 α β f =>
      let t' := by
        expose_names
        exact h ▸ t
      sorry
  | @Ty.C2 α f => sorry

[Shreyas Srinivas]

It's ugly because this substitution stuff doesn't work well with defeq and because I had to use expose_names. I hope someone like Kyle or Mario comes along and saves the day with a better answer.

[Shreyas Srinivas]

The fact that it introduces a second \beta suggests it can't tell whether the \beta in the args of F can be unified with the \beta in the constructor at some step.

[Shreyas Srinivas]

CC : @Mario Carneiro

[Mario Carneiro]

I think the use of indices in Ty is the issue. Lean is able to promote α to a parameter but not β because it changes in C2

[Mario Carneiro]

if C2 instead had an equality argument then they could both be promoted to parameters and you wouldn't have this issue

inductive Ty : Type _ → Type _ → Type _ where
| C1 {α β} : (f : α → β → Prop) → Ty α β
| C2 {α β} : α = β → (f : α → Prop) → Ty α β

def F {α β : Type _} (t : @Ty α β) : Unit := by
  match t with
  | Ty.C1 f => sorry
  | Ty.C2 e f => subst e; sorry

[Markus de Medeiros]

I see. So the variables that can get promoted and hence not shadowed are the ones that are the same in all results of constructors (I don't know what the terminology for this is but the last Ty _ _ in every line).

This is interesting, I think Lean is different to Rocq in this regard no?

[Mario Carneiro]

yes that's right

[Mario Carneiro]

Rocq is different because it uses match+fix instead of recursors

[Mario Carneiro]

the recursor generated for such a type will have to generalize beta

[Markus de Medeiros]

Ty for the explanation!

[Shreyas Srinivas]

Btw, in my “solution” why was the h only included in the context when I added a name for the match?

[Mario Carneiro]

that's what that syntax does

[Shreyas Srinivas]

No that syntax usually only introduces on equality that equates the matched variable to its arms

[Mario Carneiro]

it's not just a name for the match, match _: t is saying to have an equality in scope

[Shreyas Srinivas]

This time it introduced two equalities

[Mario Carneiro]

and you can't have that equality without the dependent equalities for the type in this case

[Shreyas Srinivas]

Oh right okay

[Shreyas Srinivas]

So at the point of the match lean was able to deduce the equality of types you suggested to Markus

[Shreyas Srinivas]

Oh not really. It was a different equality

[Mario Carneiro]

yes, it's also something you can do manually but it's a bit more complicated

[Mario Carneiro]

it's basically the same as:

def F {α β : Type _} (t : @Ty α β) : Unit := by
  generalize eq : t = t'; revert t'
  match t with
  | Ty.C1 f => intro t eq; sorry
  | Ty.C2 f => intro t eq; sorry

[Mario Carneiro]

with the dependent form it looks more like:

def F {α β : Type _} (t : @Ty α β) : Unit := by
  generalize h : β = β', eq : t = t'; revert eq
  match t with
  | Ty.C1 f => intro eq; sorry
  | Ty.C2 f => intro eq; sorry

[Shreyas Srinivas]

Mario Carneiro said:

with the dependent form it looks more like:

def F {α β : Type _} (t : @Ty α β) : Unit := by
  generalize h : β = β', eq : t = t'; revert eq
  match t with
  | Ty.C1 f => intro eq; sorry
  | Ty.C2 f => intro eq; sorry

This example seems the same as my last suggestion.

[Mario Carneiro]

yes that's the point, it's showing you what the match eq: t syntax is doing under the hood