The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello, this is a very usual question: you need a correct induction
principle to prove this the one created automatically is not good
enough.

The reason is that you use (list (... s ...)) in the types of
constructors of s. This kind of definition is ok but the induction
principle of s is not powerful enough to reason correctly on s. There
are two solutions:

1) replace list (...s...)
 by a inductive type that is mutual with s.

2) prove a correct induction principle for your current version of s.

There are explanations on this issue here:

* Coq'art section 14.3.3
* http://adam.chlipala.net/cpdt/html/InductiveTypes.html#lab32 .

Hope this helps,
Pierre Courtieu

2014-04-22 1:28 GMT+02:00 窦亮 
<ldou AT cs.ecnu.edu.cn>:
> Hi guys, I have the following definition for a complicate inductive type s:
>
> Definition name := string.
> Definition lname := list string.
> Definition pname := lname * lname.
>
> Inductive s : Type :=
> |basic_s : name -> pname -> s
> |complex_s : name -> list s -> nat ->
>          list (name * s * set name * name * lname * set name * s * name) ->
>          pname -> s
> |complex_s2 : name -> set s -> pname -> s
> .
>
> Definition t := name * s * set name * name * lname * set name * s * name.
> ----------------------
> you can see i rename a part of "complex_s" as t for better reference.
> My question is i don't know how to finish the proof for the decidable
> equality definition for t and s:
> ---------------------------
> Definition s_dec : forall (a b : s) ,{a = b} + {a <> b}.
>
> Definition t_dec : forall (a b : t) ,{a = b} + {a <> b}.