Zulip Chat Archive

Stream: new members

Topic: Proving functions are equal

view this post on Zulip Devon Richards (Jan 13 2021 at 00:36):

I was playing around with lean trying to familiarize myself with it so I decided to try and define finite sequences and some operations on them. I defined finite_sequence (n : nat) (\alpha : Type u) as fin n \to \alpha. Then I defined initial_segment s m which is the sequence of the first m elements of s, and concat s t which is the sequence made by the elements of s followed by the elements of t.
Now I'm trying to prove that \forall (s t : finite_sequence n \alpha), s = initial_segment (concat s t) and I'm having trouble figuring out how to prove it in Lean. The outline of the proof in my head is to show that \forall i, s i = (initial_segment (concat s t)) i. Do I need to restate the theorem in that form or is there some good way to prove them equal otherwise without needing to simplify the definitions till they're definitionaly equal? I was wanting to treat the sequences as concrete objects not functions so the equality without the explicit parameter seemed much more aesthetically appealing.

view this post on Zulip Hanting Zhang (Jan 13 2021 at 00:44):

To "prove things are equal by proving their parts are equal," i.e. extensionality, you use the ext tactic (tactic#ext). Although this is general advice and I'm not completely sure it will work for your case.

view this post on Zulip Chris Hughes (Jan 13 2021 at 00:46):

funext is the theorem you need. The ext tactic is one way of automatically applying funext

view this post on Zulip Devon Richards (Jan 13 2021 at 00:47):

Thank you, that was exactly what I wanted.

Last updated: May 14 2021 at 12:18 UTC