declaring instances for mutually inductive types

Stream: new members

[Kris Brown]

I'm modeling a programming language with datatypes, and to capture the notion of a structure which itself has fields I wrote the following

  mutual inductive PrimType, Struct
  with PrimType : Type
   | pInt : nat  → PrimType
   | pStr : string  → PrimType
   | pBool: bool → PrimType
   | pStruct {s: string}: Struct s → PrimType

  with Struct : string → Type
   | mk (name: string) (fields : list (string × PrimType))
          : Struct name
   | nil (name: string) : Struct name

Lean can't derive decidable_eq for this pair. Here's a more minimal example:

mutual inductive A,B
with A: Type
 | a1 : ℕ → A
 | a2 : B → A
with B:  Type
 | b1 (a:A): B

I think it's possible to define decidable equality for the pair, but I don't know how to do this syntactically. I've only ever seen declaring an instance for a single type at a time, whereas the only way I can define equality for A is to define it for B at the same time. How would I do this?

[Reid Barton]

I don't know whether there is syntax to write mutually recursive instances directly, but you can just write mutually recursive defs and then mark them as instances with attribute [instance].

[Kris Brown]

Thanks, that makes sense! I've made some progress, but hit two roadblocks

variables {p q : Prop}

instance and_eq [decidable p] [decidable q] : decidable (p ∧ q) :=
    if hp : p then
    if hq : q then is_true ⟨hp, hq⟩
    else is_false (assume h : p ∧ q, hq (and.right h))
    else is_false (assume h : p ∧ q, hp (and.left h))

mutual def P_eq, S_eq
with P_eq : decidable_eq PrimType
    | (pInt _)       (pBool _)      := by {simp only [], exact decidable.false}
    | (pInt _)       (pStr _)       := by {simp only [], exact decidable.false}
    | (pInt _)       (pStruct _)    := by {simp only [], exact decidable.false}
    | (pBool _)      (pInt _)       := by {simp only [], exact decidable.false}
    | (pBool _)      (pStr _)       := by {simp only [], exact decidable.false}
    | (pBool _)      (pStruct _)    := by {simp only [], exact decidable.false}
    | (pStr _)       (pInt _)       := by {simp only [], exact decidable.false}
    | (pStr _)       (pBool _)      := by {simp only [], exact decidable.false}
    | (pStr _)       (pStruct _)    := by {simp only [], exact decidable.false}
    | (pStruct _)    (pInt _)       := by {simp only [], exact decidable.false}
    | (pStruct _)    (pStr _)       := by {simp only [], exact decidable.false}
    | (pStruct _)    (pBool _)      := by {simp only [], exact decidable.false}
    | (pInt x)       (pInt y)       := by {simp only [], exact nat.decidable_eq x y}
    | (pBool x)      (pBool y)      := by {simp only [], exact bool.decidable_eq x y}
    | (pStr x)       (pStr y)       := by {simp only [], exact string.has_decidable_eq x y}
    | (@pStruct n x) (@pStruct m y) := by {simp only [],
        have p: decidable (n=m), by exact string.has_decidable_eq n m,
        have q: decidable (heq x y), by {
            have h: (n=m ∨ ¬ n = m), from @decidable.em (n=m) p,
            exact or.elim h _ _ -- this can only prove a Prop, not decidable (...)
            },
        exact @and_eq (n=m) (heq x y) p q
        }

with S_eq : Π{s: string}, decidable_eq (Struct s)
    | _ (Struct.mk _ _) (Struct.nil _) := by {simp only [], exact decidable.false}
    | _ (Struct.nil _)  (Struct.mk _ _) := by {simp only [], exact decidable.false}
    | _ (Struct.mk _ x) (Struct.mk _ y) := by {simp only [],
        have h: decidable_eq (string × PrimType), by {exact @prod.decidable_eq string PrimType string.has_decidable_eq P_eq},
        exact @list.decidable_eq (string × PrimType) h x y}
    | _ (Struct.nil _) (Struct.nil _) := by {simp only [], exact decidable.true}
--using_well_founded {rel_tac := λ _ _, _}

I'm a bit unsure how to go about proving that the recursion is well- founded here, even after looking at https://leanprover-community.github.io/extras/well_founded_recursion.html (lean cannot determine this for P_eq ).

Also there's one sorry at the end of P_eq because I'm stuck trying to prove decidability of heterogenous equality for the first time (decidable (Struct n = Struct m)). I thought I could case split on n=m but this doesn't work since or.elim can only prove another Prop from a disjunction.

[Kris Brown]

I also had to copypaste the and_eq from mathlib because that instance didn't have a name, so I didn't know how to refer to it in the proof otherwise. Not sure if there's a workaround for that.

[Floris van Doorn]

You can run #print instances decidable to see a (long) list of all its instances.

[Mario Carneiro]

@Kris Brown All instances have names. If they are not specified, their names are automatically generated from the statement, where A (B x) gets the name B.A

[Floris van Doorn]

Also, here is a problem to your or problem: use cases p.

@[simp] def heq_iff_eq {α} (x y : α) : x == y ↔ x = y :=
⟨eq_of_heq, heq_of_eq⟩

mutual def P_eq, S_eq
with P_eq : decidable_eq PrimType
    | (pInt _)       (pBool _)      := by {simp only, apply_instance}
    | (pInt _)       (pStr _)       := by {simp only, apply_instance}
    | (pInt _)       (pStruct _)    := by {simp only, apply_instance}
    | (pBool _)      (pInt _)       := by {simp only, apply_instance}
    | (pBool _)      (pStr _)       := by {simp only, apply_instance}
    | (pBool _)      (pStruct _)    := by {simp only, apply_instance}
    | (pStr _)       (pInt _)       := by {simp only, apply_instance}
    | (pStr _)       (pBool _)      := by {simp only, apply_instance}
    | (pStr _)       (pStruct _)    := by {simp only, apply_instance}
    | (pStruct _)    (pInt _)       := by {simp only, apply_instance}
    | (pStruct _)    (pStr _)       := by {simp only, apply_instance}
    | (pStruct _)    (pBool _)      := by {simp only, apply_instance}
    | (pInt x)       (pInt y)       := by {simp only, apply_instance}
    | (pBool x)      (pBool y)      := by {simp only, apply_instance}
    | (pStr x)       (pStr y)       := by {simp only, apply_instance}
    | (@pStruct n x) (@pStruct m y) := by {simp only,
        have p: decidable (n=m), by exact string.has_decidable_eq n m,
        cases p; simp [p], apply_instance, subst p,
        rw [heq_iff_eq], apply S_eq,
        }

with S_eq : Π{s: string}, decidable_eq (Struct s)
    | _ (Struct.mk _ _) (Struct.nil _) := by {simp only [], exact decidable.false}
    | _ (Struct.nil _)  (Struct.mk _ _) := by {simp only [], exact decidable.false}
    | _ (Struct.mk _ x) (Struct.mk _ y) := by {simp only [],
        have h: decidable_eq (string × PrimType), by {exact @prod.decidable_eq string PrimType string.has_decidable_eq P_eq},
        exact @list.decidable_eq (string × PrimType) h x y}
    | _ (Struct.nil _) (Struct.nil _) := by {simp only [], exact decidable.true}

[Floris van Doorn]

using_well_founded still scares me. You can try to mimic src#lists.equiv.decidable

[Kris Brown]

That example is scary. I'll make a post focused on this in #general.