Help: how to use dependent function type

Stream: lean4

[Locria Cyber]

How do I make something like this to work? map_to_T is not reducing in the type position.

abbrev map_to_T ( x : String) : Type :=
if x = "0" then
  Nat
else
  String

def map_to : (x : String) -> map_to_T x :=
λ x => if x = "0" then
  42
  else
  x

[Joe Watt]

Here's something that works:

abbrev map_to_T (x : String) : Type :=
  if x = "0" then Nat else String

def map_to (x : String) : map_to_T x :=
  if h : x = "0" then by
    simp [map_to_T, h]
    exact 42
  else by
    simp [map_to_T, h]
    exact x

The idea here is that we want to be able to use the definition of map_to_T and the condition of whether x = "0" in both branches, to simplify the type to either Nat or String. To perform such simplification, we can leverage the Curry-Howard correspondence underlying dependent type theory to supply the terms in tactic mode, using simp to simplify the terms as such.

[Locria Cyber]

Thanks! I didn't know tactics can be used like this.

[Locria Cyber]

How do i mark this topic as "done"? I remember being able to do that.

[Joscha Mennicken]

The feature for resolving threads was disabled recently: #Zulip meta > ✔ Resolving topics @ 💬