From Undecidability Require Import TM.Util.Prelim TM.Util.TM_facts.
From Undecidability.TM Require Import Lifting.LiftTapes CodeTM ChangeAlphabet. (* for simpl_not_in *)

(* * Tactics that help verifying complex machines *)

(* This tactic automatically solves/instantiates premises of a hypothesis. If the hypothesis is a conjunction, it is destructed. *)
Ltac modpon' H :=
  simpl_surject;
  once lazymatch type of H with
  | forall (i : Fin.t _), ?P => idtac
  | forall (x : ?X), ?P =>
    once lazymatch type of X with
    | Prop =>
      tryif spec_assert H by
          (simpl_surject;
           solve [ eauto
                 | contains_ext
                 | isVoid_mono
                 ]
          )
      then idtac (* "solved premise of type" X *);
           modpon' H
      else (spec_assert H;
            [ idtac (* "could not solve premise" X *) (* new goal for the user *)
            | modpon' H (* continue after the user has proved the premise manually *)
            ]
           )
    | _ =>
      (* instantiate variable x with evar *)
      let x' := fresh "x" in
      evar (x' : X); specialize (H x'); subst x';
      modpon' H
    end
  | ?X /\ ?Y =>
    let H' := fresh H in
    destruct H as [H H']; modpon' H; modpon' H'
  | _ => idtac
  end.

Ltac modpon H := progress (modpon' H).

Ltac dec_pos P := let H := fresh in destruct (Dec P) as [_ | H]; [ | now contradiction H].
Ltac dec_neg P := let H := fresh in destruct (Dec P) as [H | _]; [now contradiction H | ].

Ltac simpl_dec :=
  match goal with
  | [ H : context [ Dec (?x = ?x) ] |- _ ] => dec_pos (x=x)
  | [ |- context [ Dec (?x = ?x) ]] => dec_pos (x=x)
  | [ _ : ?H |- context [ Dec ?H ]] => dec_pos H
  | [ _ : ~ ?H |- context [ Dec ?H ]] => dec_neg H
  | [ _ : ?H, _ : context [ Dec ?H ] |- _] => dec_pos H
  | [ _ : ~ ?H, _ : context [ Dec ?H ] |- _] => dec_neg H
  | _ => fail "could not match goal"
  end.

Section test.
  Variable P : Prop.
  Variable dec_P : dec P.
  Goal if Dec (1 = 1) then True else False.
  Proof.
    intros. deq 1. tauto.
  Qed.
  Goal P -> if (Dec P) then True else False.
  Proof.
    intros. simpl_dec. tauto.
  Qed.
  Goal ~ P -> if (Dec P) then False else True.
  Proof.
    intros. simpl_dec. tauto.
  Qed.
  Goal P -> (if (Dec P) then False else True) -> False.
  Proof.
    intros. simpl_dec. tauto.
  Qed.
  Goal ~ P -> (if (Dec P) then True else False) -> False.
  Proof.
    intros. simpl_dec. tauto.
  Qed.
End test.

Ltac inv_pair :=
  once lazymatch goal with
  | [ H : (_, _) = (_, _) |- _] => inv H
  | [ |- (_, _) = (_, _) ] => f_equal
  end.

Ltac destruct_param_tape_pair :=
  once lazymatch goal with
  | [ x : _ * tapes _ _ |- _] =>
    let ymid := fresh "ymid" in
    let tmid := fresh "tmid" in
    destruct x as (ymid&tmid)
  end.

Ltac destruct_unit :=
  repeat once lazymatch goal with
         | [ x : unit |- _ ] => destruct x
         end.

(* Rewrite eq-assumptions, but only in the goal. This is much faster than TMSimp. *)
Ltac TMSimp_goal :=
  repeat multimatch goal with
         | [ H : ?X = _ |- _ ] => rewrite H
         end.

Fixpoint all_vec {X:Type} {n:nat} {struct n}: (Vector.t X n -> Prop) -> Prop :=
  match n with
      0 => fun A => A (@Vector.nil _)
    | S n => fun A => forall x, all_vec (fun xs => A (x:::xs))
  end.

Lemma all_vec_correct {X:Type} {n:nat} (P : Vector.t X n -> Prop):
  all_vec P -> forall xs, P xs.
Proof.
  revert P. induction n;cbn;intros. now apply Vector.case0.
  intros. apply Vector.caseS'. intro. now eapply IHn.
Qed.
Lemma all_vec_correct2 {X:Type} {n:nat} (P : Vector.t X n -> Prop):
(forall xs, P xs) -> all_vec P.
Proof.
  revert P. induction n;cbn;intros. now apply Vector.case0. eauto.
Qed.

Tactic Notation "vector_destruct" hyp(tin) :=
  let rec introT n :=
      once lazymatch n with
      | S ?n =>
        let x := fresh tin "_0" in
        intro x;introT n
      | 0 => try clear tin
      | _ => simple apply all_vec_correct2;try clear tin;let tin' := fresh tin in intros tin'
      end
  in
  let tac n := revert dependent tin; refine (all_vec_correct _);
    cbn [all_vec];introT n;cbn [Vector.nth Vector.caseS];intros
  in
    once lazymatch type of tin with
      tapes _ ?n => tac n
    | Vector.t _ ?n => tac n
    end.

Lemma eq_nth_iff' X n (v w : Vector.t X n):
(forall i : Fin.t n, v[@i] = w[@i]) -> v = w.
Proof. intros. eapply Vector.eq_nth_iff. now intros ? ? ->. Qed.

Ltac TMSimp1 T :=
  try destruct_param_tape_pair; destruct_unit;
  simpl_not_in;
  cbn in *;
  repeat match goal with
  | [ H : ?x = _ |- _ ] => is_var x;move x at bottom;subst x
  | [ H : _ = ?x |- _ ] => is_var x;move x at bottom;symmetry in H;subst x
  | [ H : (forall i : Fin.t _, _[@i] = _[@i]) |- _ ] => apply eq_nth_iff' in H
  end;
  unfold finType_CS in *;
  try T;
  repeat
  once lazymatch goal with
  | [ x : unit |- _ ] => destruct x
  | [ H : _ ::: _ = [| |] |- _ ] => discriminate H
  | [ H : [| |] = _ ::: _ |- _ ] => discriminate H
  | [ H : _ ::: _ = _ ::: _ |- _ ] => apply VectorSpec.cons_inj in H

  | [ H : _ :: _ = [] |- _ ] => discriminate H
  | [ H : [] = _ :: _ |- _ ] => discriminate H
  | [ H : _ :: _ = _ :: _ |- _ ] => inv H


  | [ H : Some _ = Some _ |- _ ] => inv H
  | [ H : None = Some _ |- _ ] => discriminate H
  | [ H : Some _ = None |- _ ] => discriminate H

  | [ H : _ /\ _ |- _] => destruct H
  | [ H : @ex ?A ?P |- _] =>
    once lazymatch A with
    | tapes _ _ =>
      let tmid := fresh "tmid" in
      destruct H as (tmid&H)
    | _ => (* probably some label *)
      let ymid := fresh "ymid" in
      destruct H as (ymid&H)
    end
  | [ x : _ * _ |- _ ] => destruct x
  end.

  Ltac TMSimp2 :=
  let tac ts n :=
    once lazymatch n with
      S _ => vector_destruct ts
    end
  in
    once match goal with
    | [ ts: tapes _ ?n|- _ ] => tac ts n
    | [ ts: Vector.t _ ?n|- _ ] => tac ts n
    | [H : @Vector.nil _ = @Vector.nil _ |-_ ] => clear H
    end.

Tactic Notation "TMSimp" tactic(T) :=
  repeat progress (repeat progress TMSimp1 T; repeat TMSimp2; unlock all).

Tactic Notation "TMSimp" := TMSimp idtac.

(* DO NOT USE THE FOLLOWING (deprecated) TACTICS, except in TM.Compound! *)

Tactic Notation "TMBranche" :=
  (
    match goal with
    | [ H : context [ match ?x with _ => _ end ] |- _ ] => let E := fresh "E" in destruct x eqn:E
    | [ |- context [ match ?x with _ => _ end ] ] => let E := fresh "E" in destruct x eqn:E
    | [ H : _ \/ _ |- _] => destruct H
    | [ IH : ?P -> ?Q |- _] =>
      match type of P with
      | Prop => spec_assert IH; [ clear IH | ]
      end

    | [ x : bool |- _ ] => destruct x
    | [ x : option _ |- _ ] => destruct x

    | [ |- ex ?P ] => eexists
    | [ H : _ \/ _ |- _] => destruct H
    end
  ).

Tactic Notation "TMSolve" int_or_var(k) :=
  repeat progress first [
           match goal with
           | [ |- (_ ::: _) = (_ ::: _) ] => f_equal
           | [ |- Some _ = Some _ ] => f_equal
           | [ |- _ /\ _ ] => split
           end
           || congruence
           || eauto k
         ].

Tactic Notation "TMCrush" tactic(T) :=
  repeat progress
         (
           TMSimp T;
           try TMBranche
         ).

Tactic Notation "TMCrush" :=
  repeat progress
         (
           TMSimp;
           try TMBranche
         ).