The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

What is happening here with the following two definitions? As you can  
see, the elimination operator for stuff1 provides for a proper  
inductive hypothesis, but stuff2 doesn't. For some reason, Coq  
doesn't derive the proper scheme for using the 'induction' tactic if  
I have an occurrence of the inductive type being described combined  
with 'and' or 'exists', for example? Is there an easy way in general  
to get this to be defined properly? My inductive definitions are  
actually a lot more complex than these: the occurrence of the  
recursive definition is under an implication, exists, and conjunction.

Thanks in advance for your help/ideas/clarification!

--- nadeem


Inductive stuff1 : Prop :=
  | s1a : stuff1
  | s1b : True -> stuff1 -> stuff1.

Inductive stuff2 : Prop :=
  | s2a : stuff2
  | s2b : True /\ stuff2 -> stuff2.

Print stuff1_ind.

(*
stuff1_ind =
fun (P : Prop) (f : P) (f0 : True -> stuff1 -> P -> P) =>
fix F (s : stuff1) : P :=
  match s with
  | s1a => f
  | s1b t s0 => f0 t s0 (F s0)
  end
     : forall P : Prop, P -> (True -> stuff1 -> P -> P) -> stuff1 -> P
*)

Print stuff2_ind.

(*
stuff2_ind =
fun (P : Prop) (f : P) (f0 : True /\ stuff2 -> P) (s : stuff2) =>
match s with
| s2a => f
| s2b x => f0 x
end
     : forall P : Prop, P -> (True /\ stuff2 -> P) -> stuff2 -> P
*)

(* I can define my own elimination scheme by hand; does this make  
sense? *)
Definition stuff2_myind
  : forall P : Prop, P -> (True /\ stuff2 -> P -> P) -> stuff2 -> P
    := fun (P : Prop) (f : P) (f0 : True /\ stuff2 -> P -> P) =>
fix F (s : stuff2) : P :=
  match s with
  | s2a => f
  | s2b X => match X with conj t s0 => f0 (conj t s0) (F s0) end
  end.

(* then I could potentially use 'elim H using stuff2_myind.' as a
   tactic instead of just induction H,  where (H:stuff2) ? *)