How to collapse this match?

Using Coq
1

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?

2

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
3

Thanks!

In the end this did the trick:

  apply Lt.lt_0_neq in H.
  destruct l.
  contradiction.
  reflexivity.
4

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.
  contradiction.
  reflexivity.
Qed.