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
```

`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.

:/ 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.

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

instead of `l`

?

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

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

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.
```

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)

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