coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Brian Aydemir <baydemir AT cis.upenn.edu>
- To: robdockins AT fastmail.fm
- Cc: Coq Mailing List <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] odd termination issue
- Date: Sat, 16 Feb 2008 20:17:10 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Robert Dockins wrote:
The issue is that I would like to reuse a fancy finite map datastructure in a datatype definition. ...
Has anyone else encountered this problem and is there a better solution?
It is possible to avoid reinventing the wheel. There has been some previous discussion on this topic:
- Inductive definitions that go through lists:
http://pauillac.inria.fr/pipermail/coq-club/2007/003224.html
- How Coq checks the well-formedness of recursive calls:
http://pauillac.inria.fr/pipermail/coq-club/2008/003390.html
Below, I give one take on your example. The code's a bit much at first glance, but the first part can go in some library (you could instead define the exact version of list_pair_snd_ind that you need) and the third part proves a useful induction principle for your datatype.
Cheers,
Brian
(* ******************************************* *)
Require Import List.
(* *********************************************** *)
(** * Generic library code. *)
(** The following tactic calls the [apply] tactic with the first
hypothesis that succeeds, "first" meaning the hypothesis that
comes earlist in the context (i.e., higher up in the list). *)
Ltac apply_first_hyp :=
match reverse goal with
| H : _ |- _ => apply H
end.
(** A slightly more useful combinator for working with lists of pairs.
Compared to the default induction principle for lists, in the case
for [cons], we get an additional hypothesis about the second
component of the pair being consed.
The use of tactics here is overkill, but it fits into a pattern
that seems to save a reasonable amount of effort when you have
many constructors to deal with. See below.
I essentially got this idea from Yves Bertot. See
http://logical.futurs.inria.fr/cgi-bin/bugzilla/show_bug.cgi? id=1751 *)
Definition list_pair_snd_ind :
forall (A B : Type)
(P : B -> Type)
(P' : list (A * B) -> Type)
(Hnil : P' nil)
(Hcons : forall a b xs, P b -> P' xs -> P' ((a,b) :: xs)),
(forall x, P x) -> (forall xs, P' xs).
Proof.
intros A B P P' Hnil Hcons f.
fix g 1.
intros xs; case xs; [ | intros pair ys; destruct pair ];
repeat (first [apply_first_hyp]).
Defined.
(* *********************************************** *)
(** * The data structure and function of interest. *)
Inductive ex1 : Set :=
| ex1_nat : nat -> ex1
| ex1_map : list (nat * ex1) -> ex1.
Section interp.
Variables
(A : Type)
(f : nat -> A)
(INil : A)
(IComb : nat -> A -> A -> A).
Fixpoint ex_interp (X : ex1) { struct X } : A :=
match X with
| ex1_nat n => f n
| ex1_map M => list_pair_snd_ind _ _ (fun _ => A) (fun _ => A)
INil
(fun a b xs arec brec => IComb a arec brec)
ex_interp
M
end.
End interp.
(* *********************************************** *)
(** * Prove a useful induction principle. *)
Section Recursion.
Variables
(P : ex1 -> Type)
(P' : list (nat * ex1) -> Type)
(Pnat : forall n : nat, P (ex1_nat n))
(Pcons : forall l : list (nat * ex1), P' l -> P (ex1_map l))
(Inil : P' nil)
(Icons : forall n x xs, P x -> P' xs -> P' ((n, x) :: xs)).
Definition ex1_rect' : forall x : ex1, P x.
fix f 1.
intros x; destruct x;
repeat (first [apply_first_hyp | eapply list_pair_snd_ind]).
Defined.
End Recursion.
- [Coq-Club] odd termination issue, Robert Dockins
- Re: [Coq-Club] odd termination issue, Brian Aydemir
- Re: [Coq-Club] odd termination issue,
Robert Dockins
- Re: [Coq-Club] odd termination issue,
Robin Green
- Re: [Coq-Club] odd termination issue, Yves Bertot
- Re: [Coq-Club] odd termination issue,
Robin Green
- Re: [Coq-Club] odd termination issue,
Robert Dockins
- Re: [Coq-Club] odd termination issue, Brian Aydemir
Archive powered by MhonArc 2.6.16.