The Coq mailing list

["Shen Shixiong" <ssxtim AT 163.com>]

Hi all,

  We have an inductive type 'a' which has two cases. We want to write a fixpoint 'getnames' to combine the names in ‘a’ recursively. But 'getnames' involves two fixpoints calling each other. We get stuck in the definition of this fixpoint.  The definition of 'a' and  a failure try are given below. Any suggestions are welcome. Thanks in advance.

Require Export String.

Require Import List.

Require Import ListSet.

Open Scope string_scope.

Open Scope list_scope.

Definition name:=string.

Inductive a : Set:=

|base_a : name -> a

|or_a : name -> list a -> a.

Definition a1 : a := base_a "a1".

Definition a2 : a := base_a "a2".

Definition a3 : a := or_a "a3" (a1 :: a2 :: nil).

Definition set_name_dec:forall (a b : set name) ,{a = b} + {a <> b}.

    repeat decide equality. 

Defined.

 

(* Hopefully,

 (Compute getName a3) should return:

 (a3::a1::nil)::(a3::a1::nil)::nil

*)

Fixpoint getNames (p : a) : set (set name) :=

match p with

|base_a n => (n::nil)::nil

|or_a n lp  => set_add set_name_dec (n::nil) (fix aux (l: list a): set (set name) :=

    match l with

        | nil => (n::nil)::nil

        | p :: tail => set_union set_name_dec (getNames p) (aux tail)

    end

end.