No confusion puzzle

Stream: general

[Andrew Yang]

Does anyone have a proof to this?

axiom F : Nat → Nat

inductive Foo : Nat → Type
  | foo n : Foo (F n)

example (a b : Nat) (hab : F a = F b) (hab' : a ≠ b) :
    Foo.foo a ≠ hab ▸ Foo.foo b := by sorry

[Andrew Yang]

And level two (which should have more or less the same proof and is the case that I need)

axiom F : Nat → Nat

inductive Foo : Nat → Type
  | foo n : Foo (F n)
  | bar n : Foo (F n)

example (a b : Nat) (hab : F a = F b) : Foo.foo a ≠ hab ▸ Foo.bar b := by sorry

[Markus Himmel]

Here is one way for the first one:

axiom F : Nat → Nat

inductive Foo : Nat → Type
  | foo n : Foo (F n)

def Foo.out {n} : Foo n → Nat
  | Foo.foo k => k

@[simp]
theorem Foo.out_mk {n} : (Foo.foo n).out = n := rfl

@[simp]
theorem Foo.out_cast {n m} (h : n = m) (f : Foo n) : (h ▸ f).out = f.out :=
  by cases h; rfl

example (a b : Nat) (hab : F a = F b) (hab' : a ≠ b) :
    Foo.foo a ≠ hab ▸ Foo.foo b := by
  apply ne_of_apply_ne Foo.out
  simpa using hab'

[Markus Himmel]

The second one works the same way:

axiom F : Nat → Nat

inductive Foo : Nat → Type
  | foo n : Foo (F n)
  | bar n : Foo (F n)

inductive Bar : Type
  | foo (n : Nat) : Bar
  | bar (n : Nat) : Bar

def Foo.out {n} : Foo n → Bar
  | .foo n => .foo n
  | .bar n => .bar n

@[simp] theorem Foo.out_foo {n} : (Foo.foo n).out = .foo n := rfl
@[simp] theorem Foo.out_bar {n} : (Foo.bar n).out = .bar n := rfl
@[simp] theorem Foo.out_cast {n m} (h : n = m) (f : Foo n) : (h ▸ f).out = f.out := by cases h; rfl

example (a b : Nat) (hab : F a = F b) : Foo.foo a ≠ hab ▸ Foo.bar b := by
  apply ne_of_apply_ne Foo.out
  simp

[Andrew Yang]

Great! (I originally tried a bijection with inductive Foo2 : Nat → Type | foo a b (h : F a = b) : Foo2 b which works but is much more messy)
Is there a good way to achieve this without auxiliary defs? Or for every inductive type with inductive indices I need to define such an auxiliary inductive type to get the no-confusion lemmas?

[Edward van de Meent]

personally i'd try to avoid this kind of inductive... For example, you might be happier using inductive Bar where | foo n : Foo | bar n : Foo, to then work with the subtype Foo x := {b : Bar| F b.out = x}. When you need to rewrite , use a cast function, such that the rewrites are cleaner and part of the object, as well as in a way that the kernel gets to forget when trying to match on the actual value.

[Edward van de Meent]

for a concrete usecase of this pattern, check out docs#List.Vector

[Andrew Yang]

The inductive in question is docs#CategoryTheory.Limits.WalkingMulticospan.Hom . And because it is constructing arrows in a category it needs to have type WalkingMulticospan fst snd → WalkingMulticospan fst snd → Type _

[Edward van de Meent]

i think strictly speaking my suggestion still works? the only thing i imagine people might take issue with is the fact that it mentions object equality, but i'm not a category theorist