Set Implicit Arguments.
Unset Strict Implicit.
Require Export Sequent.
Require Export NaturalDeduction.
Require Export List.

Ltac REPLACE :=
  repeat apply replaceRoot || apply replaceRight || apply replaceLeft.

Inductive path : Set :=
  | r : path
  | l : path.

Fixpoint getTermByPath (Atoms : Set) (T : Term Atoms)
 (p : list path) {struct p} : option (Term Atoms) :=
  match T, p with
  | T, nil ⇒ Some T
  | OneForm _, p1 :: p2 ⇒ None (A:=Term Atoms)
  | Comma T1 T2, p1 :: p2 ⇒
      match p1 with
      | l ⇒ getTermByPath T1 p2
      | r ⇒ getTermByPath T2 p2
      end
  end.

Definition getDotForms (Atoms : Set) (T : Term Atoms) :
  option (Form Atoms × Form Atoms) :=
  match T with
  | OneForm A ⇒
      match A with
      | Dot A1 B1 ⇒ Some (A1, B1)
      | other ⇒ None (A:=Form Atoms × Form Atoms)
      end
  | other ⇒ None (A:=Form Atoms × Form Atoms)
  end.


Definition getSlashTerms (Atoms : Set) (T : Term Atoms) :
  option (Form Atoms × Form Atoms × Term Atoms) :=
  match T with
  | OneForm _ ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
  | Comma F1 Delta ⇒
      match F1 with
      | OneForm A1 ⇒
          match A1 with
          | Slash A B ⇒ Some (A, B, Delta)
          | other ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
          end
      | other ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
      end
  end.

Definition getBackSlashTerms (Atoms : Set) (T : Term Atoms) :
  option (Form Atoms × Form Atoms × Term Atoms) :=
  match T with
  | OneForm _ ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
  | Comma Delta F ⇒
      match F with
      | OneForm A1 ⇒
          match A1 with
          | Backslash B A ⇒ Some (B, A, Delta)
          | other ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
          end
      | other ⇒ None (A:=Form Atoms × Form Atoms × Term Atoms)
      end
  end.

Fixpoint replaceTermByTerm (Atoms : Set) (T Tr : Term Atoms)
 (p : list path) {struct p} : option (Term Atoms) :=
  match T, p with
  | _, nil ⇒ Some Tr
  | OneForm _, _ :: _ ⇒ None (A:=Term Atoms)
  | Comma T1 T2, p1 :: p2 ⇒
      match p1 with
      | l ⇒
          match replaceTermByTerm T1 Tr p2 with
          | None ⇒ None (A:=Term Atoms)
          | Some t ⇒ Some (Comma t T2)
          end
      | r ⇒
          match replaceTermByTerm T2 Tr p2 with
          | None ⇒ None (A:=Term Atoms)
          | Some t ⇒ Some (Comma T1 t)
          end
      end
  end.

Ltac leftSlashTac p :=
  match goal with
  | |- (gentzenSequent _ ?X11 _) ⇒
      match eval compute in (getTermByPath X11 p) with
      | None ⇒ idtac
      | (Some ?X1) ⇒
          match eval compute in (getSlashTerms X1) with
          | None ⇒ idtac
          | (Some (?X2, ?X3, ?X4)) ⇒
              match eval compute in (replaceTermByTerm X11 (OneForm X2) p) with
              | None ⇒ idtac
              | (Some ?X5) ⇒
                  apply LeftSlash with X4 X5 X2 X3;
                   [ REPLACE | idtac | idtac ]
              end
          end
      end
  | |- _ ⇒ idtac
  end.

Ltac leftBackSlashTac p :=
  match goal with
  | |- (gentzenSequent _ ?X11 _) ⇒
      match eval compute in (getTermByPath X11 p) with
      | None ⇒ idtac
      | (Some ?X1) ⇒
          match eval compute in (getBackSlashTerms X1) with
          | None ⇒ idtac
          | (Some (?X2, ?X3, ?X4)) ⇒
              match eval compute in (replaceTermByTerm X11 (OneForm X3) p) with
              | None ⇒ idtac
              | (Some ?X5) ⇒
                  apply LeftBackSlash with X4 X5 X3 X2;
                   [ REPLACE | idtac | idtac ]
              end
          end
      end
  | |- _ ⇒ idtac
  end.

Ltac leftDotTac p :=
  match goal with
  | |- (gentzenSequent _ ?X11 _) ⇒
      match eval compute in (getTermByPath X11 p) with
      | None ⇒ idtac
      | (Some ?X1) ⇒
          match eval compute in (getDotForms X1) with
          | None ⇒ idtac
          | (Some (?X2, ?X3)) ⇒
              match eval compute in
                    (replaceTermByTerm X11 (Comma (OneForm X2) (OneForm X3))
                       p) with
              | None ⇒ idtac
              | (Some ?X5) ⇒
                  apply LeftDot with X5 X2 X3; [ REPLACE | idtac | idtac ]
              end
          end
      end
  | |- _ ⇒ idtac
  end.

Ltac cutTac A p :=
  match goal with
  | |- (gentzenSequent _ ?X11 _) ⇒
      match eval compute in (getTermByPath X11 p) with
      | None ⇒ idtac
      | (Some ?X1) ⇒
          match eval compute in (replaceTermByTerm X11 (OneForm A) p) with
          | None ⇒ idtac
          | (Some ?X5) ⇒
              apply CutRule with X1 X5 A; [ REPLACE | idtac | idtac ]
          end
      end
  | |- _ ⇒ idtac
  end.

Inductive directionL : Set :=
  | LR : directionL
  | RL : directionL.

Definition getTreeL (Atoms : Set) (dl : directionL)
  (T : Term Atoms) : option (Term Atoms) :=
  match T with
  | OneForm _ ⇒ None (A:=Term Atoms)
  | Comma T1 T2 ⇒
      match dl with
      | LR ⇒
          match T1 with
          | OneForm _ ⇒ None (A:=Term Atoms)
          | Comma T3 T4 ⇒ Some (Comma T3 (Comma T4 T2))
          end
      | RL ⇒
          match T2 with
          | OneForm _ ⇒ None (A:=Term Atoms)
          | Comma T3 T4 ⇒ Some (Comma (Comma T1 T3) T4)
          end
      end
  end.

Ltac lSequentTac p d :=
  match goal with
  | |- (gentzenSequent L_Sequent ?X1 _) ⇒
      match eval compute in (getTermByPath X1 p) with
      | None ⇒ idtac
      | (Some ?X2) ⇒
          match eval compute in (getTreeL d X2) with
          | None ⇒ idtac
          | (Some ?X3) ⇒
              match eval compute in (replaceTermByTerm X1 X3 p) with
              | None ⇒ idtac
              | (Some ?X4) ⇒
                  apply SequentExtension with X4 X3 X2;
                   [ apply L_Intro_lr || apply L_Intro_rl | REPLACE | idtac ]
              end
          end
      end
  | |- _ ⇒ idtac
  end.

Ltac lNaturalTac p d :=
  match goal with
  | |- (natDed L_Sequent ?X1 _) ⇒
      match eval compute in (getTermByPath X1 p) with
      | None ⇒ idtac
      | (Some ?X2) ⇒
          match eval compute in (getTreeL d X2) with
          | None ⇒ idtac
          | (Some ?X3) ⇒
              match eval compute in (replaceTermByTerm X1 X3 p) with
              | None ⇒ idtac
              | (Some ?X4) ⇒
                  apply NatExt with X4 X3 X2;
                   [ apply L_Intro_lr || apply L_Intro_rl | REPLACE | idtac ]
              end
          end
      end
  | |- _ ⇒ idtac
  end.