Puzzle: Decidable HEq

Stream: lean4

[Joachim Breitner]

Idle experimentation; I was exploring types for lean fails to derive DecidableEq and noticed that it cannot handle types with indices where the constructor parameters are not determined by the indices. I was wondering if this is a fundamental issue, or if it would be possible to generalize to DecidableHEq and then make it go through, but I couldn't quite close the goal. MWE might be

opaque f : Nat → Nat
inductive I : (n : Nat) → Type where
  | mk n : I (f n)

def instDecidableHEqI {n m} (x : I n) (y : I m) : Decidable (HEq x y) :=
  match x, y with
  | I.mk n1, I.mk n2 =>
    if h : n1 = n2 then
      by subst h; exact isTrue HEq.rfl
    else
      isFalse <| by
        sorry

Can I make progress here, or is this doomed?

[Robin Arnez]

Nah, you can't, there's a counterexample:

def f : Nat → Nat := fun x => x % 2

def I (n : Nat) : Type :=
  match n with
  | 0 => Nat
  | 1 => Nat
  | _ + 2 => Empty

def I.mk0 (n : Nat) : I 0 := n
def I.mk1 (n : Nat) : I 1 := n

def I.val0 (n : I 0) : Nat := n
def I.val1 (n : I 1) : Nat := n

def I.mk (n : Nat) : I (f n) :=
  match hf : f n with
  | 0 => n / 2
  | 1 => n / 2
  | _ + 2 => False.elim (by grind [f])

@[elab_as_elim, induction_eliminator]
def I.rec.{u_1} {motive : (n : Nat) → (t : I n) → Sort u_1}
    (mk : ∀ n, motive (f n) (I.mk n)) {n : Nat} (t : I n) :
    motive n t :=
  match n with
  | 0 => cast ?_ (mk ((show Nat from t) * 2))
  | 1 => cast ?_ (mk ((show Nat from t) * 2 + 1))
  | _ + 2 => t.elim
where finally
  · simp only [f, I.mk, Nat.succ_eq_add_one]
    congr
    · simp
    · refine HEq.trans (I.mk.match_1.congr_eq_1 (heq_1 := Nat.mul_mod_left t 2) ..) ?_
      rw [Nat.mul_div_cancel _ (by decide)]
  · simp only [f, I.mk, Nat.succ_eq_add_one]
    congr
    · simp
    · refine HEq.trans (I.mk.match_1.congr_eq_2 (heq_1 := ?_) ..) ?_
      · simp
      · grind

theorem I.rec_mk {motive : (n : Nat) → (t : I n) → Sort u_1}
    (mk : ∀ n, motive (f n) (I.mk n)) (n : Nat) :
    I.rec (motive := motive) mk (I.mk n) = mk n := by
  simp only [I.mk, Nat.succ_eq_add_one, rec, f]
  rcases Nat.mod_two_eq_zero_or_one n with hn | hn <;> grind

example : ∃ (n1 n2 : Nat), I.mk n1 ≍ I.mk n2 ∧ n1 ≠ n2 := by
  exists 0, 1

[Damiano Testa]

Is this really a counterexample, or is it simply showing that you cannot deduce isFalse when n1 and n2 are different?

[Joachim Breitner]

That's not my inductive I :-).

[Robin Arnez]

Well, it is a counterexample in the sense that it tells you that there is a model of Lean where I is defined in such a way that the isFalse branch is false

[Arthur Adjedj]

Joachim Breitner said:

Can I make progress here, or is this doomed?

Because type constructors are (in most cases) not injective, it is in general not possible to prove that two constructor of an inductive family with distinct indices are not equal, e.g for the following type, ¬ foo ≍ bar is not provable.

inductive Foo : Nat → Type
  | foo : Foo 1
  | bar : Foo 2

[Arthur Adjedj]

This issue also appears in your case, since I.mk n1 and I.mk n2 have distinct types/indices. I would say that this is probably doomed.

[Robin Arnez]

I will mention though that I actually tried something similar some time ago, but with the necessary equalities:

opaque f : Nat → Nat

inductive I : (n : Nat) → Type where
  | mk n : I (f n)

@[elab_as_elim]
abbrev HEq.recEq.{u_1, u} {α : Sort u} {a : α} {motive : (b : α) → (t : a ≍ b) → Sort u_1}
    (refl : motive a (HEq.refl a)) {b : α} (t : a ≍ b) : motive b t :=
  @Eq.rec α a (fun b t => motive b (heq_of_eq t)) refl b (eq_of_heq t)

def I.noConfusionHEqType (P : Sort u) (a : I m) (b : I n) : Sort u :=
  a.casesOn fun n1 => b.casesOn fun n2 => (n1 = n2 → P) → P

def I.noConfusionHEq {P : Sort u} {m : Nat} {a : I m} :
    {n : Nat} → (h₁ : m = n) → {b : I n} → (h₂ : a ≍ b) → I.noConfusionHEqType P a b :=
  Eq.rec (HEq.recEq (a.casesOn fun _ h => h rfl))

def I.decHEq {n m} (hnm : n = m) (x : I n) (y : I m) : Decidable (HEq x y) :=
  match x, y with
  | I.mk n1, I.mk n2 =>
    if h : n1 = n2 then
      by subst h; exact isTrue HEq.rfl
    else
      isFalse (fun heq => I.noConfusionHEq hnm heq h)

instance : DecidableEq (I n) := fun _ _ =>
  haveI := I.decHEq (rfl : n = n)
  decidable_of_decidable_of_iff ⟨eq_of_heq, heq_of_eq⟩

[Joachim Breitner]

Robin Arnez schrieb:

Well, it is a counterexample in the sense that it tells you that there is a model of Lean where I is defined in such a way that the isFalse branch is false

Ah, ok, I was too quick to complain. You define constructors and a recursor, so if it would work for the normal indictive it would work for yours as well. Thanks!

(Still a bit surprising if I think of it as just data)

[Robin Arnez]

I just realized that I did it way more complicated than it had to be:

def f : Nat → Nat := id
def I (n : Nat) := Unit
def I.mk (n : Nat) : I n := ()
def I.rec {motive : (n : Nat) → (t : I n) → Sort u_1}
    (mk : ∀ n, motive n (I.mk n)) {n : Nat} (t : I n) : motive n t := mk n
theorem I.rec_mk {motive : (n : Nat) → (t : I n) → Sort u_1}
    (mk : ∀ n, motive n (I.mk n)) (n : Nat) : I.rec (motive := motive) mk (I.mk n) = mk n := rfl

[Kyle Miller]

When I've run into this issue before (decidable equality for inductive types with complicated indices), one trick is to first create an auxiliary decidable equality function that also takes in index equality proofs, then call it with rfl in the instance. The index equalities are passed to the match to generalize them; using rfl for the pattern gets match to do dependent elimination (if that works), and otherwise you can either simulate dependent elimination yourself, if you happen to know some extra facts about the type, or you can define some projection functions that give the constructor fields, which somehow helps as a technique to prove that the field disequality gives a contradiction, because it enables a congruence argument.

I think the general idea is you imagine defining a type I' that doesn't have indices, define a function from I to I' that forgets indices, define decidable equality on I', then pull it back to I. You lose the sub-quadratic case analysis this way, but possibly you can recover it by using constructor indices somehow (indices in the nth constructor sense).

import Mathlib.Tactic

opaque f : Nat → Nat
inductive I : (n : Nat) → Type where
  | mk n : I (f n)

def I.decEqAux {n m} (x : I n) (y : I m) (h1 : n = m) :
    Decidable (x ≍ y) :=
  match x, y, h1 with
  | I.mk n1, I.mk n2, h1 =>
    if h : n1 = n2 then
      isTrue <| by subst h; exact HEq.rfl
    else
      isFalse <| by
        intro h'
        let getVal : {n : Nat} → (x : I n) → Nat := fun x => match x with | .mk n => n
        have : getVal (mk n1) = getVal (mk n2) := by
          refine congr_heq ?_ h'
          exact congr_arg_heq _ h1
        exact h this

instance {n} : DecidableEq (I n) := fun x y =>
  @decidable_of_iff _ (x ≍ y) heq_iff_eq (I.decEqAux x y rfl)

[Kyle Miller]

Here's a more complicated example with multiple constructors, to show the general design pattern. The ctorIdx does end up working as a way to limit it to a linear number of cases.

import Mathlib.Tactic

opaque f : Nat → Nat
inductive I : (n : Nat) → Type where
  | mk n : I (f n)
  | mk' (a : Nat) (z : I a) : I (2 * a)

def I.ctorIdx {n} : I n → Nat
  | .mk .. => 0
  | .mk' .. => 1

def I.mk_n {n} (x : I n) (h : x.ctorIdx = 0) : Nat :=
  match x, h with
  | .mk n, _ => n
def I.mk'_a {n} (x : I n) (h : x.ctorIdx = 1) : Nat :=
  match x, h with
  | .mk' a _, _ => a
def I.mk'_z {n} (x : I n) (h : x.ctorIdx = 1) : I (I.mk'_a x h) :=
  match x, h with
  | .mk' _ z, _ => z

def I.decEqAux {n m} (x : I n) (y : I m) (h1 : n = m) :
    Decidable (x ≍ y) :=
  if hidx : x.ctorIdx = y.ctorIdx then
    match x, y, hidx, h1 with
    | I.mk n1, I.mk n2, _, h1 =>
      if h : n1 = n2 then
        isTrue <| by subst h; exact HEq.rfl
      else
        isFalse <| by
          intro h'
          have : (mk n1).mk_n rfl = (mk n2).mk_n rfl := by
            congr
          exact h this
    | I.mk' a1 z1, I.mk' a2 z2, _, h1 =>
      if ha : a1 = a2 then
        match I.decEqAux z1 z2 ha with
        | isTrue hz => isTrue <| by subst_vars; rfl
        | isFalse hz => isFalse <| by
          intro h'
          have : (mk' a1 z1).mk'_z rfl ≍ (mk' a2 z2).mk'_z rfl := by
            congr
          exact hz this
      else
        isFalse <| by
          intro h'
          have : (mk' a1 z1).mk'_a rfl = (mk' a2 z2).mk'_a rfl := by
            congr
          exact ha this
  else
    isFalse <| by
      intro h
      subst_vars
      contradiction

instance {n} : DecidableEq (I n) := fun x y =>
  @decidable_of_iff _ (x ≍ y) heq_iff_eq (I.decEqAux x y rfl)

[Kyle Miller]

The IR for this is reasonable too.

    def I.decEqAux._redArg (x_1 : @& obj) (x_2 : @& obj) : u8 :=
      let x_3 : tobj := I.ctorIdx._redArg x_1;
      let x_4 : tobj := I.ctorIdx._redArg x_2;
      let x_5 : u8 := Nat.decEq x_3 x_4;
      dec x_4;
      dec x_3;
      case x_5 : u8 of
      Bool.false →
        ret x_5
      Bool.true →
        case x_1 : obj of
        I.mk →
          let x_6 : tobj := proj[0] x_1;
          let x_7 : tobj := proj[0] x_2;
          let x_8 : u8 := Nat.decEq x_6 x_7;
          ret x_8
        I.mk' →
          let x_9 : tobj := proj[0] x_1;
          let x_10 : obj := proj[1] x_1;
          let x_11 : tobj := proj[0] x_2;
          let x_12 : obj := proj[1] x_2;
          let x_13 : u8 := Nat.decEq x_9 x_11;
          case x_13 : u8 of
          Bool.false →
            ret x_13
          Bool.true →
            let x_14 : u8 := I.decEqAux._redArg x_10 x_12;
            ret x_14

[Joachim Breitner]

That’s clever! It’s not an itch that I feel like I need to scratch at the moment, but I’ll try to keep it in mind if we ever have user-demand for deriving DecidableEq for such types.

[Aaron Liu]

I recently had to do the decidable heq trick on some of my types

[Aaron Liu]

there was one really annoying case