## Stream: Coq users

### Topic: Snoc lists decomposition

#### Adrián García (Aug 31 2021 at 23:38):

I'm trying to prove the following lemma:

``````Lemma ctx_pos_dec:
forall {X : Type} (G G' D D': slist X) (A: X) (i : nat),
(G, A);G' = (D, A); D' -> ((G, A);G')!i = Some A -> ((D, A);D')!i = Some A
-> G = D /\ G' = D'.
Proof.
intros.
split.
``````

where slists are defined as snoc lists, and the ! operator works as nth in lists counting from right to left, but I'm not able to find something useful in the standard library about nth or list's concatenation. I was thinking about a lemma to show that if ((G, A); G') ! i = Some A and ((D, A); D') ! i = Some A, then G,A = D,A /\ G' = D' and that would be easy I guess, that's a good approach?

#### Adrián García (Aug 31 2021 at 23:44):

I'm doubting about that my helper lemma would be even easy to prove or impossible :thinking:

#### Olivier Laurent (Sep 01 2021 at 06:57):

Is the following an appropriate translation of your statement with usual lists?

``````Lemma ctx_pos_dec:
forall {X : Type} (G G' D D': list X) (A: X) (i : nat),
G' ++ A :: G = D' ++ A :: D -> nth_error (G' ++ A :: G) i = Some A -> nth_error (D' ++ A :: D) i = Some A
-> G = D /\ G' = D'.
``````

If so, you probably need some additional hypotheses like "each element occurs at most once in the lists" otherwise the statement is false. Consider `G = D' = `, `G' = D = []`, `A = 0` and `i = 1`.

Last updated: Feb 09 2023 at 00:03 UTC