Helping the type checker, propagating type equality

Stream: new members

[Justin Pearson]

What can I do with the following piece of code ?

variable f : ℕ → Type
variable my_fun (x : ℕ) (y : ℕ)  : f x

def my_sub (new_x : ℕ)  (new_y : f new_x )  (x : ℕ) (y : ℕ) : f x  :=
  if (x = new_x) then new_y else my_fun x

It does not type check because new_y has type f new_x, but should have type f x. It is easy to prove that f x = f new_x from x=y, but how do I have convince the type checker that is true?

[Johan Commelin]

@Justin Pearson You can do

variable f : ℕ → Type
variable my_fun (x : ℕ) (y : ℕ)  : f x

#check my_fun -- Π (x : ℕ), ℕ → f x

def my_sub (new_x : ℕ) (new_y : f new_x) (x : ℕ) (y : ℕ) : f x :=
if h : x = new_x
  then (by { cases h, exact new_y }) -- new_y
  else my_fun x x -- my_fun x

but I think it will be hard to work with this definition.

[Johan Commelin]

Can you explain what you are trying to do exactly?

[Johan Commelin]

Does my_fun actually have the type that you intended it to have?

[Eric Wieser]

Note that my_sub is precisely docs#function.update

[Justin Pearson]

The example has been reduced down to work on the naturals. I'm modelling multi-sorted first order logic, and this is a version of the substitution function. An assignment has a type that is something like

 (assign (s:S) : V →   (f s) )

So given a sort 's' it should have a value in the type (f s). Maybe there is a better way of doing this?

[Justus Springer]

You could also use dite, a dependent version of if:

variable f : ℕ → Type
variable my_fun (x : ℕ) (y : ℕ)  : f x

variables (new_x : ℕ)  (new_y : f new_x )  (x : ℕ) (y : ℕ)

def my_sub (new_x : ℕ)  (new_y : f new_x )  (x : ℕ) (y : ℕ) : f x  :=
  dite (x = new_x) (λ h, h.symm.rec_on new_y) (λ h, my_fun x x)

[Eric Wieser]

@Justus Springer , the if h : x = new_x then ... else ... in Johan Commelin's message above is syntax for dite.

[Justus Springer]

Oh right, I didn't know you could do that