Recursive membership instance

Stream: new members

[aron]

Is it possible to define an instance of Membership recursively? I can't figure out how to do this for the below code. I can't define it directly in the Membership.mem instance because it's recursive, but I also can't do it in a separate function first because I want to rely on the Membership instance of List. How can I implement my instance correctly?

I also can't seem to automatically derive a DecidableEq instance for ZonkedSimpleType for some reason.

inductive Primitive
  | int
  | string

inductive TypeVar
  | typeVar


mutual

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

  deriving DecidableEq

structure ZonkedPolyType where
  typeVars : List TypeVar
  type : ZonkedSimpleType

  deriving DecidableEq


inductive ZonkedPolyOrMonoType where
  | poly : ZonkedPolyType → ZonkedPolyOrMonoType
  | mono : ZonkedSimpleType → ZonkedPolyOrMonoType

  deriving DecidableEq

end


def ZonkedPolyOrMonoType.mem (container : ZonkedPolyOrMonoType) (simpleType : ZonkedSimpleType) : Prop :=
  match container with
  | .mono m =>
    if m = simpleType then
      True
    else
      match m with
      | .primitive _ => False
      | .typeCtor _ inners => List.instMembership.mem inners simpleType
      | .typeVar _ => False
  | .poly p => ZonkedPolyOrMonoType.mem p.type simpleType



instance instMembershipZonkedSimpleTypeZonkedPolyOrMonoType : Membership ZonkedSimpleType ZonkedPolyOrMonoType where
  mem container simpleType :=
    match container with
  | .mono m =>
    match m with
    | .primitive _ => False
    | .typeCtor _ inners => List.instMembership.mem inners simpleType
    | .typeVar _ => False
  | .poly p => instMembershipZonkedSimpleTypeZonkedPolyOrMonoType.mem p.type simpleType

[Matt Diamond]

there's an error in the poly case of ZonkedPolyOrMonoType.mem:

ZonkedPolyOrMonoType.mem p.type simpleType

the first argument to ZonkedPolyOrMonoType.mem has to be a ZonkedPolyOrMonoType, but p.type is a ZonkedSimpleType

I think there's a similar issue in instMembershipZonkedSimpleTypeZonkedPolyOrMonoType

[Yan Yablonovskiy 🇺🇦]

aron said:

Is it possible to define an instance of Membership recursively? I can't figure out how to do this for the below code. I can't define it directly in the Membership.mem instance because it's recursive, but I also can't do it in a separate function first because I want to rely on the Membership instance of List. How can I implement my instance correctly?

I also can't seem to automatically derive a DecidableEq instance for ZonkedSimpleType for some reason.

inductive Primitive
  | int
  | string

inductive TypeVar
  | typeVar


mutual

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

  deriving DecidableEq

structure ZonkedPolyType where
  typeVars : List TypeVar
  type : ZonkedSimpleType

  deriving DecidableEq


inductive ZonkedPolyOrMonoType where
  | poly : ZonkedPolyType → ZonkedPolyOrMonoType
  | mono : ZonkedSimpleType → ZonkedPolyOrMonoType

  deriving DecidableEq

end


def ZonkedPolyOrMonoType.mem (container : ZonkedPolyOrMonoType) (simpleType : ZonkedSimpleType) : Prop :=
  match container with
  | .mono m =>
    if m = simpleType then
      True
    else
      match m with
      | .primitive _ => False
      | .typeCtor _ inners => List.instMembership.mem inners simpleType
      | .typeVar _ => False
  | .poly p => ZonkedPolyOrMonoType.mem p.type simpleType



instance instMembershipZonkedSimpleTypeZonkedPolyOrMonoType : Membership ZonkedSimpleType ZonkedPolyOrMonoType where
  mem container simpleType :=
    match container with
  | .mono m =>
    match m with
    | .primitive _ => False
    | .typeCtor _ inners => List.instMembership.mem inners simpleType
    | .typeVar _ => False
  | .poly p => instMembershipZonkedSimpleTypeZonkedPolyOrMonoType.mem p.type simpleType

Recursive instances have some quirks/workarounds , have a look at this for possible solutions:
https://lean-lang.org/doc/reference/latest///Type-Classes/Instance-Declarations/#recursive-instances

[aron]

@Matt Diamond yeah oops you're right. I've modified my code a bit and now it seems like the main issue is that I can't automatically derive an instance of BEq or DecidableEq on my types, even for Primitive and TypeVar which should be trivially derivable imo?

inductive Primitive
  | int
  | string
  deriving LawfulBEq


inductive TypeVar
  | typeVar
  deriving LawfulBEq



mutual

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

  deriving LawfulBEq


structure ZonkedPolyType where
  typeVars : List TypeVar
  type : ZonkedSimpleType

  deriving LawfulBEq


inductive ZonkedPolyOrMonoType where
  | poly : ZonkedPolyType → ZonkedPolyOrMonoType
  | mono : ZonkedSimpleType → ZonkedPolyOrMonoType

  deriving LawfulBEq


end



def ZonkedSimpleType.mem (container : ZonkedSimpleType) (simpleType : ZonkedSimpleType) : Prop :=
  if h : container = simpleType then -- failed to synthesize `Decidable (container = simpleType)`
    True
  else
    match container with
    | .primitive _ => False
    | .typeCtor _ inners => List.instMembership.mem inners simpleType
    | .typeVar _ => False


def ZonkedPolyOrMonoType.mem (container : ZonkedPolyOrMonoType) (simpleType : ZonkedSimpleType) : Prop :=
  match container with
  | .mono m => ZonkedSimpleType.mem m simpleType
  | .poly p =>
    -- @TODO: need to instantiate the `typeVars` here before doing a straight comparison – because any type vars inside `simpleType` will be from a higher scope so will not be equal to the type vars in `p.typeVars`
    ZonkedSimpleType.mem p.type simpleType



instance instMembershipZonkedSimpleTypeZonkedPolyOrMonoType : Membership ZonkedSimpleType ZonkedPolyOrMonoType where
  mem container simpleType := ZonkedPolyOrMonoType.mem container simpleType

[Aaron Liu]

That's because you're trying to deriving LawfulBEq, deriving DecidableEq does work. (for Primitive and TypeVar at least)

[aron]

@Aaron Liu yeah I never know which of these to use. deriving DecidableEq does indeed work for most of them but not for ZonkedSimpleType for some reason. Do you know why not?

inductive Primitive
  | int
  | string
  deriving DecidableEq


inductive TypeVar
  | typeVar
  deriving DecidableEq



mutual

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

  deriving DecidableEq -- default handlers have not been implemented yet, class: 'DecidableEq' types: [ZonkedSimpleType, ZonkedPolyType, ZonkedPolyOrMonoType]


structure ZonkedPolyType where
  typeVars : List TypeVar
  type : ZonkedSimpleType

  deriving DecidableEq


inductive ZonkedPolyOrMonoType where
  | poly : ZonkedPolyType → ZonkedPolyOrMonoType
  | mono : ZonkedSimpleType → ZonkedPolyOrMonoType

  deriving DecidableEq


end



def ZonkedSimpleType.mem (container : ZonkedSimpleType) (simpleType : ZonkedSimpleType) : Prop :=
  if h : container = simpleType then -- failed to synthesize `Decidable (container = simpleType)`
    True
  else
    match container with
    | .primitive _ => False
    | .typeCtor _ inners => List.instMembership.mem inners simpleType
    | .typeVar _ => False


def ZonkedPolyOrMonoType.mem (container : ZonkedPolyOrMonoType) (simpleType : ZonkedSimpleType) : Prop :=
  match container with
  | .mono m => ZonkedSimpleType.mem m simpleType
  | .poly p =>
    -- @TODO: need to instantiate the `typeVars` here before doing a straight comparison – because any type vars inside `simpleType` will be from a higher scope so will not be equal to the type vars in `p.typeVars`
    ZonkedSimpleType.mem p.type simpleType



instance instMembershipZonkedSimpleTypeZonkedPolyOrMonoType : Membership ZonkedSimpleType ZonkedPolyOrMonoType where
  mem container simpleType := ZonkedPolyOrMonoType.mem container simpleType

[Aaron Liu]

It's because they're mutual types and those are more complicated, no one has written in support for deriving DecidableEq on those mutual inductives yet.

[Aaron Liu]

It looks like you don't actually use them recursively though, so why are they mutual?

[aron]

by "mutual types" do you mean that they're in a mutual block? because you're right I'm not using them mutually atm (I did in an earlier version of the code but I don't think they need to be anymore) but even when I remove the mutual block deriving DecidableEq still doesn't work :/

inductive Primitive
  | int
  | string
  deriving DecidableEq

inductive TypeVar
  | typeVar
  deriving DecidableEq

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

  deriving DecidableEq -- default handlers have not been implemented yet, class: 'DecidableEq' types: [ZonkedSimpleType]

[aron]

unless you mean the issue is that ZonkedSimpleType contains recursive ZonkedSimpleTypes? but why is that an issue?

[Aaron Liu]

I mean that they have mutual recursors, which is partially the mutual block's fault

[Aaron Liu]

If you #print ZonkedSimpleType.rec you see multiple motives, because you use it recursively inside the List.

[aron]

If you #print ZonkedSimpleType.rec you see multiple motives, because you use it recursively inside the List.

hm ok I don't 100% understand what that means, but either way, ok. Why is that a problem? Why is a ctor param being inside a recursive type an issue?

[aron]

and is there a way for me to solve this? what "default handler" is lean looking for and how can I provide it?

[Aaron Liu]

aron said:

Why is that a problem? Why is a ctor param being inside a recursive type an issue?

Because those are more complicated, and someone has to implement the DecidableEq handler, and no one has done it for recursive types yet.

[Aaron Liu]

aron said:

and is there a way for me to solve this? what "default handler" is lean looking for and how can I provide it?

You can just implement the DecidableEq yourself, without relying on a handler.

[aron]

Ok here's where I'm up to so far trying to implement DecidableEq myself. For some reason Lean can't figure out that the my instance is structurally recursive so I need to prove termination myself.

inductive Primitive
  | int
  | string
  deriving DecidableEq

inductive TypeVar
  | typeVar
  deriving DecidableEq

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

def ZonkedSimpleType.typeVar_inj a b : ZonkedSimpleType.typeVar a = .typeVar b → a = b := by
  intro h
  simp


instance instDecidableEqZonkedSimpleType : DecidableEq ZonkedSimpleType :=
  fun a b =>
    match ha : a, hb : b with
    | .primitive p1, .primitive p2 => by
      match decEq p1 p2 with
      | isTrue h =>
        simp
        exact isTrue h
      | isFalse h =>
        simp
        exact isFalse h

    | .typeVar tv1, .typeVar tv2 => by
      match hh : decEq tv1 tv2 with
      | isTrue h =>
        refine isTrue ?_
        simp
      | isFalse h =>
        refine isFalse ?_
        intro hhh
        have := ZonkedSimpleType.typeVar_inj tv1 tv2 hhh
        rw [this] at h
        contradiction

    | .typeCtor name1 inners1, .typeCtor name2 inners2 => by
      let inners := @List.hasDecEq ZonkedSimpleType instDecidableEqZonkedSimpleType inners1 inners2
      match decEq name1 name2, inners with
      | isTrue h1, isTrue h2 =>
        simp
        exact isTrue ⟨h1, h2⟩
      | isFalse h1, isFalse h2 =>
        simp
        refine isFalse ?_
        intro h
        rw [h.left] at h1
        contradiction
      | isFalse h1, isTrue h2 =>
        simp
        refine isFalse ?_
        intro h
        rw [h.left] at h1
        contradiction
      | isTrue h1, isFalse h2 =>
        simp
        refine isFalse ?_
        intro h
        rw [h.right] at h2
        contradiction

    | .primitive _, .typeCtor _ _
    | .primitive _, .typeVar _
    | .typeCtor _ _, .primitive _
    | .typeCtor _ _, .typeVar _
    | .typeVar _, .primitive _
    | .typeVar _, .typeCtor _ _ => by
      all_goals
        refine isFalse ?_
        intro h
        simp at h

  termination_by a b => a
  decreasing_by
    simp

But my proof state is:

unsolved goals
a✝ b✝ : ZonkedSimpleType
name1 : String
inners1 : List ZonkedSimpleType
name2 : String
inners2 : List ZonkedSimpleType
ha : a✝ = ZonkedSimpleType.typeCtor name1 inners1
hb : b✝ = ZonkedSimpleType.typeCtor name2 inners2
a b : ZonkedSimpleType
⊢ sizeOf a < 1 + sizeOf name1 + sizeOf inners1

The problem is I don't know which a this is referring to, because there are no other hypotheses about a available. So there's nothing else I can say about a. How do I solve this?

[Robin Arnez]

I don't think this construction is possible (using List.hasDecEq). This probably works with mutual structural recursion though, one for DecidableEq ZonkedSimpleType and another for DecidableEq (List ZonkedSimpleType)

[Robin Arnez]

Here:

inductive Primitive
  | int
  | string
  deriving DecidableEq

inductive TypeVar
  | typeVar
  deriving DecidableEq

inductive ZonkedSimpleType where
  | primitive : Primitive → ZonkedSimpleType
  | typeCtor : String → List ZonkedSimpleType → ZonkedSimpleType
  | typeVar : TypeVar → ZonkedSimpleType

mutual

def decEqListZonkedSimpleType : DecidableEq (List ZonkedSimpleType) := fun a b =>
  match a, b with
  | [], [] => .isTrue rfl
  | _ :: _, [] => .isFalse List.noConfusion
  | [], _ :: _ => .isFalse List.noConfusion
  | x :: l, y :: l' =>
    match instDecidableEqZonkedSimpleType x y with
    | .isFalse h => .isFalse (fun h' => List.noConfusion h' fun h'' _ => h h'')
    | .isTrue h =>
      match decEqListZonkedSimpleType l l' with
      | .isFalse h2 => .isFalse (fun h' => List.noConfusion h' fun _ h'' => h2 h'')
      | .isTrue h2 => .isTrue (h ▸ h2 ▸ rfl)
termination_by structural a => a

instance : DecidableEq ZonkedSimpleType := fun a b =>
  match a, b with
  | .primitive x, .primitive y =>
    match instDecidableEqPrimitive x y with
    | .isFalse h => .isFalse (fun h' => ZonkedSimpleType.noConfusion h' h)
    | .isTrue h => .isTrue (h ▸ rfl)
  | .typeVar x, .typeVar y =>
    match instDecidableEqTypeVar x y with
    | .isFalse h => .isFalse (fun h' => ZonkedSimpleType.noConfusion h' h)
    | .isTrue h => .isTrue (h ▸ rfl)
  | .typeCtor s l, .typeCtor s' l' =>
    match instDecidableEqString s s' with
    | .isFalse h => .isFalse (fun h' => ZonkedSimpleType.noConfusion h' fun h'' _ => h h'')
    | .isTrue h =>
      match decEqListZonkedSimpleType l l' with
      | .isFalse h2 => .isFalse (fun h' => ZonkedSimpleType.noConfusion h' fun _ h'' => h2 h'')
      | .isTrue h2 => .isTrue (h ▸ h2 ▸ rfl)
  | .primitive .., .typeCtor .. => .isFalse ZonkedSimpleType.noConfusion
  | .primitive .., .typeVar .. => .isFalse ZonkedSimpleType.noConfusion
  | .typeCtor .., .primitive .. => .isFalse ZonkedSimpleType.noConfusion
  | .typeCtor .., .typeVar .. => .isFalse ZonkedSimpleType.noConfusion
  | .typeVar .., .primitive .. => .isFalse ZonkedSimpleType.noConfusion
  | .typeVar .., .typeCtor .. => .isFalse ZonkedSimpleType.noConfusion

end

[Aaron Liu]

This will cause diamonds, you should probably make the instance : DecidableEq (List ZonkedSimpleType) a def.

[Robin Arnez]

Oh yeah, you're right, I edited my message

[aron]

@Robin Arnez ooh ok this seems to work!

What is .noConfusion? it seems to be an automatically generated method for every inductive? what does it do, what is it for?

And how does this approach let us avoid proving termination? (it looks like the termination_by structural a => a isn't even needed btw)

[aron]

plus a few more questions:

1. it looks like instDecidableEqZonkedSimpleType is an automatically generated name for the instance? same for instDecidableEqPrimitive and instDecidableEqTypeVar? is this true for all typeclass instances? how do I know what name is generated for each instance?
2. is .typeVar .. syntax sugar for .typeVar _ _? does this always work? is it just one . per _? is the benefit of this syntax that you don't need to put spaces between the dots?

[Aaron Liu]

.. is sugar for "add as many underscores as possible, based on the type". The benefit of this is you don't need to remember how many underscores to add.

[Robin Arnez]

noConfusion is an automatically generated declaration for every inductive type. It is used to power contradiction and simp only [reduceCtorEq] and all Induct.ctor.inj and Induct.ctor.injEq lemmas. It takes in an equality a = b and produces noConfusionType P a b. noConfusionType is just P if a and b are different constructors (i.e. it gives you a value of any type you want) and otherwise it's a function of the form (a = b -> c = d -> ... -> P) -> P (i.e. if you get P for a pairwise equality of all fields, then you get P).
The problem with using List.decEq is that lean can't know (or doesn't try to infer) how instDecidableEqZonkedSimpleType will be called, for all it knows List.decEq could call it on any two values, causing it to go in an infinite loop. When writing out List.decEq ourselves in mutual recursion it can take into account how it does recursion.
The names for instances are generated automatically and are usually of the shape inst + everything occurring in the type from left to right.