The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> I have the following definition:
> 
>   Inductive comp_widening_chain (S : Set) : Set :=
>     comp_widening_chain_intro : forall x : S,
>       (forall y : S,
>         (option (comp_widening_chain S))) -> (comp_widening_chain S).
> 
> If I try to do reasonings by induction using the "induction" or "elim" 
> on such a datatype, I don't get an induction hypothesis.

  This is because "induction" and "elim" relies on the automatically
defined schemas "comp_widening_chain_rect", "comp_widening_chain_rec"
and "comp_widening_chain_ind" and the algorithm used to build these
schemas is not clever enough to know what to do with the "option"
type.

  You have to define the induction scheme by yourself, e.g. as follows:


Definition option_fold (A:Set) (B:Type) (f:A->B) (b:B) o :=
  match o with
  | None => b
  | Some x => f x
  end.

Implicit Arguments option_fold [A B].

Definition comp_widening_chain_rect'
  (S:Set)
  (P : comp_widening_chain S -> Type)
  (f : forall (x:S) (c: S -> option (comp_widening_chain S)),
       (forall y:S, option_fold P True (c y)) ->
       P (comp_widening_chain_intro S x c))
  :=
  fix F (c : comp_widening_chain S) : P c :=
    match c return (P c) with
    | comp_widening_chain_intro x d =>
      f x d (fun y => 
        match d y as z return option_fold P True z with
        | None => I
        | Some x => F x
        end)
    end.

and then use "induction ... using comp_widening_chain_rect'".


  Alternatively, using refine is a priori not a bad idea.


  Alternatively, you can redefine your inductive type as follows

Inductive comp_widening_chain_opt (S : Set) : Set :=
| comp_widening_chain_none : (comp_widening_chain_opt S)
| comp_widening_chain_some (x : S) :
   (forall y : S, comp_widening_chain_opt S) -> (comp_widening_chain_opt S).

Inductive comp_widening_chain (S : Set) : Set :=
  comp_widening_chain_intro : forall x : S,
    (forall y : S, comp_widening_chain_opt S) -> (comp_widening_chain S).

but that probably was not the objective.


  Best regards,

  Hugo Herbelin