The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 28 Apr 2010 02:11:11 +0200, 
<harke AT cs.pdx.edu>
 a écrit:

> I suspect you can do it without having to resort to OCaml.
>
> If you want to see a concrete instance of what double induction does,
> take a proof and instead of invoking 'double induction m n' invoke
> 'info double induction m n'.  When I do that on an example with nats
> I see that double induction expands to 3 uses of nat_ind and some
> administrative stuff.

It doesn't mean you can program 'double induction' in Ltac;
in fact a lot tactic application expands to such things,
but for instance, even programming "induction" in Ltac is not easy
(except if you write "Ltac induction := induction." or so),
since given a type, you must make a good generalization and then
find the correct application to call
(nat_ind for nat, bool_ind for bool, etc...) and I am not sure it is
feasable in Ltac without using the induction tactic somewhere.

Furthermore, I think that if 'double induction' were so easy,
it should have been made in Ltac and not in OCaml

That said, the code for double induction seems rather simple,
and may be easily adapted IMO (see <trunk>/tactics/elim.ml[line 155/196]):


let induction_trailer abs_i abs_j bargs =
  tclTHEN
    (tclDO (abs_j - abs_i) intro)
    (onLastHypId
       (fun id gls ->
          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 hyps; tclTRY (clear ids);
             simple_elimination (mkVar id)])
          gls))

let double_ind h1 h2 gls =
  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
  (tclTHEN (tclDO abs_i intro)
     (onLastHypId
        (fun id ->
           elimination_then
             (introElimAssumsThen (induction_trailer abs_i abs_j))
             ([],[]) (mkVar id)))) gls

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


> Sorry I can't be more concrete.  The phrases double and triple induction
> are ambiguous.  What particular scheme did you have in mind?  Perhaps,
> if you need to do more than one triple induction you can prove that
> scheme as a lemma.  Perhaps functional induction is appropriate.
>
> On Mon, Apr 26, 2010 at 03:53:07PM -0400, M. Scott Doerrie wrote:
> > I need to perform triple induction in a similar way as double induction.
> > Is there a straightforward way to get this up and running in 8.2pl1, or
> > do I need to learn to write tactics in OCaml?  I'm looking at functional
> > induction and dependent induction, but can't seem to invoke them even
> > after importing the required libraries.
> >
> > Scott Doerrie

By the way, a probably well known stupid funny thing about induction:

Definition t_ind := True.
Inductive t : Prop := A | B.

doesn't compile... (but I don't know if one could whish it to compile,
as it may break induction tactic and other stuffs)


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay