Library HF
Set theory without infinity axiom: hereditarily finite sets
Require Export Setoid Morphisms.
Require Import List.
Require Import Bool.
Lemma in_map_inv : ∀ (A B:Set) (f:A->B) x l,
In x (map f l) -> exists2 y, In y l & x = f y.
Inductive hf : Set := HF (elts : list hf).
Definition hf_elts (x:hf) := let (lx) := x in lx.
Lemma hf_elts_ext : ∀ x, HF (hf_elts x) = x.
Lemma hf_ind2 : ∀ P : hf -> Prop,
(∀ l, (∀ x, In x l -> P x) -> P (HF l)) ->
∀ x, P x.
Definition forall_elt P x :=
fold_right (fun y b => P y && b) true (hf_elts x).
Definition exists_elt P x :=
negb (forall_elt (fun x => negb (P x)) x).
Lemma forall_elt_case :
∀ P x,
forall_elt P x = true /\ (∀ y, In y (hf_elts x) -> P y = true) \/
forall_elt P x = false /\ (exists2 y, In y (hf_elts x) & P y = false).
Lemma forall_elt_true_intro :
∀ P x,
(∀ y, In y (hf_elts x) -> P y = true) ->
forall_elt P x = true.
Lemma forall_elt_false_intro :
∀ P y x,
In y (hf_elts x) ->
P y = false ->
forall_elt P x = false.
Lemma forall_elt_true_elim :
∀ P y x,
forall_elt P x = true ->
In y (hf_elts x) ->
P y = true.
Lemma forall_elt_false_elim :
∀ P x,
forall_elt P x = false ->
exists2 y, In y (hf_elts x) & P y = false.
Lemma exists_elt_true_intro :
∀ P y x,
In y (hf_elts x) ->
P y = true ->
exists_elt P x = true.
Lemma exists_elt_true_elim :
∀ P x,
exists_elt P x = true ->
exists2 y, In y (hf_elts x) & P y = true.
Equality
Fixpoint eq_hf (x y: hf) {struct x} : bool :=
forall_elt (fun x1 => exists_elt (fun y1 => eq_hf x1 y1) y) x &&
forall_elt (fun y1 => exists_elt (fun x1 => eq_hf x1 y1) x) y.
Definition Eq_hf x y := eq_hf x y = true.
Lemma eq_hf_intro :
∀ x y,
(∀ x', In x' (hf_elts x) ->
exists2 y', In y' (hf_elts y) & Eq_hf x' y') ->
(∀ y', In y' (hf_elts y) ->
exists2 x', In x' (hf_elts x) & Eq_hf x' y') ->
Eq_hf x y.
Lemma eq_hf_elim1 :
∀ x' x y,
Eq_hf x y ->
In x' (hf_elts x) ->
exists2 y', In y' (hf_elts y) & Eq_hf x' y'.
Lemma eq_hf_elim2 :
∀ y' x y,
Eq_hf x y ->
In y' (hf_elts y) ->
exists2 x', In x' (hf_elts x) & Eq_hf x' y'.
Instance eq_hf_refl : Reflexive Eq_hf.
Qed.
Instance eq_hf_sym : Symmetric Eq_hf.
Qed.
Instance eq_hf_trans : Transitive Eq_hf.
Qed.
Instance eq_hf_equiv : Equivalence Eq_hf. Qed.
Instance eq_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq bool) eq_hf.
Qed.
Membership
Definition in_hf (x y: hf) : bool := exists_elt (fun y1 => eq_hf x y1) y.
Definition In_hf x y := in_hf x y = true.
Lemma in_hf_intro : ∀ x x' y,
Eq_hf x x' ->
In x' (hf_elts y) ->
In_hf x y.
Lemma in_hf_elim : ∀ x y,
In_hf x y ->
exists2 x', In x' (hf_elts y) & Eq_hf x x'.
Lemma in_hf_reg_l: ∀ a a' b,
Eq_hf a a' -> In_hf a b -> In_hf a' b.
Lemma in_hf_reg_r :
∀ a x y,
Eq_hf x y ->
In_hf a x ->
In_hf a y.
Instance In_hf_morph : Proper (Eq_hf ==> Eq_hf ==> iff) In_hf.
Qed.
Instance in_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq _) in_hf.
Qed.
Lemma In_hf_head : ∀ x y l,
Eq_hf x y ->
In_hf x (HF (y::l)).
Lemma In_hf_tail : ∀ x y l,
In_hf x (HF l) ->
In_hf x (HF (y::l)).
Lemma In_hf_elim : ∀ x y l,
In_hf x (HF (y::l)) ->
Eq_hf x y \/ In_hf x (HF l).
Lemma In_app_left : ∀ x l1 l2,
In_hf x (HF l1) ->
In_hf x (HF (l1 ++ l2)).
Lemma In_app_right : ∀ x l1 l2,
In_hf x (HF l2) ->
In_hf x (HF (l1 ++ l2)).
Lemma In_app_elim : ∀ x l1 l2,
In_hf x (HF (l1 ++ l2)) ->
In_hf x (HF l1) \/ In_hf x (HF l2).
Definition incl_hf x y :=
forall_elt (fun x1 => in_hf x1 y) x.
Definition Incl_hf x y := ∀ a, In_hf a x -> In_hf a y.
Instance incl_hf_morph : Proper (Eq_hf ==> Eq_hf ==> iff) Incl_hf.
Qed.
Lemma incl_hf_sound : ∀ x y,
incl_hf x y = true -> Incl_hf x y.
Lemma incl_hf_complete : ∀ x y,
Incl_hf x y -> incl_hf x y = true.
Lemma Eq_hf_intro : ∀ x y,
Incl_hf x y -> Incl_hf y x -> Eq_hf x y.
Lemma Eq_hf_cons : ∀ x1 x2 l1 l2,
Eq_hf x1 x2 ->
Eq_hf (HF l1) (HF l2) ->
Eq_hf (HF (x1::l1)) (HF (x2::l2)).
Lemma Eq_hf_split : ∀ l1 l1' l2 l2',
Eq_hf (HF l1) (HF l1') ->
Eq_hf (HF l2) (HF l2') ->
Eq_hf (HF(l1++l2)) (HF(l1'++l2')).
Lemma hf_size_ind : ∀ (P:hf->Type) x,
P (HF nil) ->
(∀ x' y,
In_hf x' x ->
Incl_hf y x ->
P y -> P (HF(x'::hf_elts y))) ->
P x.
Cancelling redundancies
Lemma cancel_repeat : ∀ a l,
In_hf a (HF l) -> Eq_hf (HF(a::l)) (HF l).
Definition cons_hf x l := if in_hf x (HF l) then l else x :: l.
Lemma cons_hf_cons :
∀ x l, Eq_hf (HF(cons_hf x l)) (HF(cons x l)).
Lemma In_hf_head_hf : ∀ x y l,
Eq_hf x y ->
In_hf x (HF (cons_hf y l)).
Lemma In_hf_tail_hf : ∀ x y l,
In_hf x (HF l) ->
In_hf x (HF (cons_hf y l)).
Lemma In_hf_elim_hf : ∀ x y l,
In_hf x (HF (cons_hf y l)) ->
Eq_hf x y \/ In_hf x (HF l).
Lemma Eq_hf_cons_hf : ∀ x1 x2 l1 l2,
Eq_hf x1 x2 ->
Eq_hf (HF l1) (HF l2) ->
Eq_hf (HF (cons_hf x1 l1)) (HF (cons_hf x2 l2)).
Fixpoint app_hf (l1 l2:list hf) {struct l1} : list hf :=
match l1 with
nil => l2
| cons x l' => cons_hf x (app_hf l' l2)
end.
Lemma In_app_hf_left : ∀ x l1 l2,
In_hf x (HF l1) ->
In_hf x (HF (app_hf l1 l2)).
Lemma In_app_hf_right : ∀ x l1 l2,
In_hf x (HF l2) ->
In_hf x (HF (app_hf l1 l2)).
Lemma In_app_hf_elim : ∀ x l1 l2,
In_hf x (HF (app_hf l1 l2)) ->
In_hf x (HF l1) \/ In_hf x (HF l2).
Definition fold_set (X:Type) (f:hf->X->X) (x:hf) (acc:X) : X :=
let fix F (l:list hf) : X :=
match l with
nil => acc
| cons x l' => if in_hf x (HF l') then F l' else f x (F l')
end in
F (hf_elts x).
Lemma fold_set_unfold : ∀ X f x l acc,
fold_set X f (HF(x::l)) acc =
if in_hf x (HF l) then fold_set X f (HF l) acc
else f x (fold_set X f (HF l) acc).
Lemma fold_set_ind : ∀ X (P:hf->X->Prop) f x acc,
P (HF nil) acc ->
(∀ x' y acc, In_hf x' x -> In_hf x' y -> P y acc ->
P (HF(x'::hf_elts y)) acc) ->
(∀ x' y acc, In_hf x' x -> ~ In_hf x' y -> P y acc ->
P (HF(x'::hf_elts y)) (f x' acc)) ->
P x (fold_set X f x acc).
Fixpoint canonical (x:hf) : hf :=
HF (fold_set _ (fun y cl => canonical y :: cl) x nil).
Lemma canonical_correct : ∀ x, Eq_hf (canonical x) x.
Hint Resolve In_hf_head In_hf_head_hf In_hf_head_hf In_hf_tail_hf.
Notations
Notation "{ l }" := (HF l) (at level 0, l at level 99).
Notation EMPTY := {nil}.
Notation ONE := {EMPTY::nil}.
Notation TWO := {EMPTY::ONE::nil}.
Infix ":::" := cons_hf (at level 60, right associativity).
Infix "+++" := app_hf (at level 60, right associativity).
Notation "x ∈ y" := (In_hf x y) (at level 60).
Notation "x == y" := (Eq_hf x y) (at level 70).
Notation morph1 := (Proper (Eq_hf ==> Eq_hf)).
Notation morph2 := (Proper (Eq_hf ==> Eq_hf ==> Eq_hf)).
Notation morph3 := (Proper (Eq_hf ==> Eq_hf ==> Eq_hf ==> Eq_hf)).
Set theoretical operators
Definition empty := HF nil.
Definition singl x := HF (x:::nil).
Definition pair x y := HF (x:::y:::nil).
Definition union (x:hf) :=
HF (fold_set _ (fun y l => hf_elts y+++l) x nil).
Definition power (x:hf) :=
HF (fold_set _
(fun y pow p => pow p ++ pow (y::p)) x
(fun p => HF (rev p) :: nil) nil).
Definition subset (x:hf) (P:hf->bool) :=
HF (fold_set _ (fun y l => if P y then y :: l else l) x nil).
Definition repl (x:hf) (f:hf->hf) :=
HF (map f (hf_elts x)).
Instance singl_morph : morph1 singl.
Instance pair_morph : morph2 pair.
Definition eq_hf_fun (x:hf) (f1 f2:hf->hf) :=
∀ y1 y2, y1 ∈ x -> y1 == y2 -> f1 y1 == f2 y2.
Lemma eq_hf_fun_sym : ∀ x f1 f2,
eq_hf_fun x f1 f2 -> eq_hf_fun x f2 f1.
Lemma eq_hf_fun_trans : ∀ x f1 f2 f3,
eq_hf_fun x f1 f2 -> eq_hf_fun x f2 f3 -> eq_hf_fun x f1 f3.
Lemma eq_hf_fun_left : ∀ x f1 f2,
eq_hf_fun x f1 f2 -> eq_hf_fun x f1 f1.
Definition hf_pred_morph x P :=
∀ y1 y2, y1 ∈ x -> y1 == y2 -> P y1 = true -> P y2 = true.
Definition eq_hf_pred (x:hf) (f1 f2:hf->bool) :=
∀ y1 y2, y1 ∈ x -> y1 == y2 -> f1 y1 = f2 y2.
Lemma empty_elim : ∀ x, ~ x ∈ empty.
Lemma empty_ext : ∀ a, (∀ x, ~ x ∈ a) -> a == empty.
Lemma singl_intro : ∀ x y, x == y -> x ∈ singl y.
Lemma singl_elim : ∀ x a, x ∈ singl a -> x == a.
Lemma singl_ext :
∀ y x,
x ∈ y ->
(∀ z, z ∈ y -> z == x) ->
y == singl x.
Lemma pair_elim : ∀ x a b,
x ∈ pair a b -> x == a \/ x == b.
Lemma pair_intro1 : ∀ x a b, x == a -> x ∈ pair a b.
Lemma pair_intro2 : ∀ x a b, x == b -> x ∈ pair a b.
Lemma union_intro : ∀ x y z, x ∈ y -> y ∈ z -> x ∈ union z.
Lemma union_elim : ∀ x z, x ∈ union z -> exists2 y, x ∈ y & y ∈ z.
Lemma union_ext :
∀ u z,
(∀ x y, x ∈ y -> y ∈ z -> x ∈ u) ->
(∀ x, x ∈ u -> exists2 y, x ∈ y & y ∈ z) ->
u == union z.
Instance union_morph : morph1 union.
Qed.
Lemma union_singl : ∀ x, union (singl x) == x.
power properties
Lemma power_intro :
∀ x y, Incl_hf x y -> x ∈ power y.
Lemma power_elim : ∀ x y z, x ∈ power y -> z ∈ x -> z ∈ y.
Lemma power_ext :
∀ p a,
(∀ x, (∀ y, y ∈ x -> y ∈ a) -> x ∈ p) ->
(∀ x y, x ∈ p -> y ∈ x -> y ∈ a) ->
p == power a.
Lemma power_morph : morph1 power.
Lemma subset_intro_gen : ∀ a (P:hf->bool) x,
x ∈ a -> (∀ x', x==x' -> P x' = true) -> x ∈ subset a P.
Lemma subset_intro : ∀ a (P:hf->bool) x,
hf_pred_morph a P ->
x ∈ a -> P x = true -> x ∈ subset a P.
Lemma subset_elim1 : ∀ a (P:hf->bool) x, x ∈ subset a P -> x ∈ a.
Lemma subset_elim2_gen : ∀ a (P:hf->bool) x,
x ∈ subset a P ->
exists2 x', x==x' & P x' = true.
Lemma subset_elim2 : ∀ a (P:hf->bool) x,
hf_pred_morph a P ->
x ∈ subset a P ->
P x = true.
Lemma subset_ext :
∀ s a (P:hf->bool),
hf_pred_morph a P ->
(∀ x, x ∈ a -> P x = true -> x ∈ s) ->
(∀ x, x ∈ s -> x ∈ a) ->
(∀ x, x ∈ s -> P x = true) ->
s == subset a P.
Lemma subset_morph_ext : ∀ x1 x2 y1 y2,
x1 == x2 -> eq_hf_pred x1 y1 y2 -> subset x1 y1 == subset x2 y2.
Lemma subset_empty1 : ∀ P, subset empty P == empty.
Lemma subset_singl : ∀ x a (P:hf->bool),
x ∈ a ->
P x = true ->
(∀ x', x' ∈ a -> (x==x' <-> P x' = true)) ->
subset a P == singl x.
replacement properties
Lemma repl_intro : ∀ a f y x,
eq_hf_fun a f f ->
y ∈ a -> x == f y -> x ∈ repl a f.
Lemma repl_elim : ∀ a f x,
eq_hf_fun a f f ->
x ∈ repl a f -> exists2 y, y ∈ a & x == f y.
Lemma repl_ext : ∀ x a f,
eq_hf_fun a f f ->
(∀ y, y ∈ a -> f y ∈ x) ->
(∀ y, y ∈ x -> exists2 z, z ∈ a & y == f z) ->
x == repl a f.
Lemma repl_morph :
∀ x1 x2 f1 f2,
x1 == x2 ->
eq_hf_fun x1 f1 f2 ->
repl x1 f1 == repl x2 f2.
bool
Definition hf_false := empty.
Definition hf_true := singl hf_false.
Definition hf_bool := pair hf_false hf_true.
Definition hf_true := singl hf_false.
Definition hf_bool := pair hf_false hf_true.
couples
Definition couple x y := pair (singl x) (pair x y).
Definition fst p := union (subset (union p) (fun x => in_hf (singl x) p)).
Definition snd p :=
union (subset (union p) (fun y => eq_hf (pair (fst p) y) (union p))).
Lemma union_couple_eq : ∀ a b, union (couple a b) == pair a b.
Instance couple_morph : morph2 couple.
Qed.
Instance fst_morph : morph1 fst.
Qed.
Lemma fst_def : ∀ x y, fst (couple x y) == x.
Instance snd_morph : morph1 snd.
Qed.
Lemma snd_def : ∀ x y, snd (couple x y) == y.
Lemma snd_ext : ∀ p x y,
p == couple x y ->
y == snd p.
Definition fst p := union (subset (union p) (fun x => in_hf (singl x) p)).
Definition snd p :=
union (subset (union p) (fun y => eq_hf (pair (fst p) y) (union p))).
Lemma union_couple_eq : ∀ a b, union (couple a b) == pair a b.
Instance couple_morph : morph2 couple.
Qed.
Instance fst_morph : morph1 fst.
Qed.
Lemma fst_def : ∀ x y, fst (couple x y) == x.
Instance snd_morph : morph1 snd.
Qed.
Lemma snd_def : ∀ x y, snd (couple x y) == y.
Lemma snd_ext : ∀ p x y,
p == couple x y ->
y == snd p.
regularity