Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Rewrite rules from functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewrite rules from functions


chronological Thread 
  • 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,

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

...
Not exactly what you describe, but you can also have directly the single fix-point equation:

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





Archive powered by MhonArc 2.6.16.

Top of Page