Coq simpl failing to do beta reduction in this fixpoint expression

Question

I have

Fixpoint concat_aux {A : Type} (lang1 lang2 : list A -> nat -> nat -> bool) (w : list A) (start : nat) (delta i : nat) : bool :=
    match lang1 w start i && lang2 w (start + i) (delta - i) with
    | true => true
    | false => match i with
        | 0 => false
        | S i' => concat_aux lang1 lang2 w start delta i'
        end
    end.

This lemma should be trivial by substituting,

Lemma concat_aux_correct1 {A : Type} : forall lang1 lang2 w start delta i,
    lang1 w start i = true /\ lang2 w (start + i) (delta - i) = true
    -> @concat_aux A lang1 lang2 w start delta i = true.

But the following fails to make progress.

Proof.
    intros.
    simpl. (* nothing happens *)
    unfold concat_aux.
    simpl. (* nothing happens *)
Admitted.

Why is this happening and what do I do?

Answer 1

There is no reduction to be done, which is why simpl isn't doing anything.

First of all, concat_aux is not a double fixpoint, but a simple fixpoint on the 7th argument i (as you can check from Coq's message upon going through the definition: concat_aux is recursively defined (guarded on 7th argument)). This means that reduction is only possible when the 7th argument is a constructor, i.e., either O or S j for some j, which is not the case.

Second of all, having an equality in your context is not enough to reduce anything. Compare

Eval simpl in (0 + 1).

with

Variable n : nat. Hypothesis H : n = 0.
Eval simpl in (n + 1).

The former reduces to 1, while the latter stays the same.

Given the above, the way to make progress with your lemma is to do case analysis on i and then use your hypothesis about lang1 and lang2 being true to solve the goals. The case analysis is spurious, yes, but it will actually allow you to make progress. You can use the same proof for both cases (with copy-paste, ;, goal selectors, a lemma, etc).