mutual dependent injectivity

Stream: Is there code for X?

[Aaron Liu]

I have some mutual inductive types in my code, and I've defined some dependent functions with them, which are obviously injective. But proving they are injective was weirdly annoying and took ~50 lines. I'm wondering if there's an easier way.

universe u v

namespace Ex

inductive Object (ι : Type u) : Type u where
  | of (i : ι) : Object ι
  | unit : Object ι
  | prod (left right : Object ι) : Object ι
  | hom (source target : Object ι) : Object ι

mutual

inductive Normal {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | ofNeutral {ctx : List (Object ι)} {t : ι} (n : Neutral ζ ctx (.of t)) : Normal ζ ctx (.of t)
  | lam {ctx : List (Object ι)} (dom : Object ι) {tb : Object ι}
    (body : Normal ζ (dom :: ctx) tb) : Normal ζ ctx (.hom dom tb)
  | unit (ctx : List (Object ι)) : Normal ζ ctx .unit
  | prod {ctx : List (Object ι)} {tl tr : Object ι}
    (left : Normal ζ ctx tl) (right : Normal ζ ctx tr) : Normal ζ ctx (.prod tl tr)

inductive Neutral {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | of (k : κ) (ctx : List (Object ι)) : Neutral ζ ctx (ζ k)
  | app {ctx : List (Object ι)} {typed typea : Object ι}
    (fn : Neutral ζ ctx (.hom typed typea)) (arg : Normal ζ ctx typed) : Neutral ζ ctx typea
  | left {ctx : List (Object ι)} {tl tr : Object ι} (tup : Neutral ζ ctx (.prod tl tr)) :
    Neutral ζ ctx tl
  | right {ctx : List (Object ι)} {tl tr : Object ι} (tup : Neutral ζ ctx (.prod tl tr)) :
    Neutral ζ ctx tr
  | bvar {ctx : List (Object ι)} (n : Nat) (typ : Object ι) (sat : typ ∈ ctx[n]?) :
    Neutral ζ ctx typ

end

mutual

inductive Normalu {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | ofNeutral {ctx : List (Object ι)} {t : ι} (n : Neutralu ζ ctx (.of t)) : Normalu ζ ctx (.of t)
  | lam {ctx : List (Object ι)} (dom : Object ι) {tb : Object ι}
    (body : Normalu ζ (dom :: ctx) tb) : Normalu ζ ctx (.hom dom tb)

inductive Neutralu {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | of (k : κ) (ctx : List (Object ι)) : Neutralu ζ ctx (ζ k)
  | app {ctx : List (Object ι)} {typed typea : Object ι}
    (fn : Neutralu ζ ctx (.hom typed typea)) (arg : Normalu ζ ctx typed) : Neutralu ζ ctx typea
  | bvar {ctx : List (Object ι)} (n : Nat) (typ : Object ι) (sat : typ ∈ ctx[n]?) :
    Neutralu ζ ctx typ

end

mutual

def Normalu.toNormal {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (t : Normalu ζ ctx typ) : Normal ζ ctx typ :=
  match t with
  | .ofNeutral n => .ofNeutral n.toNeutral
  | .lam dom body => .lam dom body.toNormal

def Neutralu.toNeutral {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (t : Neutralu ζ ctx typ) : Neutral ζ ctx typ :=
  match t with
  | .of k ctx => .of k ctx
  | .app fn arg => .app fn.toNeutral arg.toNormal
  | .bvar n typ sat => .bvar n typ sat

end

-- want to prove: `Normalu.toNormal` and `Neutralu.toNeutral` are both `Function.Injective`

[Joachim Breitner]

What have you tried (induction, recursive theorems)? Why was it hard?

[Joachim Breitner]

And I assume the example is simplified? These functions look like the identity to me (at least on the phone )

[Kenny Lau]

Joachim Breitner said:

look like the identity

it's from xxxu to xxx, and xxxu seems to be simplified versions of xxx (with less constructors)

[Floris van Doorn]

You need that ζ is injective to prove this, right?

[Floris van Doorn]

Here is some code that works and is significantly less than 50 lines, but is very ugly:

attribute [simp] Normalu.toNormal Neutralu.toNeutral
open Function
mutual

theorem toNormal_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (hζ : Injective ζ) :
    Injective (Normalu.toNormal : Normalu ζ ctx typ → _)
  | .ofNeutral .., .ofNeutral .., hxy => by simp_all; exact toNeutral_inj hζ hxy
  | .lam .., .lam .., hxy => by simp_all; exact toNormal_inj hζ hxy

theorem toNeutral_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (hζ : Injective ζ) :
    Injective (Neutralu.toNeutral : Neutralu ζ ctx typ → _)
  | x, y, hxy => by
    cases x <;> try cases y <;> simp_all
    · rename_i k
      have : ∀ (u : Object ι) (h : u = ζ k) (y : Neutralu ζ ctx u),
         (Neutralu.of k ctx).toNeutral = (h ▸ y).toNeutral → Neutralu.of k ctx = h ▸ y := by
        intro u h y hy
        cases y <;> try cases h <;> simp_all
        cases hζ h
        cases h
        simp_all
      specialize this _ rfl y
      simp_all
    · cases hxy.1
      simp at *
      exact ⟨toNeutral_inj hζ hxy.1, toNormal_inj hζ hxy.2⟩

end

[Floris van Doorn]

(I'm not sure why Lean managed to figure out termination of this proof, but not of the proof where I did to_Normal_inj also in tactic mode. I expected I had to do both with pattern matching)

[Joachim Breitner]

Interesting that

theorem toNormal_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (hζ : Injective ζ) :
    Injective (Normalu.toNormal : Normalu ζ ctx typ → _)
  | .ofNeutral .., .ofNeutral .., hxy => by simp_all; exact toNeutral_inj hζ hxy
  | .lam .., .lam .., hxy => by simp_all; exact toNormal_inj hζ hxy

works but not

| .lam dom1 body₁, .lam dom2 body₂, hxy => by simp_all; exact toNormal_inj hζ hxy

does not. Ah, but

| .lam dom body₁, .lam .(dom) body₂, hxy => by simp_all; exact toNormal_inj hζ hxy

does! :bulb:

[Floris van Doorn]

Here a bit cleaner with pattern matching for both lemmas:

attribute [simp] Normalu.toNormal Neutralu.toNeutral
open Function
mutual

theorem toNormal_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (hζ : Injective ζ) :
    Injective (Normalu.toNormal : Normalu ζ ctx typ → _)
  | .ofNeutral .., .ofNeutral .., hxy => by simp_all; exact toNeutral_inj hζ hxy
  | .lam .., .lam .., hxy => by simp_all; exact toNormal_inj hζ hxy

theorem toNeutral_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (hζ : Injective ζ) :
    Injective (Neutralu.toNeutral : Neutralu ζ ctx typ → _)
  | .of k .., y, hxy => by
      have : ∀ (u : Object ι) (h : u = ζ k) (y : Neutralu ζ ctx u),
         (Neutralu.of k ctx).toNeutral = (h ▸ y).toNeutral → Neutralu.of k ctx = h ▸ y := by
        intro u h y hy
        cases y
        · cases hζ h
          simp_all
        all_goals { cases h; simp_all }
      specialize this _ rfl y
      simp_all
  | .app .., .app .., hxy => by
    simp_all; cases hxy.1; simp_all; exact ⟨toNeutral_inj hζ hxy.1, toNormal_inj hζ hxy.2⟩
  | .bvar .., .bvar .., _ => by simp_all

end

[Floris van Doorn]

It would be nice if there is a tactic that does the have automatically: generalize ζ k to a new variable u and insert casts (or in complicated cases, Eq.rec) to ensure that the rest of the context is still well-typed).

[Joachim Breitner]

I was playing around with a variant of generalizing toNeutral_inj like this:

theorem toNeutral_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ₁ typ₂ : Object ι} (hζ : Injective ζ) : (ht : typ₁ = typ₂) →
    {t₁ : Neutralu ζ ctx typ₁} → {t₂ : Neutralu ζ ctx typ₂} → (ht ▸ t₁.toNeutral = t₂.toNeutral) → ht ▸ t₁ = t₂
  | ht, .of .., .of .., _ => by specialize hζ ht; cases hζ; dsimp
  | ht, .app fn₁ arg₁, .app fn₂ arg₂, heq => by
    cases ht
    simp_all
    cases heq.1
    simp_all
    have := toNeutral_inj hζ rfl heq.1
    have := toNormal_inj hζ heq.2
    simp_all
  | ht, .bvar .., .bvar .., heq => by
    cases ht
    simp_all

and the .of case works well, but in this way the pattern match compilation does not recognize that only the diagonal is reachable. (and the termination checker isn't happy)

[Aaron Liu]

Floris van Doorn said:

You need that ζ is injective to prove this, right?

No you don't I proved it without assuming anything about ζ

[Aaron Liu]

but it's 50 lines I want something shorter

[Aaron Liu]

Joachim Breitner said:

And I assume the example is simplified? These functions look like the identity to me (at least on the phone )

No this is directly extracted from my code (hence why I said it was obvious but weirdly annoying)

[Aaron Liu]

I can show you my proof if you want

[Aaron Liu]

My Proof

import Mathlib

universe u v

namespace Ex

inductive Object (ι : Type u) : Type u where
  | of (i : ι) : Object ι
  | unit : Object ι
  | prod (left right : Object ι) : Object ι
  | hom (source target : Object ι) : Object ι

mutual

inductive Normal {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | ofNeutral {ctx : List (Object ι)} {t : ι} (n : Neutral ζ ctx (.of t)) : Normal ζ ctx (.of t)
  | lam {ctx : List (Object ι)} (dom : Object ι) {tb : Object ι}
    (body : Normal ζ (dom :: ctx) tb) : Normal ζ ctx (.hom dom tb)
  | unit (ctx : List (Object ι)) : Normal ζ ctx .unit
  | prod {ctx : List (Object ι)} {tl tr : Object ι}
    (left : Normal ζ ctx tl) (right : Normal ζ ctx tr) : Normal ζ ctx (.prod tl tr)

inductive Neutral {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | of (k : κ) (ctx : List (Object ι)) : Neutral ζ ctx (ζ k)
  | app {ctx : List (Object ι)} {typed typea : Object ι}
    (fn : Neutral ζ ctx (.hom typed typea)) (arg : Normal ζ ctx typed) : Neutral ζ ctx typea
  | left {ctx : List (Object ι)} {tl tr : Object ι} (tup : Neutral ζ ctx (.prod tl tr)) :
    Neutral ζ ctx tl
  | right {ctx : List (Object ι)} {tl tr : Object ι} (tup : Neutral ζ ctx (.prod tl tr)) :
    Neutral ζ ctx tr
  | bvar {ctx : List (Object ι)} (n : Nat) (typ : Object ι) (sat : typ ∈ ctx[n]?) :
    Neutral ζ ctx typ

end

mutual

inductive Normalu {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | ofNeutral {ctx : List (Object ι)} {t : ι} (n : Neutralu ζ ctx (.of t)) : Normalu ζ ctx (.of t)
  | lam {ctx : List (Object ι)} (dom : Object ι) {tb : Object ι}
    (body : Normalu ζ (dom :: ctx) tb) : Normalu ζ ctx (.hom dom tb)

inductive Neutralu {ι : Type u} {κ : Type v} (ζ : κ → Object ι) :
    (ctx : List (Object ι)) → (typ : Object ι) → Type (max u v) where
  | of (k : κ) (ctx : List (Object ι)) : Neutralu ζ ctx (ζ k)
  | app {ctx : List (Object ι)} {typed typea : Object ι}
    (fn : Neutralu ζ ctx (.hom typed typea)) (arg : Normalu ζ ctx typed) : Neutralu ζ ctx typea
  | bvar {ctx : List (Object ι)} (n : Nat) (typ : Object ι) (sat : typ ∈ ctx[n]?) :
    Neutralu ζ ctx typ

end

mutual

def Normalu.toNormal {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (t : Normalu ζ ctx typ) : Normal ζ ctx typ :=
  match t with
  | .ofNeutral n => .ofNeutral n.toNeutral
  | .lam dom body => .lam dom body.toNormal

def Neutralu.toNeutral {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} (t : Neutralu ζ ctx typ) : Neutral ζ ctx typ :=
  match t with
  | .of k ctx => .of k ctx
  | .app fn arg => .app fn.toNeutral arg.toNormal
  | .bvar n typ sat => .bvar n typ sat

end

mutual

theorem Normalu.toNormal_injective {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} : (@Normalu.toNormal ι κ ζ ctx typ).Injective :=
  fun a b hab =>
    match a, b with
    | .ofNeutral _, .ofNeutral _ =>
      congrArg Normalu.ofNeutral (Neutralu.toNeutral_injective (Normal.ofNeutral.inj hab))
    | .lam _ _, .lam _ _ =>
      congrArg (Normalu.lam _) (Normalu.toNormal_injective (Normal.lam.inj hab))

theorem Neutralu.toNeutral_injective {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} : (@Neutralu.toNeutral ι κ ζ ctx typ).Injective :=
  fun a b hab =>
    match typ, a with
    | _, .of k₁ _=>
        @id (∀ (t : Object ι) (ht : ζ k₁ = t) (b : Neutralu ζ ctx t)
          (hb : ht ▸ Neutral.of k₁ ctx = b.toNeutral),
          Neutralu.of k₁ ctx = ht ▸ b) (fun t ht b hb =>
            match t, b with
            | _, .of k₂ _ => by
              let f {ctx : List (Object ι)} {typ : Object ι} (t : Neutral ζ ctx typ) : Option κ :=
                Neutral.rec
                  (motive_1 := fun _ _ _ => PUnit)
                  (motive_2 := fun _ _ _ => Option κ)
                  (ofNeutral := fun _ _ => .unit)
                  (lam := fun _ _ _ _ => .unit)
                  (unit := fun _ => .unit)
                  (prod := fun _ _ _ _ => .unit)
                  (of := fun k _ => some k)
                  (app := fun _ _ _ _ => none)
                  (left := fun _ _ => none)
                  (right := fun _ _ => none)
                  (bvar := fun _ _ _ => none) t
              have hf := congrArg f hb
              change _ = some k₂ at hf
              rewrite! [← ht] at hf
              cases hf
              rfl
            | _, .bvar _ _ _
            | _, .app _ _ => by cases ht; exact Neutral.noConfusion hb
          ) (ζ k₁) rfl b hab
    | _, .bvar n _ _ =>
      match b with
      | .bvar _ _ _ => by cases hab; rfl
    | _, .app _ _ =>
      match b with
      | .app _ _ => by
        cases (Neutral.app.inj hab).1
        exact congr (congrArg Neutralu.app
          (Neutralu.toNeutral_injective (Neutral.app.inj hab).2.1.eq))
          (Normalu.toNormal_injective (Neutral.app.inj hab).2.2.eq)

end

[Aaron Liu]

In my case having ζ be injective is actually really restrictive, it amounts to saying that you can't have two free variables of the same type, so it really doesn't work require ζ to be injective.

[Floris van Doorn]

Nice technique to not require injectivity of zeta. And I didn't know about rw!, that a significant part of the tactic I was requesting.

Here is your proof written in my style:

import Mathlib.Tactic

-- <first code snippet>

attribute [simp] Normalu.toNormal Neutralu.toNeutral
open Function

def Neutral.aux {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} : Neutral ζ ctx typ → Option κ
  | .of k ctx => some k
  | _ => none

@[simp] lemma Neutral.aux_of {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {k : κ} : Neutral.aux (ζ := ζ) (.of k ctx) = some k := rfl

mutual

theorem toNormal_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} :
    Injective (Normalu.toNormal : Normalu ζ ctx typ → _)
  | .ofNeutral .., .ofNeutral .., hxy => by simp_all; exact toNeutral_inj hxy
  | .lam .., .lam .., hxy => by simp_all; exact toNormal_inj hxy

theorem toNeutral_inj {ι : Type u} {κ : Type v} {ζ : κ → Object ι}
    {ctx : List (Object ι)} {typ : Object ι} :
    Injective (Neutralu.toNeutral : Neutralu ζ ctx typ → _)
  | .of k .., y, hxy => by
      -- The first four lines are basically "`generalize h : ζ k = u` but try harder".
      obtain ⟨u, hu⟩ : ∃ u, ζ k = u := ⟨_, rfl⟩
      revert y
      rw! (castMode := .all) [hu]
      intro y hy
      cases y
      · apply_fun Neutral.aux at hy
        simp at hy
        rewrite! [← hu] at hy
        cases hy
        rfl
      all_goals { subst hu; simp_all }
  | .app .., .app .., hxy => by
    simp_all; cases hxy.1; simp_all; exact ⟨toNeutral_inj hxy.1, toNormal_inj hxy.2⟩
  | .bvar .., .bvar .., _ => by simp_all

end

(EDIT: simplified)

[Aaron Liu]

Currently rw! is in a half-broken state (it works, but can make your goals look ugly (if it does make stuff ugly, dsimp should clear it up)) so I would just use rewrite! for now until I get around to fixing rw!