Stream: new members
Ned Summers (Aug 20 2018 at 15:15):
I'm trying to construct a function
f : a → b (as part of an instance of a structure) with two types a and b and non-trivially I have that for some type c defined differently in fact
b=c (and I can prove that if needed).
How can I let lean know that in fact, what might appear to be of type
a → c (being given by
λ x , y, for some
y : c) is in fact totally fine and fulfils the requirement for being of type
a → b?
Simon Hudon (Aug 20 2018 at 15:18):
One way do it is to use
cast. It does get in the way when trying to reason about the function but it does what you said. You could do it as
cast (by subst c) f
Simon Hudon (Aug 20 2018 at 15:21):
I sometimes define local notations for this kind of cast:
local prefix `♯`:0 := cast (by cc <|> solve_by_elim)
Ned Summers (Aug 21 2018 at 09:48):
Ah ok, thanks. I'm not familiar with using subst, how would I include a proof that b = c in this? Currently, I'm being told "subst tactic failed, given expression is not a local constant". Apologies, I am very much a beginning.
Ned Summers (Aug 21 2018 at 10:21):
Never mind, managed to get that sorted!
Ned Summers (Aug 21 2018 at 10:39):
I'm not sure if this is what you originally meant, Simon, but I ended up solving this with
λ x , cast( ... ) y, using my proof in the brackets. However, if I also had properties previously expressed about y, how do I go about using these for the cast version?
For example (fairly close to what I'm doing), if y were in the center of a group, is it possible to prove that for some other member x, cast _ y * x = x * cast _ y? Or do we lose this information in casting?
Kevin Buzzard (Aug 21 2018 at 13:31):
Maybe you should take a look at https://leanprover.github.io/theorem_proving_in_lean/tactics.html#rewriting
Last updated: May 08 2021 at 09:11 UTC