Stream: Coq users

Topic: Stuck on Seemingly Trivial Lemma


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Julia Dijkstra (Dec 20 2023 at 09:26):

(deleted)

view this post on Zulip 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