Beginners use of CoeDep

Stream: new members

[Garrison Venn]

I'm trying to figure out why I cannot get a dependent coercion to trigger.
I have:

inductive GBinTree (α : Type) where
  | leaf : GBinTree α
  | branch : GBinTree α → α → GBinTree α → GBinTree α
deriving Repr

def eqBinTree [BEq α] : GBinTree α → GBinTree α → Bool
  | GBinTree.leaf, GBinTree.leaf => true
  | GBinTree.branch l x r, GBinTree.branch l2 x2 r2 =>
    x == x2 && eqBinTree l l2 && eqBinTree r r2
  | _, _ => false

instance [BEq α] : BEq (GBinTree α) where
  beq := eqBinTree

def hashBinTree [Hashable α] : GBinTree α → UInt64
  | GBinTree.leaf => 0
  | GBinTree.branch left value right =>
    mixHash 1
      (mixHash (hashBinTree left)
        (mixHash (hash value)
          (hashBinTree right)))

instance [Hashable α] : Hashable (GBinTree α) where
  hash := hashBinTree

def GBinTree.map {α : Type} {β : Type}: (α -> β) -> GBinTree α -> GBinTree β
  | _, leaf => leaf
  | f, branch left value right =>
    branch (map f left) (f value) (map f right)

instance : Functor GBinTree  where
  map := GBinTree.map

instance : Coe Unit (GBinTree α) where
  coe _ := .leaf

def GOptEither (α : Type) (τ : Type) : Type :=
  Option (α ⊕ τ)

def GBinTreeState (α : Type) := GOptEither α (GBinTree α)

-- Not triggered
instance : CoeDep (GBinTreeState α) (some (Sum.inr tree)) (GBinTree α) where
  coe := tree

def toTest1 : GBinTreeState String := some (Sum.inr (GBinTree.leaf))
-- Expected a dependent coercion but get a Type mismatch failure
def toTest2 : GBinTree String := toTest1
-- Non-dependent coercion which works
def toTest3: GBinTree String := ()

The question I have is why the definition of toTest2 does not work. I'm thinking that maybe it is the way I "defined" GBinTreeState, and possibly GOptEither?

This example is derived from the Lean tutorial. Even though they are not directly used, I included the Class Type instantiations of BEq, Hashable, and Functor just in case there is some kind of interference.

Thanks in advance

[Aaron Liu]

toTest1 does not get unfolded

[Aaron Liu]

it's not transparent enough for typeclass to unfold it

[Garrison Venn]

So use abbrev.

[Garrison Venn]

Transform:

def toTest1 : GBinTreeState String := some (Sum.inr (GBinTree.leaf))

to:

abbrev toTest1 : GBinTreeState String := some (Sum.inr (GBinTree.leaf))

Thanks!! :slight_smile:

[Garrison Venn]

[Garrison Venn]

To dive deeper: if I have a function which returns an element of the above tree vs just defining it immediately as is done above for toTest1, it seems also to not keep the result unfolded when trying the same dependent coercion. I attempted changing from def to abbrev for such a function with no consequence. I'm gathering there is a more intricate requirement than just changing a function to be defined by abbrev? Is it even possible? Sorry I'm obviously an extreme noob right now, but the answers I get here help to toward my understanding. I can provide code of course if needed.

[Aaron Liu]

well all the parts of your function also have to be reducible enough

[Garrison Venn]

So I have:

--def leftTreeStep {α : Type} : GBinTree α → GBinTreeState α
abbrev leftTreeStep {α : Type} : GBinTree α → GBinTreeState α
  | GBinTree.leaf => none
  | GBinTree.branch l _ _ => some (Sum.inr l)

open GBinTree in
def aTree :=
  branch
    (branch
      (branch leaf "a" (branch leaf "b" leaf))
      "c"
      leaf)
    "d"
    (branch leaf "e" leaf)

abbrev toTest6 := leftTreeStep aTree
-- Fails
def toTest7 : GBinTree String := toTest6

[Garrison Venn]

Never mind aTree needed abbrev vs def. :zany_face:

[Garrison Venn]

Unfortunately I don't have a good internalized model yet, and I think I have a long way to go. :slight_smile: