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

Julia Dijkstra (Dec 20 2023 at 09:26):

(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: Oct 13 2024 at 01:02 UTC