Stream: math-comp devs

Topic: lemma names

Christian Doczkal (Sep 30 2020 at 09:14):

I'm just going over the sequence of lemmas that I proved about `subseq`, `index`, `rot`, and the likes and which I plan to PR. But I'm still looking for some good lemma names. What would be good names for the following (assuming the statements are in the right form to begin with):

``````Lemma eqseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) (x : T) :
uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4).
Lemma subseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) x :
uniq (s3 ++ x :: s4) -> subseq (s1 ++ x :: s2) (s3 ++ x :: s4) -> subseq s1 s3 /\ subseq s2 s4.
``````

Cyril Cohen (Sep 30 2020 at 11:14):

Christian Doczkal said:

I'm just going over the sequence of lemmas that I proved about `subseq`, `index`, `rot`, and the likes and which I plan to PR. But I'm still looking for some good lemma names. What would be good names for the following (assuming the statements are in the right form to begin with):

``````Lemma eqseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) (x : T) :
uniq (s3 ++ x :: s4) -> s1 ++ x :: s2 == s3 ++ x :: s4 = (s1 == s3) && (s2 == s4).
Lemma subseq_??? (T : eqType) (s1 s2 s3 s4 : seq T) x :
uniq (s3 ++ x :: s4) -> subseq (s1 ++ x :: s2) (s3 ++ x :: s4) -> subseq s1 s3 /\ subseq s2 s4.
``````

yes indeed, I think we need a name for this pattern `s1 ++ x :: s2` and decide once and forall whether which of the former and `rcons s1 x ++ s2` we prefer as a canonical formulation.

Last updated: Jul 23 2024 at 20:01 UTC