Require Export HFS.Tactics.
Section ExtDec.
Variable X: HF.
Implicit Types x y z a b: X.
Instance dec_0_eq y: dec (0 = y).
Proof.
hf_induction y; hfs.
Qed.
Instance dec_0_el y: dec (0 el y).
Proof.
hf_induction y; [hfs |].
intros a x _ [IHx|IHx]; decide (0 = a) as [-> |A]; hfs.
Qed.
Instance dec_0_incl y: dec (y <<= 0).
Proof.
hf_induction y; hfs.
Qed.
Lemma dec_adj_incl a x y:
dec (a el y) -> dec (x <<= y) -> dec (a@ x <<= y).
Proof.
intros [A|A] [B|B]; hfs.
Qed.
Lemma dec_adj_el y a x:
dec (y = a) -> dec (y el x) -> dec (y el a@x).
Proof.
intros [A|A] [B|B]; hfs.
Qed.
Fact dec_part a x:
(forall z, dec (a el z)) ->
(forall z, dec (a = z)) ->
a el x ->
Sigma u, x = a@u /\ a nel u.
Proof.
intros H H'. hf_induction x.
- hfs.
- intros b x _ IH A.
decide (a el x) as [B|B].
+ destruct (IH B) as (u&->&C).
assert (b el b @ a@u) by hfs.
decide (a=b) as [<-|D].
* exists u. hfs.
* exists (b@u). split. now apply swap.
contradict D. hfs.
+ exists x. hfs.
Qed.
Lemma dec_ext x y:
dec (x <<= y) * dec (y <<= x) *
dec (x el y) * dec (y el x) *
(x <<= y -> y <<= x -> x = y) *
dec (x = y).
Proof.
revert y.
hf_induction x.
- intuition; hfs.
- intros a x IHa IHx y.
hf_induction y.
+ intuition; hfs.
+ intros b y IHb IHy.
assert (C1: dec (a @ x <<= b @ y)).
{ apply dec_adj_incl. apply IHa. apply IHx. }
assert (C2: dec (b @ y <<= a @ x)).
{ apply dec_adj_incl. apply IHb. apply IHy. }
assert (C3: a @ x <<= b @ y -> b @ y <<= a @ x -> a @ x = b @ y).
{ intros A B.
assert (dec (a el x)) as [ax |nax] by apply IHa.
- rewrite ax in *. now apply IHx.
- destruct (@dec_part a (b@y)) as (u&H1&H2).
+ apply IHa.
+ apply IHa.
+ apply A. hfs.
+ rewrite H1 in *. f_equal. apply IHx; hfs. }
repeat split.
* apply C1.
* apply C2.
* apply dec_adj_el. apply IHb. apply IHy.
* apply dec_adj_el. apply dec_eq_sym, IHa. apply IHx.
* apply C3.
* { destruct C1 as [C1|C1].
- destruct C2 as [C2|C2].
+ left. now apply C3.
+ right. intros A. apply C2. rewrite A. auto.
- right. intros A. apply C1. rewrite A. auto. }
Qed.
Theorem extensionality x y :
(forall z, z el x <-> z el y) -> x = y.
Proof.
intros A. apply dec_ext; hfs.
Qed.
Global Instance dec_HF : eq_dec X.
Proof.
intros x y. apply dec_ext.
Qed.
Fact membership_dec x y:
dec (x el y).
Proof.
auto.
Qed.
Global Instance incl_dec x y :
dec (x <<= y).
Proof.
apply dec_ext.
Qed.
Global Instance hf_ex_dec x p (A : forall x, dec (p x)) :
dec (exists z, z el x /\ p z).
Proof.
hf_induction x.
- right. now intros (z& B%discrim& _).
- intros a x _ [IH|IH].
+ left. destruct IH as (z&A1&A2).
exists z. split. now rewrite swap, A1. assumption.
+ decide (p a) as [pa|npa].
* left. exists a. split. now apply cancel. assumption.
* right. intros (z&[-> |A1]%member&A2).
contradiction. apply IH. eauto.
Qed.
Global Instance hf_all_dec x p (A : forall x, dec (p x)) :
dec (forall z, z el x -> p z ).
Proof.
hf_induction x.
- left. now intros x B%discrim.
- intros a x _ [IH|IH].
+ decide (p a) as [pa|npa].
* left. intros z [-> |A1] % member.
assumption. now apply IH.
* right. intros B. apply npa, B, cancel.
+ right. intros B. apply IH. intros z C.
apply B. now rewrite swap, C.
Qed.
Lemma adj_nel x y z :
z nel x@y <-> z <> x /\ z nel y.
Proof.
rewrite adj_el, dec_DM_or. reflexivity. auto.
Qed.
Fact adj_el_strong x y z:
z el x@y -> (z = x) + (z <> x /\ z el y).
Proof.
intros A. decide (z = x) as [->|B].
- now left.
- right. apply adj_el in A. tauto.
Qed.
Fact part a x:
a el x -> Sigma u, x = a@u /\ a nel u.
Proof.
apply dec_part; auto.
Qed.
Inclusion ordering
Fact incl_refl x:
x <<= x.
Proof.
auto.
Qed.
Fact incl_trans x y z:
x <<= y -> y <<= z -> x <<= z.
Proof.
auto.
Qed.
Fact incl_antisym x y:
x <<= y -> y <<= x -> x = y.
Proof.
intros; apply extensionality; intuition.
Qed.
Epsilon induction
Fact eps_ind (p : X -> Type) :
(forall x, (forall z, z el x -> p z) -> p x) -> forall x, p x.
Proof.
intros A x. apply A. hf_induction x.
- hfs.
- intros a x IHa IHx z B % member.
decide (z=a) as [->|C].
+ auto.
+ apply IHx. tauto.
Qed.
Fact el_irrefl x :
x nel x.
Proof.
revert x. apply eps_ind.
intros x A B. apply (A x B B).
Qed.
Fact no_universal_set x:
~ (forall y, y el x).
Proof.
intros A. specialize (A x).
revert A. apply el_irrefl.
Qed.
Fact el_asym x y:
x el y -> y nel x.
Proof.
revert y. pattern x. revert x. apply eps_ind.
intros x IH z B C. revert B. now apply IH.
Qed.
Fact succ_inj x y:
x@x = y@y -> x = y.
Proof.
intros A.
assert (x el y@y) as B by (rewrite <- A; hfs).
assert (y el x@x) as C by (rewrite A; hfs).
apply member in B as [->|B]. reflexivity.
apply member in C as [->|C]. reflexivity.
contradiction (el_asym B C).
Qed.
End ExtDec.
Tactic Notation "extensio" "as" simple_intropattern(z) :=
apply extensionality; intros z.
Ltac epsilon_induction x :=
pattern x; revert x; apply eps_ind.
Without
Lemma without (X : HF) (x a : X) :
Sigma u, forall z, z el u <-> z el x /\ z <> a.
Proof.
decide (a el x) as [A|A].
- apply part in A as (u&->&B). exists u. hfs.
- exists x. hfs.
Qed.
Notation "x '\\' a" := (projT1 (without x a)) (at level 66).
Section Without.
Variable X: HF.
Implicit Types x y z a b: X.
Fact without_el x a z :
z el x\\a <-> z el x /\ z <> a.
Proof.
destruct (without x a) as (u&A). auto.
Qed.
Fact without_nin a x :
a nel x -> x\\a = x.
Proof.
intros A. extensio as z. rewrite without_el. hfs.
Qed.
Fact withoutA_eq a x:
(a@x)\\a = x\\a.
Proof.
extensio as z. rewrite !without_el. hfs.
Qed.
Fact withoutA_neq a b x :
a <> b -> (b@x)\\a = b@(x\\a).
Proof.
intros. extensio as z. rewrite adj_el, !without_el. hfs.
Qed.
End Without.