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 : ∀ 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 : ∀ (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 : ∀ 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.