The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello.

I am facing with the dilemma between 
an inductive definition and a parameteried definition.

Let me assume a function "good" of type Prop -> Prop 
and:

Inductive llist: list nat -> Prop :=
| llist_constr: forall i l,
  good (llist l) -> llist (i :: l).

For this inductive definition to be sound, good must satisfy 
the positivity condition for the argument. 
So it seems necessary to define good transparently,
like:

(* nonsense at all *)
Definition good (p:Prop) := True /\ p.

Yet, I prefer to keep good opaque, 
instead provide an axiom for unfolding:

Parameter good: Prop -> Prop.
Axiom good_unfold: forall (p:Prop), good p = True /\ p. 


In this way, I can control constants to be unfolded (delta-reduction) 
by conversion tactics, e.g. simpl.

I am able to 
1) avoid inductive definition of llist, or
2) restrict the use of simpl, or
3) apply "fold" to undo simpl's job a little. 
So this is not a crucial problem. 
But it would be much nicer if I can inductively define llist,
while still able to enjoy simpl.

Does someone have idea to break the situation?

With best,
Keiko