The Coq mailing list

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

Hi,

I would not rely too much on "double induction" actually and I wonder
whether we should not remove it from the reference manual. Tactic
"double induction x y" is basically either "induction x; induction y"
or "induction y; induction x" depending on the order of x and y in the
goal + a useless regeneralization in the second induction of the
hypotheses introduced after x + a non very convenient naming policy of
variables (see analysis of the code below).

My experience is that the various kinds of "double induction" we may
commonly need are the following (in decreasing strength order):

(* Lexicographic induction *)

Variable P:nat->nat->Prop.
Variable H1 : P 0 0.
Variable H2 : forall n : nat, P 0 n -> P O (S n).
Variable H3 : forall m n : nat, (forall n, P m n) -> P (S m) O.
Variable H4 : forall m n : nat, P (S m) n -> (forall n, P m n) -> P (S m) (S 
n).

Goal forall m n, P m n.
induction m; induction n; auto using H1, H2, H3, H4.
  (* "double induction m n" also ok but adds detours *)

(* Double induction (a special case of lexicographic induction) *)
(* I'm not sure that the terminology "double" is actually standard *)

Variable P:nat->nat->Prop.
Variable H1 : P 0 0.
Variable H2 : forall m : nat, P m 0 -> P (S m) 0.
Variable H3 : forall n : nat, P 0 n -> P 0 (S n).
Variable H4 : forall m n : nat, P (S m) n -> P m (S n) -> P (S m) (S n).

Goal forall m n, P m n.
induction m; induction n; auto using H1, H2, H3, H4.
  (* "double induction m n" also ok but adds detours *)

(* Parallel induction (e.g. for proofs of equalities) *)

Variable P:nat->nat->Prop.
Variable H1 : P 0 0.
Variable H2 : forall n : nat, P O (S n).
Variable H3 : forall m : nat, P (S m) O.
Variable H4 : forall m n : nat, P m n -> P (S m) (S n).

Goal forall m n, P m n.
induction m; destruct n; auto using H1, H2, H3, H4.
  (* only one induction is needed *)

Depending on what you intend by "triple induction", the generalization
of one of the following situations will maybe fit your need. [Which
does not mean that Coq should not provide ad hoc version of the above
scheme: for instance, using "induction;induction" produces junk that
obsfucates the goal and it would be nice to have tactics that exactly
apply the induction one wants - not forgetting the "descente infinie"
approach]

Hugo Herbelin

======================================================================
Since Cedric Auger copied the code of "double induction x y", here a
some comments on it. Note also that "double induction" has been
written much before Ltac was introduced (last traces of it go back to
1997 while Ltac is from 2000).

(* induction_trailer performs the inner induction *)

> let induction_trailer abs_i abs_j bargs =
>   tclTHEN

(* we "intro" so that the second induction hypotheses comes on top of
   the context of hypotheses *)

>     (tclDO (abs_j - abs_i) intro)
>     (onLastHypId
>        (fun id gls ->

(* here is computed the set "hyps" of hypotheses introduced inbetween
   x and y and that do not occur in the type "fvty" of y (= "id") *)

>           let idty = pf_type_of gls (mkVar id) in
>           let fvty = global_vars (pf_env gls) idty in
>           let possible_bring_hyps =
>             (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
>           in
>           let (hyps,_) =
>             List.fold_left
>               (fun (bring_ids,leave_ids) (cid,_,cidty as d) ->
>                  if not (List.mem cid leave_ids)
>                  then (d::bring_ids,leave_ids)
>                  else (bring_ids,cid::leave_ids))
>               ([],fvty) possible_bring_hyps
>           in
>           let ids = List.rev (ids_of_named_context hyps) in
>           (tclTHENSEQ

(* bring_hyps regeneralize the goal with hyps (the reason why is unclear) *)

>             [bring_hyps hyps; tclTRY (clear ids);

(* simple_elimination does the inner induction *)

>              simple_elimination (mkVar id)])
>           gls))


> let double_ind h1 h2 gls =

(* We find which hypothesis is quantified first: *)

>   let abs_i = depth_of_quantified_hypothesis true h1 gls in
>   let abs_j = depth_of_quantified_hypothesis true h2 gls in
>   let (abs_i,abs_j) =
>     if abs_i < abs_j then (abs_i,abs_j) else
>     if abs_i > abs_j then (abs_j,abs_i) else
>       error "Both hypotheses are the same." in

(* We "intro" so that the first induction hypotheses comes on top of
   the context of hypotheses *)

>   (tclTHEN (tclDO abs_i intro)
>      (onLastHypId
>         (fun id ->

(* elimination_then tells to apply "induction" on id and to apply on
   each resulting subgoal the tactic "induction_trailer" *)

>            elimination_then
>              (introElimAssumsThen (induction_trailer abs_i abs_j))
>              ([],[]) (mkVar id)))) gls

(* "abstract_tactic" below is used for the "info" tactic so that a
   tactic possibly calling "double induction" will give "double
   induction" for "info" and not the code of "double induction" itself *)

> let h_double_induction h1 h2 =
>   Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2)