Require Import List.
Require Import Permutation.

From Undecidability.Shared.Libs.DLW.Utils Require Import focus utils_tac.

Ltac focus_g x ll :=
  let rr := focus_lst x ll
  in cutrewrite ( ll = rr );
      [ idtac | solve_list_eq ].

Ltac focus_g_2 x ll :=
  let rr := focus_lst_2 x ll
  in cutrewrite ( ll = rr );
      [ idtac | solve_list_eq ].

Ltac focus_g_3 x ll :=
  let rr := focus_lst_3 x ll
  in cutrewrite ( ll = rr );
      [ idtac | solve_list_eq ].

Ltac focus_h H x ll :=
  let rr := focus_lst x ll
  in cutrewrite ( ll = rr ) in H;
      [ idtac | solve_list_eq ].

Ltac focus_h_2 H x ll :=
  let rr := focus_lst_2 x ll
  in cutrewrite ( ll = rr ) in H;
      [ idtac | solve_list_eq ].

Ltac focus_h_3 H x ll :=
  let rr := focus_lst_3 x ll
  in cutrewrite ( ll = rr ) in H;
      [ idtac | solve_list_eq ].

Ltac focus_goal x ll :=
  match type of x with
    | list _ => focus_g x ll
    | _ => focus_g (x::nil) ll
  end.

Ltac focus_goal_2 x ll :=
  match type of x with
    | list _ => focus_g_2 x ll
    | _ => focus_g_2 (x::nil) ll
  end.

Ltac focus_goal_3 x ll :=
  match type of x with
    | list _ => focus_g_3 x ll
    | _ => focus_g_3 (x::nil) ll
  end.

Ltac focus_hyp H x ll :=
  match type of x with
    | list _ => focus_h H x ll
    | _ => focus_h H (x::nil) ll
  end.

Ltac focus_hyp_2 H x ll :=
  match type of x with
    | list _ => focus_h_2 H x ll
    | _ => focus_h_2 H (x::nil) ll
  end.

Ltac focus_hyp_3 H x ll :=
  match type of x with
    | list _ => focus_h_3 H x ll
    | _ => focus_h_3 H (x::nil) ll
  end.

Ltac chg_goal x :=
  match goal with
    | |- context[?hh] => match type of hh with list _ => focus_goal x hh end
  end.

Ltac chg_goal_2 x :=
  match goal with
    | |- context[?hh] => match type of hh with list _ => focus_goal_2 x hh end
  end.

Ltac chg_goal_3 x :=
  match goal with
    | |- context[?hh] => match type of hh with list _ => focus_goal_3 x hh end
  end.

Ltac chg_hyp H x :=
  let gg := fresh
  in match goal with
       |- ?G => set (gg := G)
     end;
     generalize H;
     match goal with
       | |- context[?hh] => intros _;
                            match type of hh with
                              | list _ => focus_hyp H x hh
                            end
     end;
     unfold gg;
     clear gg.

Ltac chg_hyp_2 H x :=
  let gg := fresh
  in match goal with
       |- ?G => set (gg := G)
     end;
     generalize H;
     match goal with
       | |- context[?hh] => intros _;
                            match type of hh with
                              | list _ => focus_hyp_2 H x hh
                            end
     end;
     unfold gg;
     clear gg.

Ltac chg_hyp_3 H x :=
  let gg := fresh
  in match goal with
       |- ?G => set (gg := G)
     end;
     generalize H;
     match goal with
       | |- context[?hh] => intros _;
                            match type of hh with
                              | list _ => focus_hyp_3 H x hh
                            end
     end;
     unfold gg;
     clear gg.

Tactic Notation "focus" constr(X) := chg_goal X.
Tactic Notation "focus" constr(X) "in" hyp(H) := chg_hyp H X.

Tactic Notation "focus" constr(X) "at" "2" := chg_goal_2 X.
Tactic Notation "focus" constr(X) "in" hyp(H) "at" "2" := chg_hyp_2 H X.

Tactic Notation "focus" constr(X) "at" "3" := chg_goal_3 X.
Tactic Notation "focus" constr(X) "in" hyp(H) "at" "3" := chg_hyp_3 H X.