The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I've paired down a small example of an issue I've run into with a proof 
development.  The issue is that I would like to reuse a fancy finite map 
datastructure in a datatype definition.  However, when I attempt to define 
fixpoint functions on the new datatype, Coq fails to determine that the 
function is structurally recursive.  I can work around the problem by 
defining a finite map datastructure mutually recursively with the datatype I 
am interested in; however, this is a major pain because now I have to develop 
the theory of finite maps from the ground up.

Has anyone else encountered this problem and is there a better solution?

Thanks,
Rob Dockins


---- code follows ------

Require Import List.

(* Attempt 1: reuse a standard library
   datastructure.
 *)

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).

(* Attempt 1 fails when Coq refueses to recognize
   that the following function is structurally
   recursive.

 Recursive definition of ex_map_interp is ill-formed
 ...
 Recursive call to ex_interp has principal argument equal to 
  "b"
  instead of l
 *)

(*
Fixpoint ex_interp  (X:ex1) { struct X } : A :=
  match X with
  | ex1_nat n => f n
  | ex1_map M => ex_map_interp M
  end
 with ex_map_interp (M:list (nat*ex1)) : A :=
  match M with
  | nil => INil
  | (a,b)::l => IComb a (ex_interp b) (ex_map_interp l)
  end.
*)
End interp.


(* Attempt 2: reinvent the wheel *)

Inductive ex2 : Set :=
  | ex2_nat : nat -> ex2
  | ex2_map : exmap -> ex2
 with exmap : Set :=
  | exmap_nil : exmap
  | exmap_cons : (nat * ex2) -> exmap -> exmap
  .

Section interp2.
  Variables
   (A:Type)
   (f:nat -> A)
   (INil:A)
   (IComb:nat->A->A->A).

(* Attempt 2 succeeds in reinventing the wheel...
 *)

Fixpoint ex_interp  (X:ex2) { struct X } : A :=
  match X with
  | ex2_nat n => f n
  | ex2_map M => ex_map_interp M
  end
 with ex_map_interp (M:exmap) : A :=
  match M with
  | exmap_nil => INil
  | exmap_cons (a,b) l => IComb a (ex_interp b) (ex_map_interp l)
  end.
End interp2.