coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: "Shen Shixiong" <ssxtim AT 163.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] A problem about fixpoint
- Date: Fri, 16 Nov 2012 13:00:18 +0100
Le Fri, 16 Nov 2012 10:32:52 +0800 (CST),
"Shen Shixiong"
<ssxtim AT 163.com>
a écrit :
> 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.
You just have to add "(" and ") lp)" somewhere in your code.
- [Coq-Club] A problem about fixpoint, Shen Shixiong, 11/16/2012
- Re: [Coq-Club] A problem about fixpoint, AUGER Cédric, 11/16/2012
Archive powered by MHonArc 2.6.18.