# How to collapse this match?

I have this:

1 subgoal
l : nat
H : 0 < l
______________________________________(1/1)
match l with
| 0 => true :: nil
| S _ => g_one l ++ false :: nil
end = g_one l ++ false :: nil

this seems trivially true, but I can’t figure out how to get Coq to see that - any suggestions?

A match will simplify when the head starts with a constructor, so you need a way to rewrite `l` into `S l'` for some `l'`, which suggests to use the following intermediate step:

``````assert (exists l', l = S l').
``````

Another idea (to combine with the above or not) is to use `inversion` (maybe twice) because `<` is defined using an inductive type.

You can also search for a lemma about `<` (`lt`) and `0` to solve that intermediate step:

``````SearchAbout lt 0.
``````

One result that seems particularly relevant is

``S_pred_pos: forall n : nat, 0 < n -> n = S (Nat.pred n)``
1 Like

Thanks!

In the end this did the trick:

``````  apply Lt.lt_0_neq in H.
destruct l.
reflexivity.
``````

This is the whole thing, in case you are interested.

``````Fixpoint g_one (l : nat) : list bool :=
match l with
| 0 => nil
| 1 => true::nil
| S l' => g_one l' ++ false::nil
end.

Lemma one_is_one_longer :
forall (l : nat),
0 < l -> g_one(S l) = g_one(l) ++ false::nil.
Proof.
intros.
simpl.
apply Lt.lt_0_neq in H.
destruct l.