Zulip Chat Archive

Stream: new members

Topic: Functional extensionality


view this post on Zulip Ken Roe (Jul 24 2018 at 21:53):

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
     (a:tu) (b:tu), a=b  (λ (x:t), a)=(λ (x:t), b) := sorry.

view this post on Zulip Chris Hughes (Jul 24 2018 at 21:56):

There's funext, but that's not the same as what you stated. The proof of the theorem you stated is assume a b h, by rw h

view this post on Zulip Ken Roe (Jul 24 2018 at 22:36):

Thanks. I'm running into another issue. It seems I cannot rewrite if meta variables are involved. How is the following theorem completed (ignore the "admit"--I'd like to get the "rw h" to work.

theorem dd : (λ (x:), x*2)=(λ (x:), x+x) := begin
    have h: x, x*2=x+x, intro, admit,
    rw h
end

view this post on Zulip Simon Hudon (Jul 24 2018 at 22:44):

You can't rewrite bound variables. Use simp only [h] instead

view this post on Zulip Simon Hudon (Jul 24 2018 at 22:45):

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
     (a:tu) (b:tu), a=b  (λ (x:t), a)=(λ (x:t), b) := sorry

Isn't that normal rewriting?


Last updated: May 08 2021 at 19:11 UTC