Zulip Chat Archive

Stream: new members

Topic: Helping the type checker, propagating type equality


Justin Pearson (Sep 13 2021 at 08:40):

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 (Sep 13 2021 at 08:48):

@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 (Sep 13 2021 at 08:48):

Can you explain what you are trying to do exactly?

Johan Commelin (Sep 13 2021 at 08:48):

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

Eric Wieser (Sep 13 2021 at 08:54):

Note that my_sub is precisely docs#function.update

Justin Pearson (Sep 13 2021 at 08:54):

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 (Sep 13 2021 at 13:01):

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 (Sep 13 2021 at 14:55):

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

Justus Springer (Sep 13 2021 at 15:00):

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


Last updated: Dec 20 2023 at 11:08 UTC