Require Export HFS.Preliminaries.

Structure HF := HFS {
  set :> Type;
  eset : set;
  adj : set -> set -> set;
  hf_ind (p : set -> Type) : p eset -> (forall x y, p x -> p y -> p (adj x y)) -> forall x, p x;
  swap x y z : adj x (adj y z) = adj y (adj x z);
  cancel x y : adj x (adj x y) = adj x y;
  discrim x y : adj x y <> eset;
  member x y z : adj x (adj y z) = adj y z -> x = y \/ adj x z = z }.

Arguments eset {_}.

Notation "0" := eset.
Notation "x @ y" := (adj x y) (at level 65, right associativity). (* x.y *)
Notation "x 'el' y" := (x@y = y) (at level 70). (* x ∈ y *)
Notation "x 'nel' y" := (x@y <> y) (at level 70). (* x ∉ y *)
Notation "x '<<=' y" := (forall z, z el x -> z el y) (at level 70). (* x ⊆ y *)
Notation "'inhab' x" := (exists z, z el x) (at level 70).

Ltac hf_induction x :=
  pattern x; revert x; apply hf_ind.

Section HF.
  Variable X : HF.
  Implicit Types x y z : X.

  Example membership_law_matters :
    ((0:X) @ 0) @ 0 <> 0 @ 0.
  Proof.
    intros A. assert (A' := A).
    rewrite <- cancel in A'. rewrite A in A'.
    apply member in A' as [A'|A'].
    - now apply discrim in A'.
    - now apply discrim in A'.
  Qed.

  Fact eset_el z:
    z nel 0.
  Proof.
    intros [] %discrim.
  Qed.

  Fact adj_el x y z:
    z el x@y <-> z = x \/ z el y.
  Proof.
    split.
    - apply member.
    - intros [-> | A].
      + apply cancel.
      + rewrite swap. now rewrite A.
  Qed.

  Fact choose_el x :
    (x=0) + Sigma y, y el x.
  Proof.
    hf_induction x.
    - now left.
    - intros a x _ _. right. exists a. apply cancel.
  Qed.

  Fact nonempty x :
    x <> 0 <-> inhab x.
  Proof.
    destruct (choose_el x) as [-> |(a&A)]; split.
    - tauto.
    - intros (x&A). contradiction (eset_el A).
    - eauto.
    - intros _ ->. contradiction (eset_el A).
  Qed.

  Fact adj_incl x y z:
    x@y <<= z <-> x el z /\ y <<= z.
  Proof.
    split.
    - intros A. split.
      + apply A, cancel.
      + intros a B. apply A, adj_el. now right.
    - intros (A1&A2) a [-> |B] %adj_el; auto.
  Qed.

  Fact eset_incl x:
    x <<= 0 -> x = 0.
  Proof.
    hf_induction x.
    - auto.
    - intros a x _ _ A. exfalso.
      apply (@eset_el a). apply A, adj_el. auto.
  Qed.

  Definition trans x := forall z, z el x -> z <<= x.

End HF.