The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

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.