Stream: new members
Topic: Proving functions are equal
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.
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.
Chris Hughes (Jan 13 2021 at 00:46):
funext is the theorem you need. The
ext tactic is one way of automatically applying funext
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