coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] attempting to de-convoy a function via rewrite doesn't work
- Date: Fri, 20 Feb 2015 16:15:18 -0500
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 :=-- 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 |
- [Coq-Club] attempting to de-convoy a function via rewrite doesn't work, Jonathan Leivent, 02/20/2015
- Re: [Coq-Club] attempting to de-convoy a function via rewrite doesn't work, Tahina Ramananandro, 02/20/2015
- Re: [Coq-Club] attempting to de-convoy a function via rewrite doesn't work, Jonathan Leivent, 02/20/2015
- Re: [Coq-Club] attempting to de-convoy a function via rewrite doesn't work, Tahina Ramananandro, 02/20/2015
Archive powered by MHonArc 2.6.18.