coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- To: Sean Wilson <sean.wilson AT ed.ac.uk>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Rewrite rules from functions
- Date: Tue, 28 Aug 2007 09:22:26 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Sean Wilson wrote:
Hi,Not exactly what you describe, but you can also have directly the single fix-point equation:
I'm trying to write some automatic rewriting tactics and was wondering if Coq already has a certain feature already.
Given the usual definition of app:
fun A : Type =>
fix app (l m : list A) {struct l} : list A :=
match l with
| nil => m
| a :: l1 => a :: app l1 m
end
From this definition, we can directly read off two rewrite rules it implies:
forall m, app nil m = m
forall a l1 m, app (a::l1) m = a::app l1 m
...
forall A l, app l m = match l with nil => m | a :: ll => a :: app ll m end.
Here is how:
Welcome to Coq 8.1 (Feb. 2007)
Coq < Require Import List.
Coq < Functional Scheme app_ind := Induction for app Sort Prop.
app_equation is defined
app_ind is defined
Coq < Check app_equation.
app_equation
: forall (A : Type) (l m : list A),
l ++ m = match l with
| nil => m
| a :: l1 => a :: l1 ++ m
end
Coq < Lemma example : (1::2::nil)++(3::nil) = (1::2::3::nil).
1 subgoal
============================
(1 :: 2 :: nil) ++ 3 :: nil = 1 :: 2 :: 3 :: nil
example < rewrite app_equation.
1 subgoal
============================
1 :: (2 :: nil) ++ 3 :: nil = 1 :: 2 :: 3 :: nil
example < rewrite app_equation.
1 subgoal
============================
1 :: 2 :: nil ++ 3 :: nil = 1 :: 2 :: 3 :: nil
example < rewrite app_equation.
1 subgoal
============================
1 :: 2 :: 3 :: nil = 1 :: 2 :: 3 :: nil
As you see the single equation app_equation behaves like your collection of equations when any of
them would apply...
Note that the fix-point equation is generated automatically when you use Function instead of
Fixpoint to define your recursive function (Function does a few more things, though, please refer
to the documentation).
Yves
- [Coq-Club] Rewrite rules from functions, Sean Wilson
- Re: [Coq-Club] Rewrite rules from functions, Yves Bertot
- Re: [Coq-Club] Rewrite rules from functions, Sean Wilson
- Re: [Coq-Club] Rewrite rules from functions, Yves Bertot
Archive powered by MhonArc 2.6.16.