Require Export "axioms".

Set Implicit Arguments.
Unset Strict Implicit.

Module Tactics1.
Ltac ir := intros.

Ltac rw u := rewrite u.
Ltac rwi u h := rewrite u in h.

Ltac wr u := rewrite <- u.
Ltac wri u h := rewrite <- u in h.

Ltac ap h := apply h.


Ltac am := assumption.

Ltac au := first [ solve [ am ] | auto ].
Ltac eau := eauto.
Ltac tv := trivial.
Ltac sy := symmetry in |- *.

Ltac uf u := unfold u in |- *. Ltac ufi u h := unfold u in h.

Ltac nin h := induction h.

Ltac CompareTac a b :=
  assert (toclear : a = a); [ exact (refl_equal b) | clear toclear ].

Ltac UnfoldHead1 h :=
  match constr:h with
  | (?X1 ?X2) => unfold X1 in h
  | _ => fail
  end.

Ltac Good_Unfold g h :=
  match constr:g with
  | inc => fail
  | _ => unfold g in h
  end.

Ltac Unfold_Head_R g h :=
  match constr:g with
  | (?X1 _ _ _ _ _ _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _ _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _ _) => Good_Unfold X1 h
  | (?X1 _ _ _) => Good_Unfold X1 h
  | (?X1 _ _) => Good_Unfold X1 h
  | (?X1 _) => Good_Unfold X1 h
  | ?X1 => Good_Unfold X1 h
  end.

Ltac Unfold_Head h :=
  match goal with
  | id1:?X1 |- _ => CompareTac id1 h; Unfold_Head_R X1 h
  | _ => fail
  end.

Ltac Exploit h :=
  match goal with
  | id1:?X1 |- _ =>
      CompareTac id1 h; assert X1; [ am | Unfold_Head h; Exploit h ]
  | _ => idtac
  end.

Ltac xlt h := Exploit h.

Definition DONE (A : Type) (a : A) := a.
Definition TODO (A : Type) (a : A) := a.

Ltac TodoAll :=
  match goal with
  | id1:?X1 |- _ =>
      match constr:X1 with
      | (TODO _) => fail
      | _ => change (TODO X1) in id1; TodoAll
      end
  | _ => idtac
  end.

Definition CheckProp (P : Prop) := P.

Ltac CheckPropTac P := assert (toclear : CheckProp P); [ am | clear toclear ].

Notation E1 := (E -> E).
Notation E2 := (E -> E1).
Notation E3 := (E -> E2).
Notation E4 := (E -> E3).
Notation E5 := (E -> E4).
Notation E6 := (E -> E5).

Notation EP := (E -> Prop).
Notation E2P := (E -> EP).
Notation E3P := (E -> E2P).
Notation E4P := (E -> E3P).

Definition A := and.
Infix "&":= and (right associativity, at level 100).

Ltac Deconj :=
  match goal with
  | |- (A _ _) => unfold A in |- *; ap conj; [ Deconj | Deconj ]
  | |- (_ & _) => ap conj; [ Deconj | Deconj ]
  | |- (and _ _) => ap conj; [ Deconj | Deconj ]
  | |- (_ /\ _) => ap conj; [ Deconj | Deconj ]
  | |- _ => au
  end.

Ltac EasyDeconj :=
  match goal with
  | |- (A _ _) => unfold A in |- *; ap conj; [ EasyDeconj | EasyDeconj ]
  | |- (_ & _) => ap conj; [ EasyDeconj | EasyDeconj ]
  | |- (and _ _) => ap conj; [ EasyDeconj | EasyDeconj ]
  | |- (_ /\ _) => ap conj; [ EasyDeconj | EasyDeconj ]
  | |- _ => idtac
  end.

Ltac Expand :=
  match goal with
  | id1:(A ?X1 ?X2) |- _ =>
      unfold A in id1; nin id1; Expand
  | id1:(?X1 & ?X2) |- _ => nin id1; Expand
  | id1:(and ?X1 ?X2) |- _ => nin id1; Expand
  | id1:(?X1 /\ ?X2) |- _ => nin id1; Expand
  | |- _ => Deconj
  end.

Ltac Remind u :=
  set (recalx := u);
   match goal with
   | recalx:?X1 |- _ => assert X1; [ exact recalx | clear recalx ]
   end.

Ltac cp := Remind.

Ltac EasyExpand :=
  match goal with
  | id1:(A ?X1 ?X2) |- _ =>
      unfold A in id1; nin id1; EasyExpand
  | id1:(?X1 /\ ?X2) |- _ => nin id1; EasyExpand
  | id1:(?X1 /\ ?X2) |- _ => nin id1; EasyExpand
  | |- _ => EasyDeconj
  end.

Ltac ee := EasyExpand.

Ltac xd := Expand.

Ltac PreExplode n :=
  match constr:n with
  | 0 => idtac
  | (S ?X1) =>
      match goal with
      | id1:?X2 |- _ =>
          CheckPropTac X2;
           match constr:X2 with
           | (DONE ?X3) => fail
           | _ =>
               assert (DONE X2);
                [ unfold DONE in |- *; am
                | Unfold_Head id1; EasyExpand; PreExplode X1 ]
           end
      | _ => idtac
      end
  end.

Ltac ClearDone :=
  match goal with
  | id1:(DONE ?X1) |- _ => unfold DONE in id1; ClearDone
  | _ => idtac
  end.

Ltac Exp := PreExplode 5; ClearDone.
Ltac Expl := PreExplode 10; ClearDone.
Ltac Explode := PreExplode 100; ClearDone.

Ltac CleanUp :=
  match goal with
  | id1:?X1,id2:?X1 |- _ => CheckPropTac X1; clear id2; CleanUp
  | _ => idtac
  end.

Ltac xde := Explode.
Ltac cx := Explode; CleanUp.


Ltac sh x := first
 [ ap nonemptyT_intro; exact x
 | apply ex_intro with x
 | apply ex_intro with x
 | apply nonempty_intro with x ].

Lemma seq_deconj : forall P Q : Prop, P -> (P -> Q) -> (P & Q).
ir. xd. Qed.

Ltac dj :=
  match goal with
  | |- (A ?X1 ?X2) => ap seq_deconj; ir; dj
  | |- (?X1 & ?X2) => ap seq_deconj; ir; dj
  | _ => idtac
  end.

Ltac MiddleDeconj :=
  match goal with
  | |- (A _ _) =>
      unfold A in |- *; ap conj; [ MiddleDeconj | MiddleDeconj ]
  | |- (_ /\ _) => ap conj; [ MiddleDeconj | MiddleDeconj ]
  | |- (_ /\ _) => ap conj; [ MiddleDeconj | MiddleDeconj ]
  | |- _ => first
  [ solve [ trivial | am | sy; am ] | idtac ]
  end.

Ltac MiddleExpand :=
  match goal with
  | id1:(A ?X1 ?X2) |- _ =>
      unfold A in id1; nin id1; MiddleExpand
  | id1:(?X1 /\ ?X2) |- _ => nin id1; MiddleExpand
  | id1:(?X1 /\ ?X2) |- _ => nin id1; MiddleExpand
  | |- _ => MiddleDeconj
  end.

Ltac xe := MiddleExpand.

Definition type_of (T : Type) (t : T) := T.

Ltac Copy a :=
  assert (type_of a);
   [ exact a | match goal with
               | id1:(type_of _) |- _ => ufi type_of id1
               end ].

Ltac ufk a b := Copy b; ufi a b. Ltac uh a := red in a.

Ltac uhg := red in |- *.

Ltac util a:=
match (type of a) with
| (?X1 -> ?X2 -> ?X3 -> ?X4 -> ?X5 -> ?X6) => assert X6; [apply a |idtac]
| (?X1 -> ?X2 -> ?X3 -> ?X4 -> ?X5) => assert X5; [apply a |idtac]
| (?X1 -> ?X2 -> ?X3 -> ?X4) => assert X4; [apply a |idtac]
| (?X1 -> ?X2 -> ?X3) => assert X3; [apply a |idtac]
| (?X1 -> ?X2) => assert X2; [apply a |idtac]
| _ => fail
end.

Lemma uneq : forall (f:E1) x y,
x = y -> f x = f y.
Proof.
ir. rw H; tv.
Qed.

Ltac LookUpErasing :=
match goal with
| id1 : ?X1 |- _ =>
first [exact id1 | uh id1; ee; try tv; try am|clear id1 ]
| _ => fail
end.

Ltac lu :=
LookUpErasing; lu.

Ltac app u :=
(ap u; try tv; try am).

Ltac rww u :=
(rw u; try tv; try am).

Ltac wrr u :=
(wr u; try tv; try am).

Ltac orbr t :=
match goal with
| |- (_ \/ _) =>
  solve [ap or_introl; (orbr t) | ap or_intror; (orbr t)]
| _ => t
end.

Lemma orbr_test : False \/ False \/ True \/ False \/ False.
Proof.
orbr tv.
Qed.

Module PWclear.
Ltac pw1 := fail.
Ltac pw2 := fail.
Ltac pw3 := fail.
Ltac pw4 := fail.
Ltac pw5 := fail.
Ltac pw6 := fail.
Ltac pw7 := fail.
Ltac pw8 := fail.
Ltac pw9 := fail.
Ltac pw10 := fail.
Ltac pw11 := fail.
Ltac pw12 := fail.
Ltac pw13 := fail.
Ltac pw14 := fail.
Ltac pw15 := fail.

End PWclear.

Ltac aw :=
autorewrite with aw; try tv; try am.

Lemma forup : forall A B (f g:A -> B) (a b : A),
f = g -> a = b -> f a = g b.
Proof.
ir. rw H0. rw H. tv.
Qed.

Ltac up :=
apply forup with (A:= E); try tv; try am; try up.

End Tactics1.
Export Tactics1.