The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/20/2015 01:21 PM, Tahina Ramananandro wrote:

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,

=-O    I'll report that.  I guess rewriting values isn't too common...

A workaround is pretty easy, though:

Ltac rewrite_value rw H :=
  let V := eval cbv delta [H] in H in
  let E := fresh in
  let X := fresh in
  remember V as X eqn:E in H;
  rewrite rw in E;
  subst X.

Goal forall A (a1 a2: A)
  (EQ: a1 = a2),
  let f := a1 in True.
intros.
Fail rewrite EQ in (value of f).
rewrite_value EQ f.

-- Jonathan

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