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' = [0], G' = D = [], A = 0 and i = 1.

Last updated: Oct 08 2024 at 16:02 UTC