The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Sometimes, tactics like destruct produce proof terms that, while thoroughly reduced, aren't as simple as possible due to over-zealous use of convoy patterns.  In one particular case, I tried to simplify such a function with a rewrite rule - but it doesn't work.  What am I doing wrong?

Here's the rewrite rule, showing the convoy-pattern version of the function as the lhs of the rewrite equality and the simplification as the rhs:

Lemma decon :
  forall (n : nat) A R (f0 : A -> R) (fSn : A -> nat -> R),
    (fun a : A => match n with
     | 0 => fun _ : A => f0 a
     | S n' => fun _ : A => fSn a n'
     end a) =
    (fun a : A => match n with
     | 0 => f0 a
     | S n' => fSn a n'
     end).
Proof.
  intros.
  destruct n; reflexivity.
Qed.

But, the rewrite doesn't work:

Require Setoid.

Goal forall (n : nat) A R (f0 : A -> R) (fSn : A -> nat -> R),
    let f := (fun a : A => match n with
                           | 0 => fun _ : A => f0 a
                           | S n' => fun _ : A => fSn a n'
                           end a) in True.
intros.
rewrite (decon n A R f0 fSn) in (value of f).

produces the error:

Error:
Found no subterm matching "fun a : A =>
                           match n with
                           | 0 => fun _ : A => f0 a
                           | S n' => fun _ : A => fSn a n'
                           end a" in f.

Which, even with Set Printing All, is an exact match for the body of f.

-- Jonathan