HyPre.util.ExperimentalTac

From HyPre Require Export
  Tac.

Lemma move_all_quantor_in1 {X : Type} (P : Type) (Q : X -> Prop)
  : (forall x : X, P -> Q x) <-> (P -> forall x, Q x).
Proof.
  clear.
  firstorder.
Qed.

Ltac move_Q_in1 H :=
  match type of H with
  | forall (x : ?P), ?Q -> ?R => rewrite (move_all_quantor_in1 Q) in H
  end.

Goal (forall x, 1 = 2 -> x = 2) -> 1 = 2 -> forall x : nat, x = 2.
  clear.
  intro.
  move_Q_in1 H.
  exact H.
Qed.

Lemma move_all_quantor_in2 {X1 X2 : Type} (P : X1 -> Type) (Q : X1 -> X2 -> Prop)
  : (forall (x1 : X1) (x2 : X2), P x1 -> Q x1 x2) <-> (forall x1, P x1 -> forall x2, Q x1 x2).
Proof.
  clear.
  firstorder.
Qed.

Lemma move_all_quantor_in3 {X1 X2 X3 : Type} (P : X1 -> X2 -> Type) (Q : X1 -> X2 -> X3 -> Prop)
  : (forall (x1 : X1) (x2 : X2) (x3 : X3), P x1 x2 -> Q x1 x2 x3)
    <-> (forall x1 x2, P x1 x2 -> forall x3, Q x1 x2 x3).
Proof.
  clear.
  firstorder.
Qed.

Lemma move_all_quantor_in4 {X1 X2 X3 X4 : Type} (P : X1 -> X2 -> X3 -> Type) (Q : X1 -> X2 -> X3 -> X4 -> Prop)
  : (forall (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4), P x1 x2 x3 -> Q x1 x2 x3 x4)
    <-> (forall x1 x2 x3, P x1 x2 x3 -> forall x4, Q x1 x2 x3 x4).
Proof.
  clear.
  firstorder.
Qed.

Lemma move_all_quantor_in5
  {X1 X2 X3 X4 X5: Type}
  (P : X1 -> X2 -> X3 -> X4 -> Type)
  (Q : X1 -> X2 -> X3 -> X4 -> X5 -> Prop)
  : (forall (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5), P x1 x2 x3 x4 -> Q x1 x2 x3 x4 x5)
    <-> (forall x1 x2 x3 x4, P x1 x2 x3 x4 -> forall x5, Q x1 x2 x3 x4 x5).
Proof.
  clear.
  firstorder.
Qed.

Lemma move_all_quantor_in6
  {X1 X2 X3 X4 X5 X6 : Type}
  (P : X1 -> X2 -> X3 -> X4 -> X5 -> Type)
  (Q : X1 -> X2 -> X3 -> X4 -> X5 -> X6 -> Prop)
  : (forall (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5) (x6 : X6),
        P x1 x2 x3 x4 x5 -> Q x1 x2 x3 x4 x5 x6)
    <-> (forall x1 x2 x3 x4 x5, P x1 x2 x3 x4 x5 -> forall x6, Q x1 x2 x3 x4 x5 x6).
Proof.
  clear.
  firstorder.
Qed.

Ltac move_Q_in2 H :=
  match type of H with
  | forall (x1 : ?X1) (x2 : ?X2), ?P -> ?Q => rewrite (move_all_quantor_in2) in H
  end.

Goal (forall x y, 1 = x -> y = 2) -> forall x, 1 = x -> forall y : nat, y = 2.
  clear.
  intro.
  move_Q_in2 H.
  exact H.
Qed.

Goal (forall x y, x = y -> y = 2)
     -> forall x y : nat, x = y -> y = 2.
  clear.
  intro.
  Fail move_Q_in2 H.
  exact H.
Qed.

Goal (forall x y : nat, 1 = 2 -> x = y)
     -> 1 = 2 -> forall x y : nat, x = y.
  clear.
  intro.
  move_Q_in2 H.
  move_Q_in1 H.
  exact H.
Qed.

Goal (forall x y : nat, 1 = 2 -> 1 = 2)
     -> 1 = 2 -> forall x y : nat, 1 = 2.
  clear.
  intro.
  move_Q_in2 H.
  move_Q_in1 H.
  exact H.
Qed.

Goal (forall x y z : nat, 1 = 2 -> x = y)
     -> forall x1 : nat, nat -> forall x2 : nat, 1 = 2 -> x1 = x2.
  clear.
  intro.
  move_Q_in2 H.
  exact H.
Qed.

Goal (forall x y z : nat, 1 = 2 -> x = y + z)
     -> forall x y z : nat, 1 = 2 -> x = y + z.
  clear.
  intro.
  Fail move_Q_in2 H.
  exact H.
Qed.

(* move_Q_in assumes that quantors are given in the order of their use.
   if so, it can move them in as long as the preconditions are independent of them.
   if the order of the quantors is not consistent to the order of their use you'll get stuck.
 *)
Ltac move_Q_in H :=
  lazymatch type of H with
  | ?P -> ?Q
    => fail
  | forall (x : ?P), ?Q -> ?R
    => rewrite (move_all_quantor_in1 Q) in H
  | forall (x1 : ?X1) (x2 : ?X2), ?P -> ?Q
    => rewrite (move_all_quantor_in2) in H
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3), ?P -> ?Q
    => rewrite (move_all_quantor_in3) in H
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4), ?P -> ?Q
    => rewrite (move_all_quantor_in4) in H
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4) (x5 : ?X5), ?P -> ?Q
    => rewrite (move_all_quantor_in5) in H
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4) (x5 : ?X5) (x6 : ?X6), ?P -> ?Q
    => rewrite (move_all_quantor_in6) in H
  end.

Goal (forall x y : nat, 1 = 2 -> x = y)
     -> 1 = 2 -> forall x y : nat, x = y.
  clear.
  intro.
  move_Q_in H.
  move_Q_in H.
  exact H.
Qed.

Goal (forall x y : nat, 1 = 2 -> x = y)
     -> 1 = 2 -> forall x y : nat, x = y.
  clear.
  intro.
  repeat move_Q_in H.
  exact H.
Qed.

Goal (forall x y : nat, 1 = 2 -> x = y -> 1 = 1)
     -> 1 = 2 -> forall x y : nat, x = y -> 1 = 1.
  clear.
  intro.
  repeat move_Q_in H.
  exact H.
Qed.

Goal (forall x, 1 = 2 -> x = 2) -> 1 = 2 -> forall x : nat, x = 2.
  clear.
  intro.
  move_Q_in H.
  exact H.
Qed.

Goal (forall x1 x2 x3 x4 x5 x6 : nat, 1 = 2 -> x1 = x2 + x3 + x4 + x5 + x6)
     -> 1 = 2 -> forall x x2 x3 x4 x5 x6 : nat, x = x2 + x3 + x4 + x5 + x6.
  clear.
  intro.
  repeat move_Q_in H.
  exact H.
Qed.

(* note, that x1 cannot be moved in,
   because x2 & x3 (which are both used in the second term) are blocking it
   this is unfortunately a severe limitation,
   because section variables always appear first and may not be used early in assumptions
 *)
Goal (forall x1 x2 x3 x4 x5 x6 : nat, x2 = x3 -> x1 = x2 + x3 + x4 + x5 + x6)
     -> forall x1 x2 x3 : nat, x2 = x3 -> forall x4 x5 x6 : nat, x1 = x2 + x3 + x4 + x5 + x6.
  clear.
  intro.
  repeat move_Q_in H.
  exact H.
Qed.

(* WIP exploit2
   the goal is that this tactic may be applicable when I have complicated assumption,
   with forall-quantors and preconditions,
   that it may simplify this assumption by proving all the trivially in context available preconditions
   and specializing the existential variables accordingly
 *)
Ltac exploit2' H :=
  let p := fresh "Q" in
  let y := fresh "y" in
  lazymatch type of H with
  | ?P -> ?Q => assert P as p;
              [now eauto|specialize (H p);clear p]
  | forall (x : ?X), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists x : X, P) as p;
                 [now (eexists;eapply T)| clear p]
                )
          then specialize (H _ T)
          else fail
      end
  | forall (x1 : ?X1) (x2 : ?X2), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists (x1 : X1) (x2 : X2), P) as p;
                 [now ((do 2 eexists);eapply T)| clear p]
                )
          then specialize (H _ _ T)
          else fail
      end
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists (x1 : X1) (x2 : X2) (x3 : X3), P) as p;
                 [now ((do 3 eexists);eapply T)| clear p]
                )
          then specialize (H _ _ _ T)
          else fail
      end
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4), P) as p;
                 [now ((do 4 eexists);eapply T)| clear p]
                )
          then specialize (H _ _ _ _ T)
          else fail
      end
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4) (x5 : ?X5), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5), P) as p;
                 [now ((do 5 eexists);eapply T)| clear p]
                )
          then specialize (H _ _ _ _ _ T)
          else fail
      end
  | forall (x1 : ?X1) (x2 : ?X2) (x3 : ?X3) (x4 : ?X4) (x5 : ?X5) (x6 : ?X6), ?P -> ?Q
    => match goal with
        [T : _ |- _]
        => tryif (assert (exists (x1 : X1) (x2 : X2) (x3 : X3) (x4 : X4) (x5 : X5) (x6 : X6), P) as p;
                 [now ((do 6 eexists);eapply T)| clear p]
                )
          then specialize (H _ _ _ _ _ _ T)
          else fail
      end
  end.

Ltac exploit2 H :=
  repeat ((repeat move_Q_in H); exploit2' H); repeat move_Q_in H.

Goal forall y, (forall x : nat, y = x -> x = y) -> y = 1 -> 1 = y.
  clear.
  intros.
  exploit2' H.
  exact H.
Qed.

Goal forall y, (forall x : nat, y = 1 -> x = y) -> y = 1 -> forall x : nat, x = y.
  clear.
  intros ? ? ?.
  move_Q_in H.
  exploit2' H.
  exact H.
Qed.

Goal forall y, (forall x : nat, y = 1 -> x = y) -> y = 1 -> forall x : nat, x = y.
  clear.
  intros ? ? ?.
  exploit2 H.
  exact H.
Qed.

Goal forall y, (forall x z : nat, x = z -> x = y) -> y = 1
          -> y = y.
  clear.
  intros ? ? ?.
  exploit2 H.
  exact H.
Qed.