Ltac splitb := apply/andP; split.

(* {JM} *)

From Ltac2 Require Import Ltac2.
From Ltac2 Require Bool Ltac1 List Option Control Ident.

Ltac not_subterm x t f :=
  match t with
  | context [x] => idtac
  | _ => f idtac
  end.

Ltac2 not_subterm x t f :=
  ltac1:(x t f |- not_subterm x t f) (Ltac1.of_ident x) (Ltac1.of_constr t) (Ltac1.lambda (fun t => f (); t)).

Ltac2 rec no_subterm_in_list l t f :=
  match l with
  | [] => f ()
  | x :: l =>
    not_subterm x t (fun () => no_subterm_in_list l t f)
  end.

Ltac2 clear_but1 l :=
  List.iter (fun (h, _, t) =>
    if Bool.neg (List.mem Ident.equal h l) then
      no_subterm_in_list l t (fun () => try (Std.clear [h]))
    else ()
  ) (List.rev (Control.hyps ())).

(* {JM}
   clear_except removes from the context every hypotheses excepts
   the listed ones and their requirements.. *)
Tactic Notation "clear_except" ident_list_sep(l, ",") :=
  let g := ltac2:(l |-
    Option.may (fun l =>
      let l := List.map_filter Ltac1.to_ident l in
      clear_but1 l
    ) (Ltac1.to_list l)) in
  g l.

(* {FP}
   dblib_by_cases simplifies goals in which a decidable integer comparison
   appears. *)

Ltac dblib_intro_case_clear :=
  let h := fresh in
  intro h; case h; clear h.

Ltac dblib_inspect_cases :=
  match goal with
  | |- context [le_gt_dec ?n ?n'] =>
      case (le_gt_dec n n')
  | h: context [le_gt_dec ?n ?n'] |- _ =>
      revert h; case (le_gt_dec n n'); intro h
  | |- context [eq_nat_dec ?n ?n'] =>
      case (eq_nat_dec n n')
  | h: context [eq_nat_dec ?n ?n'] |- _ =>
      revert h; case (eq_nat_dec n n'); intro h
  | |- context [(lt_eq_lt_dec ?n ?n')] =>
       case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]
  | h: context [(lt_eq_lt_dec ?n ?n')] |- _ =>
       revert h; case (lt_eq_lt_dec n n'); [ dblib_intro_case_clear | idtac ]; intro h
  end.

Ltac dblib_by_cases :=
  repeat dblib_inspect_cases; try solve [ intros; exfalso; lia ]; intros.

(* {FP}
   push h moves the hypothesis h into the goal. *)

Ltac push h :=
  generalize h; clear h.

(* {FP}
  ltac_Mark and ltac_mark are dummies. They are used as sentinels by
   certain tactics, to mark a position in the context or in the goal. *)

Inductive ltac_Mark : Type :=
| ltac_mark : ltac_Mark.

Ltac pop_until_mark :=
  match goal with
  | |- (ltac_Mark -> _) => intros _
  | _ => intro; pop_until_mark
  end.

Ltac injections :=
  (* Place an initial mark, so as to not disturb the goal. *)
  generalize ltac_mark;
  (* Look at every equality hypothesis. *)
  repeat match goal with
  | h: _ = _ |- _ =>
      (* Try to apply the primitive tactic injection to this hypothesis.
         If this succeeds, clear h and replace it with the results of
         injection. Another mark is used for this purpose. If this fails,
         just push h into the goal, as we do not wish to see it any more. *)
      first [
        generalize ltac_mark; injection h; clear h; pop_until_mark
      | push h ]
  end;
  (* Pop all of the hypotheses that have been set aside above. *)
  pop_until_mark.

(* {FP}
   The tactic unpack decomposes conjunctions and existential quantifiers
   in the hypotheses. Then, it attempts to perform substitutions, if possible. *)

Ltac unpack :=
  repeat match goal with
  | h: _ /\ _ |- _ =>
      destruct h
  | h: exists _, _ |- _ =>
      destruct h
  end;
  try subst.

Lemma f_ext_subst :
  forall (A: Type) (f g : nat -> A),
  (forall x : nat, f x = g x) -> f = g.
Proof.
  intros.
  apply functional_extensionality.
  assumption.
Qed.

Ltac f_ext := apply f_ext_subst.