Zulip Chat Archive

Stream: new members

Topic: Proving from optional parameter

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 13 2018 at 16:21):

How do I fill in the sorry?

example (c : ) (f :   ) (g :    := λ (x : ), f (2 * c - x)) :   x, g x = f (2 * c - x) := sorry

Presumably I need to intro and input an x into g somehow -- but how? I know the specific example can be rewritten in a way that makes the proof by assumption, but this situation cropped up in another proof.

view this post on Zulip Chris Hughes (Nov 13 2018 at 16:25):

I don't think this is true. The := notation for g, just assigns a default value to g, if the user doesn't specify one when using the lemma, but you still have to prove for any g, since the user can override the default and use whatever value for g they like when using the lemma.

view this post on Zulip Kevin Buzzard (Nov 13 2018 at 17:21):

Maybe you want let g := ... in ...?

view this post on Zulip Chris Hughes (Nov 13 2018 at 17:33):

If you have let g := something in some proof, you can prove g = something with rfl.

Last updated: May 11 2021 at 00:31 UTC