rfl won't work with indexed inductive types

Stream: lean4

[Jad Ghalayini]

Anyone know what I'm doing wrong here: https://github.com/leanprover/lean4/issues/837?

I ended up working around this by replacing Wk with a struct containing a RawWk and a Prop, but I still wonder what's wrong.

[Arthur Paulino]

Some more digging:

inductive Wk: Nat -> Nat -> Type 0 where
  | id: Wk n n
  | step: Wk m n -> Wk (Nat.succ m) n
  | lift: Wk m n -> Wk (Nat.succ m) (Nat.succ n)

def wk_comp {n m l: Nat} (ρ: Wk n m) (σ: Wk m l): Wk n l :=
  match ρ, σ with
    | Wk.id, σ => σ
    | Wk.step ρ, σ => Wk.step (wk_comp ρ σ)
    | Wk.lift ρ, Wk.id => Wk.lift ρ
    | Wk.lift ρ, Wk.step σ => Wk.step (wk_comp ρ σ)
    | Wk.lift ρ, Wk.lift σ => Wk.lift (wk_comp ρ σ)

variable {ρ: Wk m n}
-- they indeed match:
#check ρ                             -- ρ : Wk m n
#check wk_comp Wk.id ρ -- wk_comp Wk.id ρ : Wk m n

theorem wk_comp_id_id' {ρ: Wk m n}: wk_comp Wk.id ρ = ρ := by
-- (kernel) declaration type mismatch, 'wk_comp_id_id'' has type
--  ∀ {m n : Nat} {ρ : Wk m n}, ρ = ρ but it is expected to have type
--  ∀ {m n : Nat} {ρ : Wk m n}, wk_comp Wk.id ρ = ρ
  simp only [wk_comp]; -- goals accomplished

theorem wk_comp_id_id {ρ: Wk m n}: wk_comp Wk.id ρ = ρ := by
  sorry
  simp only [wk_comp]; -- error: no goals to be solved

[Arthur Paulino]

@Jad Ghalayini This works:

inductive Wk: Nat -> Nat -> Type 0 where
  | id: Wk n n
  | step: Wk m n -> Wk (Nat.succ m) n
  | lift: Wk m n -> Wk (Nat.succ m) (Nat.succ n)

variable {n m l: Nat}

def wk_comp (ρ: Wk n m) (σ: Wk m l): Wk n l :=
  match ρ, σ with
    | Wk.id, σ => σ
    | Wk.step ρ, σ => sorry -- Wk.step (wk_comp ρ σ)
    | Wk.lift ρ, Wk.id => sorry -- Wk.lift ρ
    | Wk.lift ρ, Wk.step σ => sorry -- Wk.step (wk_comp ρ σ)
    | Wk.lift ρ, Wk.lift σ => sorry -- Wk.lift (wk_comp ρ σ)

theorem wk_comp_id_id' {ρ: Wk m n}: wk_comp Wk.id ρ = ρ := rfl

I just used sorry on the match possibilities that weren't being used. The trick was fixing variable {n m l: Nat} instead of having those as implicit arguments of the function

[Kyle Miller]

@Jad Ghalayini This has exactly the same problem, but I wanted to mention that you can use this syntax (implicit implicit arguments and folding in the match notation):

def wk_comp : Wk n m → Wk m l → Wk n l
  | Wk.id, σ => σ
  | Wk.step ρ, σ => Wk.step (wk_comp ρ σ)
  | Wk.lift ρ, Wk.id => Wk.lift ρ
  | Wk.lift ρ, Wk.step σ => Wk.step (wk_comp ρ σ)
  | Wk.lift ρ, Wk.lift σ => Wk.lift (wk_comp ρ σ)

[Kyle Miller]

@Arthur Paulino If you sorry-out the cases in the original version the declaration type mismatch goes away, too, so variable is probably not what's seeming to fix it.

[Arthur Paulino]

(deleted)

[Arthur Paulino]

It's not just any sorry pattern either. It works as long as you sorry-out these three:

def wk_comp : Wk n m → Wk m l → Wk n l
  | Wk.id, σ => σ
  | Wk.step ρ, σ => sorry -- Wk.step (wk_comp ρ σ)
  | Wk.lift ρ, Wk.id => Wk.lift ρ
  | Wk.lift ρ, Wk.step σ => sorry -- Wk.step (wk_comp ρ σ)
  | Wk.lift ρ, Wk.lift σ => sorry -- Wk.lift (wk_comp ρ σ)

[Arthur Paulino]

(deleted)

[Arthur Paulino]

(the recursive calls)

[Jad Ghalayini]

I can post how I fixed it tomorrow if you guys want, but I do think something is quite broken here

[Leonardo de Moura]

Pushed a fix for this: https://github.com/leanprover/lean4/commit/c42196440f6346298b85891a35053dd94ca95a02