Christian Doczkal (Sep 30 2020 at 09:14): 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.
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: Oct 13 2024 at 01:02 UTC