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.