The Coq mailing list

[Tahina Ramananandro <ramananandro AT reservoir.com>]

It looks like a misbehavior (bug or misunderstanding) of `rewrite ... in (value of f)'. Here is a minimal example that has nothing to do with convoy pattern and that fails likewise, in Coq 8.4pl4 as well as in Coq 8.5beta.

Goal forall A (a1 a2: A)

  (EQ: a1 = a2),

  let f := a1 in True.

intros.

rewrite EQ in (value of f).

Error: Found no subterm matching "a1" in f.

Hope this helps,

On Fri, Feb 20, 2015 at 1:07 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

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

--

Tahina Oliver Ramananandro, Ph. D.

Senior Engineer, Advanced Compilers and Formal Verification

Reservoir Labs, Inc.

632 Broadway, Suite 803

New York, NY 10012

USA

Phone: +1 (212) 780-0527 ext. 157

E-mail: ramananandro AT reservoir.com