Require Export HFS.HF.

Module HFS.

Lemma forall_iff_L2R X P Q :
  (forall x:X, P x <-> Q x) -> forall x, P x -> Q x.
Proof.
  firstorder.
Qed.

Lemma forall_iff_R2L X P Q :
  (forall x:X, P x <-> Q x) -> forall x, Q x -> P x.
Proof.
  firstorder.
Qed.

Ltac not_in_context P :=
  match goal with
    |[_ : P |- _] => fail 1
    | _ => idtac
  end.

(* Extend context by proposition of  given proof. Fail if proposition is already in context. *)

Ltac extend H :=
  let A := type of H in not_in_context A; generalize H; intro.

Ltac Intro :=
  match goal with
  |[ |- _ -> _ ] => intro
  |[ |- _ /\ _ ] => split
  |[ |- _ <-> _] => split
  |[ |- ~ _ ] => intro
  |[ |- forall _, _ ] => intro
  |[ |- _ el _ @ _] => apply adj_el
  |[ |- inhab _] => apply nonempty
  |[ |- trans _] => hnf
  end.

Ltac Elim :=
  match goal with
  |[H: Sigma _, _ |- _ ] => destruct H
  |[H: exists _, _ |- _ ] => destruct H
  |[H: _ /\ _ |- _ ] => destruct H
  |[H: _ * _ |- _] => destruct H
  |[H: forall _, _ <-> _ |- _] => extend (forall_iff_L2R H); extend (forall_iff_R2L H); clear H
  |[H: ?P \/ ?Q |- _] => not_in_context P; not_in_context Q; destruct H
  |[H: ?P + ?Q |- _] => not_in_context P; not_in_context Q; destruct H
  |[H: _ @ _ = 0 |- _] => destruct (discrim H)
  |[H: 0 = _ @ _ |- _] => destruct (discrim (eq_sym H))
  |[H: _ el 0 |- _] => destruct (eset_el H)
  |[H: ?z el ?x @ _ |- _] => apply adj_el in H as [|]
  |[H: _ @ _ <<= _ |- _ ] => apply adj_incl in H as []
  |[H: _ <<= 0 |- _] => apply eset_incl in H as ->
  |[H: trans ?x, H': _ el ?x |- _] => extend (H _ H')
  end.

Ltac hfs n :=
  repeat progress (reflexivity || subst || Intro || Elim);
  try tauto;
  match n with
  |O => idtac
  |S ?n => match goal with
          |[ |- _ \/ _] => solve [left; hfs n | right; hfs n]
          |[ |- _ + _] => solve [left; hfs n | right; hfs n]
          |[ |- dec _] => solve [left; hfs n | right; hfs n]
          |[H: ?X |- exists x:?X, _ ] => exists H; hfs n
          |[H: forall x, x el ?z -> _, H': ?X el ?z |- _ ] => extend (H X H'); clear H; hfs n
          |[H: forall x, _ -> x el ?z |- _ el ?z] => apply H; hfs n
          |[H: ?x <<= _, H': ?z el ?x |- _ ] => extend (H z H'); clear H; hfs n
          end
  end.

End HFS.

Tactic Notation "hfs" := cbn; solve [HFS.hfs 7].