## Stream: Coq users

### Topic: Stuck on Seemingly Trivial Lemma

#### Julia Dijkstra (Dec 20 2023 at 05:47):

I am trying to prove the following lemma:

``````Lemma inner_rev: forall {X: Type} (l: list X) x, x :: l ++ [x] = rev (x :: l ++ [x]) -> l = rev l.
``````

I got stuck on part of this where I needed the following:

``````Lemma app_tail_inj: forall {X: Type} (l l1 l2: list X), l1 ++ l = l2 ++ l -> l1 = l2.
Proof.
induction l.
- intros. repeat rewrite app_nil_r in H. apply H.
- intros. apply IHl. Abort.
``````

It feels like this should be possible with something like injection, but that doesn't work with how app is defined. Any ideas? I am left with the following proof-state:

``````X : Type
x : X
l : list X
IHl : forall l1 l2 : list X, l1 ++ l = l2 ++ l -> l1 = l2
l1, l2 : list X
H : l1 ++ x :: l = l2 ++ x :: l

(1 / 1)
l1 ++ l = l2 ++ l
``````

#### Quentin VERMANDE (Dec 20 2023 at 06:58):

`x` is in the middle of your lists, so it will be difficult to get rid of. The induction on `l1` should work, since you will end up with a hypothesis like `x :: l1 ++ l = y :: l2 ++ l`, which you can work with.

#### Julia Dijkstra (Dec 20 2023 at 08:14):

:/ I seem to have been going in circles for hours now. I can make it depend on other lemmas, but those again run into the same issue of not being able to discriminate append.

#### Quentin VERMANDE (Dec 20 2023 at 08:28):

Did you get stuck when trying to start your proof by an induction on `l1` instead of `l` ?

#### Gaëtan Gilbert (Dec 20 2023 at 08:32):

I got stuck on part of this where I needed the following:

that's List.app_inv_tail, you can look at its proof here https://github.com/coq/coq/blob/36e43a08eadccc544c8550e8e760d2a4ae7efb92/theories/Lists/List.v#L250-L257

#### Gaëtan Gilbert (Dec 20 2023 at 08:34):

there's probably an alternative proof by doing induction l1;destruct l2, then when they don't match (eg in the case where your hypothesis is `x :: tl1 ++ l = [] ++ l`) using `app_length` to get the contradiction

#### Julia Dijkstra (Dec 20 2023 at 09:21):

I have reduced it as far as I could and I genuinely am about to give up. I Admitted on this lemma, because honestly it seems like you need to prove the universe for this one problem.

``````Lemma app_length_trans: forall {X: Type} (l1 l2 l: list X), l1 ++ l = l2 ++ l -> length l1 = length l2.
``````

#### Gaëtan Gilbert (Dec 20 2023 at 09:26):

from `l1 ++ l = l2 ++ l` you get `length (l1 ++ l) = length (l2 ++ l)`
then rewrite app_length gets you `length l1 + length l = length l2 + length l`
then cancellation of nat addition gets you the goal

(deleted)

#### Dominique Larchey-Wendling (Dec 20 2023 at 18:55):

Trick 1: use `List.rev` and its properties. Or trick 2: proceed by induction from the tail of the list, aka `snoc` induction.

Last updated: Jun 23 2024 at 05:02 UTC