The Coq mailing list

[Andreas Lundblad <landreas AT kth.se>]

Hi everybody,

I've run into a situation, similar to the situation below. Basically,
I would like to tell Coq to apply the argument l to the
fix-expression. The match-expression would then become

match nth 2 l 7 with ...

which could be rewritten using H and then simplified. What to do?

best regards
Andreas Lundblad


------ Coq Script: -----------------

Require Import List.

Theorem test :
  forall l,
    nth 2 l 7 = 0 ->
    0 = ((fix func (l0: list nat) :=
      match nth 2 l0 7 with
        | 0 => 0
        | _ => 1
      end) l).
Proof.
intros.


------ RESULTING STATE: ------------

1 subgoal

  l : list nat
  H : nth 2 l 7 = 0
  ============================
   0 =
   (fix func (l0 : list nat) : nat :=
      match nth 2 l0 7 with
      | 0 => 0
      | S _ => 1
      end) l

------------------------------------