Creating a dedicated ltac/ folder for Hightactics.

1 files changed, 0 insertions, 225 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
deleted file mode 100644
index 7d0df2f52..000000000
--- a/tactics/eqdecide.ml
+++ /dev/null
@@ -1,225 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(************************************************************************)
-(*                              EqDecide                               *)
-(*   A tactic for deciding propositional equality on inductive types   *)
-(*                           by Eduardo Gimenez                        *)
-(************************************************************************)
-
-open Errors
-open Util
-open Names
-open Namegen
-open Term
-open Declarations
-open Tactics
-open Tacticals.New
-open Auto
-open Constr_matching
-open Hipattern
-open Tacmach.New
-open Coqlib
-open Proofview.Notations
-
-(* This file containts the implementation of the tactics ``Decide
-   Equality'' and ``Compare''. They can be used to decide the
-   propositional equality of two objects that belongs to a small
-   inductive datatype --i.e., an inductive set such that all the
-   arguments of its constructors are non-functional sets.
-
-   The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as
-   follows:
-   1. Eliminate x and then y.
-   2. Try discrimination to solve those goals where x and y has
-      been introduced by different constructors.
-   3. If x and y have been introduced by the same constructor,
-      then analyse one by one the corresponding pairs of arguments.
-      If they are equal, rewrite one into the other. If they are
-      not, derive a contradiction from the injectiveness of the
-      constructor.
-   4. Once all the arguments have been rewritten, solve the remaining half
-      of the disjunction by reflexivity.
-
-   Eduardo Gimenez (30/3/98).
-*)
-
-let clear ids = Proofview.V82.tactic (clear ids)
-let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
-
-let choose_eq eqonleft =
-  if eqonleft then
-    left_with_bindings false Misctypes.NoBindings
-  else
-    right_with_bindings false Misctypes.NoBindings
-let choose_noteq eqonleft =
-  if eqonleft then
-    right_with_bindings false Misctypes.NoBindings
-  else
-    left_with_bindings false Misctypes.NoBindings
-
-let mkBranches c1 c2 =
-  tclTHENLIST
-    [Proofview.V82.tactic (generalize [c2]);
-     Simple.elim c1;
-     intros;
-     onLastHyp Simple.case;
-     clear_last;
-     intros]
-
-let solveNoteqBranch side =
-  tclTHEN (choose_noteq side)
-    (tclTHEN introf
-      (onLastHypId (fun id -> Extratactics.discrHyp id)))
-
-(* Constructs the type {c1=c2}+{~c1=c2} *)
-
-let make_eq () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-
-let mkDecideEqGoal eqonleft op rectype c1 c2 =
-  let equality    = mkApp(make_eq(), [|rectype; c1; c2|]) in
-  let disequality = mkApp(build_coq_not (), [|equality|]) in
-  if eqonleft then mkApp(op, [|equality; disequality |])
-  else mkApp(op, [|disequality; equality |])
-
-
-(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
-
-let idx = Id.of_string "x"
-let idy = Id.of_string "y"
-
-let mkGenDecideEqGoal rectype g =
-  let hypnames = pf_ids_of_hyps g in
-  let xname    = next_ident_away idx hypnames
-  and yname    = next_ident_away idy hypnames in
-  (mkNamedProd xname rectype
-     (mkNamedProd yname rectype
-        (mkDecideEqGoal true (build_coq_sumbool ())
-          rectype (mkVar xname) (mkVar yname))))
-
-let rec rewrite_and_clear hyps = match hyps with
-| [] -> Proofview.tclUNIT ()
-| id :: hyps ->
-  tclTHENLIST [
-    Equality.rewriteLR (mkVar id);
-    clear [id];
-    rewrite_and_clear hyps;
-  ]
-
-let eqCase tac =
-  tclTHEN intro (onLastHypId tac)
-
-let diseqCase hyps eqonleft =
-  let diseq  = Id.of_string "diseq" in
-  let absurd = Id.of_string "absurd" in
-  (tclTHEN (intro_using diseq)
-  (tclTHEN (choose_noteq eqonleft)
-  (tclTHEN (rewrite_and_clear (List.rev hyps))
-  (tclTHEN  (red_in_concl)
-  (tclTHEN  (intro_using absurd)
-  (tclTHEN  (Simple.apply (mkVar diseq))
-  (tclTHEN  (Extratactics.injHyp absurd)
-            (full_trivial []))))))))
-
-open Proofview.Notations
-
-(* spiwack: a small wrapper around [Hipattern]. *)
-
-let match_eqdec c =
-  try Proofview.tclUNIT (match_eqdec c)
-  with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
-
-(* /spiwack *)
-
-let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
-| [], [] ->
-  tclTHENLIST [
-    choose_eq eqonleft;
-    rewrite_and_clear (List.rev hyps);
-    intros_reflexivity;
-  ]
-| a1 :: largs, a2 :: rargs ->
-  Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl a1 in
-  let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
-  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
-  let subtacs =
-    if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
-    else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
-  (tclTHENS (elim_type decide) subtacs)
-  end }
-| _ -> invalid_arg "List.fold_right2"
-
-let solveEqBranch rectype =
-  Proofview.tclORELSE
-    begin
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
-        match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
-          let (mib,mip) = Global.lookup_inductive rectype in
-          let nparams   = mib.mind_nparams in
-          let getargs l = List.skipn nparams (snd (decompose_app l)) in
-          let rargs   = getargs rhs
-          and largs   = getargs lhs in
-          solveArg [] eqonleft op largs rargs
-      end }
-    end
-    begin function (e, info) -> match e with
-      | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
-      | e -> Proofview.tclZERO ~info e
-    end
-
-(* The tactic Decide Equality *)
-
-let hd_app c = match kind_of_term c with
-  | App (h,_) -> h
-  | _ -> c
-
-let decideGralEquality =
-  Proofview.tclORELSE
-    begin
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let concl = pf_nf_concl gl in
-        match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
-        let headtyp = hd_app (pf_compute gl typ) in
-        begin match kind_of_term headtyp with
-        | Ind (mi,_) -> Proofview.tclUNIT mi
-        | _ -> tclZEROMSG (Pp.str"This decision procedure only works for inductive objects.")
-        end >>= fun rectype ->
-          (tclTHEN
-             (mkBranches c1 c2)
-             (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
-      end }
-    end
-    begin function (e, info) -> match e with
-      | PatternMatchingFailure ->
-          Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
-      | e -> Proofview.tclZERO ~info e
-    end
-
-let decideEqualityGoal = tclTHEN intros decideGralEquality
-
-let decideEquality rectype =
-  Proofview.Goal.enter { enter = begin fun gl ->
-  let decide = mkGenDecideEqGoal rectype gl in
-  (tclTHENS (cut decide) [default_auto;decideEqualityGoal])
-  end }
-
-
-(* The tactic Compare *)
-
-let compare c1 c2 =
-  Proofview.Goal.enter { enter = begin fun gl ->
-  let rectype = pf_unsafe_type_of gl c1 in
-  let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
-  (tclTHENS (cut decide)
-            [(tclTHEN  intro
-             (tclTHEN (onLastHyp simplest_case) clear_last));
-             decideEquality rectype])
-  end }