Adding the induction and destruct tactics.

6 files changed, 148 insertions, 5 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index b678b65b82..7e421c8577 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -17,6 +17,10 @@ open Proofview.Notations
 
 module Value = Tac2ffi
 
+let return x = Proofview.tclUNIT x
+let v_unit = Value.of_unit ()
+let thaw f = Tac2interp.interp_app f [v_unit]
+
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)
 | _ -> assert false
@@ -119,13 +123,28 @@ and to_intro_patterns il =
   let map ipat = Loc.tag (to_intro_pattern ipat) in
   Value.to_list map il
 
+let to_destruction_arg = function
+| ValBlk (0, [| c |]) ->
+  let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
+  ElimOnConstr c
+| ValBlk (1, [| id |]) -> ElimOnIdent (Loc.tag (Value.to_ident id))
+| ValBlk (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
+| _ -> assert false
+
+let to_induction_clause = function
+| ValBlk (0, [| arg; eqn; as_; in_ |]) ->
+  let arg = to_destruction_arg arg in
+  let eqn = Value.to_option (fun p -> Loc.tag (to_intro_pattern_naming p)) eqn in
+  let as_ = Value.to_option (fun p -> Loc.tag (to_or_and_intro_pattern p)) as_ in
+  let in_ = Value.to_option to_clause in_ in
+  ((None, arg), eqn, as_, in_)
+| _ ->
+  assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 
-let return x = Proofview.tclUNIT x
-let v_unit = Value.of_unit ()
-
 let lift tac = tac <*> return v_unit
 
 let wrap f =
@@ -134,8 +153,6 @@ let wrap f =
 let wrap_unit f =
   return () >>= fun () -> f (); return v_unit
 
-let thaw f = Tac2interp.interp_app f [v_unit]
-
 let define_prim0 name tac =
   let tac = function
   | [_] -> lift tac
@@ -245,6 +262,20 @@ let () = define_prim4 "tac_set" begin fun ev idopt c cl ->
   Tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
+let () = define_prim3 "tac_destruct" begin fun ev ic using ->
+  let ev = Value.to_bool ev in
+  let ic = Value.to_list to_induction_clause ic in
+  let using = Value.to_option to_constr_with_bindings using in
+  Tac2tactics.induction_destruct false ev ic using
+end
+
+let () = define_prim3 "tac_induction" begin fun ev ic using ->
+  let ev = Value.to_bool ev in
+  let ic = Value.to_list to_induction_clause ic in
+  let using = Value.to_option to_constr_with_bindings using in
+  Tac2tactics.induction_destruct true ev ic using
+end
+
 let () = define_prim1 "tac_red" begin fun cl ->
   let cl = to_clause cl in
   Tactics.reduce (Red false) cl
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 2590d7daed..439250db78 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -6,7 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Misctypes
+open Tactypes
 open Tactics
+open Proofview
 open Tacmach.New
 open Tacticals.New
 open Proofview.Notations
@@ -23,3 +26,21 @@ let apply adv ev cb cl =
   match cl with
   | None -> Tactics.apply_with_delayed_bindings_gen adv ev cb
   | Some (id, cl) -> Tactics.apply_delayed_in adv ev id cb cl
+
+type induction_clause =
+  EConstr.constr with_bindings tactic destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+let map_destruction_arg = function
+| ElimOnConstr c -> ElimOnConstr (delayed_of_tactic c)
+| ElimOnIdent id -> ElimOnIdent id
+| ElimOnAnonHyp n -> ElimOnAnonHyp n
+
+let map_induction_clause ((clear, arg), eqn, as_, occ) =
+  ((clear, map_destruction_arg arg), (eqn, as_), occ)
+
+let induction_destruct isrec ev ic using =
+  let ic = List.map map_induction_clause ic in
+  Tactics.induction_destruct isrec ev (ic, using)
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 86278f177e..f29793411a 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -16,3 +16,12 @@ open Proofview
 val apply : advanced_flag -> evars_flag ->
   EConstr.constr with_bindings tactic list ->
   (Id.t * intro_pattern option) option -> unit tactic
+
+type induction_clause =
+  EConstr.constr with_bindings tactic destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+val induction_destruct : rec_flag -> evars_flag ->
+  induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic
diff --git a/tests/example2.v b/tests/example2.v
index d89dcfd450..812f9172c9 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -61,3 +61,37 @@ Proof.
 econstructor 1.
 split.
 Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+induction &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+destruct &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall b1 b2, andb b1 b2 = andb b2 b1.
+Proof.
+intros b1 b2.
+destruct &b1 as [|], &b2 as [|]; split.
+Qed.
diff --git a/theories/Notations.v b/theories/Notations.v
index e7792c1555..20f01c3b48 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -96,3 +96,45 @@ Ltac2 Notation "apply"
   cb(list1(thunk(seq(constr, bindings)), ","))
   cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
   apply0 true false cb cl.
+
+Ltac2 induction0 ev ic use :=
+  let f ev use :=
+    let use := match use with
+    | None => None
+    | Some u =>
+      let ((_, c, wth)) := u in Some (c, wth)
+    end in
+    Std.induction ev ic use
+  in
+  enter_h ev f use.
+
+Ltac2 Notation "induction"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  induction0 false ic use.
+
+Ltac2 Notation "einduction"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  induction0 true ic use.
+
+Ltac2 destruct0 ev ic use :=
+  let f ev use :=
+    let use := match use with
+    | None => None
+    | Some u =>
+      let ((_, c, wth)) := u in Some (c, wth)
+    end in
+    Std.destruct ev ic use
+  in
+  enter_h ev f use.
+
+Ltac2 Notation "destruct"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  destruct0 false ic use.
+
+Ltac2 Notation "edestruct"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  destruct0 true ic use.
diff --git a/theories/Std.v b/theories/Std.v
index c2027e41c7..19bdc4c82a 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -107,6 +107,12 @@ Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_patter
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
 Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
 
+Ltac2 @ external destruct : evar_flag -> induction_clause list ->
+  constr_with_bindings option -> unit := "ltac2" "tac_induction".
+
+Ltac2 @ external induction : evar_flag -> induction_clause list ->
+  constr_with_bindings option -> unit := "ltac2" "tac_induction".
+
 Ltac2 @ external red : clause -> unit := "ltac2" "tac_red".
 Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf".
 Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv".