Type Equivalence

Stream: new members

[Simon Daniel]

Hi all,
i defined this Option like Inductive I

inductive I (ns: Finset Nat) (n: Nat) (α: Type)   where
| Some:  (n ∈ ns) -> α -> I ns n α
| None:  (n ∉ ns) ->      I ns n α

def v1: I  {1,2} 2 String        := I.Some (by decide) "hello"

It holds a value of α if the second type parameter n is included in the set ns.
obviously there is an equivalence of types I ns n and I ns' n where ns and ns' are equal.
the function castI transforms from one to another.

def castI (eq: ns' = ns): I ns n α -> I ns' n α
| I.Some p v => I.Some (by simp [eq]; exact p) v
| I.None p =>   I.None (by simp [eq]; exact p)

def v2: I ({1,2} ∪ {1}) 2 String := castI  (by decide) v1
def v3: I ({1,2} ∪ {1}) 2 String := v1 -- shoud be casted / coerced automatically

Is there an elegant way to hide this casting step? I thought of a coe instance but failed to define it.
thanks in advance :)

[Number Eighteen]

Note that you don't need a separate lemma:

def v1: I  {1,2} 2 String := I.Some (by decide) "hello"

def eq : ({1,2} : Finset Nat) ∪ {1} = {1,2} := by decide

def v2: I ({1,2} ∪ {1}) 2 String :=  eq ▸ v1

[Robert Maxton]

Generally no, and indeed much of the difficulty of programming with dependent types is due to the poor behavior of casting and HEq at a mathemtical-foundational level. We tend to avoid dealing with type equality in general as a result, instead preferring just such explicit type-specific casting functions.

[Robert Maxton]

Playing around with the code in the Lean playground, I'm guessing the problem you're running into with Coe instances is errors of the form cannot find synthesization order for instance ...? That means that there's no reasonable way for the compiler to infer one of the variables in the instance from the context; in this case, there's no good way to guess what ns should be given only that the output is I ns' n α, since the set of things that are propositionally equal to ns could be huge.

[Robert Maxton]

In certain cases, the compiler can make use of definitional equality to make this go through for you, but that requires that ns be definitionally equal to ns' -- usually meaning that it's syntactically the same after unfolding reducible definitions -- and not merely that there exists a proof that they're equal (which is propositional equality and a much broader class).

[Simon Daniel]

thanks for your answers, explicit casting seems reasonable

i was already wondering why lean is able to make sense of this:

def v1: I  {1,2} 2 String  := I.Some (by decide) "hello"
def v3: I ({1} ∪ {2}) 2 String := v1

but it seems like lean unfolds the union directly.
i tried to define coe like this:

instance (eq: ns = ns'): Coe (I ns n α) (I ns' n α) where
  coe := castI eq

with a "instance does not provide concrete values for (semi-)out-params" error that i dont quite understand.