Stream: math-comp devs

Topic: lemma names


view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 21:01 UTC