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.
Proof.
induction l; simpl in |- *; intros.
elim H.
destruct H.
exists a; auto.
elim IHl; intros; trivial.
exists x0; auto.
Qed.
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.
destruct x; reflexivity.
Qed.
Lemma hf_ind2 : ∀ P : hf -> Prop,
(∀ l, (∀ x, In x l -> P x) -> P (HF l)) ->
∀ x, P x.
Proof.
intros P Pnode.
fix hf_ind 1.
destruct x.
apply Pnode.
induction elts; simpl in |- *; intros.
elim H.
destruct H.
elim H.
apply hf_ind.
apply IHelts; trivial.
Qed.
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).
Proof.
unfold forall_elt in |- *.
destruct x as (lx); simpl.
induction lx; simpl in |- *; intros.
left.
split; trivial.
destruct 1.
elimtype (P a = true \/ P a = false); intros.
rewrite H; simpl in |- *.
elim IHlx; intros.
left.
destruct H0; split; trivial.
destruct 1; auto.
elim H2; auto.
right.
destruct H0.
split; auto.
destruct H1.
exists x; auto.
rewrite H; simpl in |- *.
right.
split; auto.
exists a; auto.
destruct (P a); auto.
Qed.
Lemma forall_elt_true_intro :
∀ P x,
(∀ y, In y (hf_elts x) -> P y = true) ->
forall_elt P x = true.
intros.
elim forall_elt_case with P x; intros.
destruct H0; trivial.
destruct H0.
destruct H1.
rewrite (H _ H1) in H2; discriminate.
Qed.
Lemma forall_elt_false_intro :
∀ P y x,
In y (hf_elts x) ->
P y = false ->
forall_elt P x = false.
intros.
elim forall_elt_case with P x; intros.
destruct H1.
rewrite (H2 _ H) in H0; discriminate.
destruct H1; trivial.
Qed.
Lemma forall_elt_true_elim :
∀ P y x,
forall_elt P x = true ->
In y (hf_elts x) ->
P y = true.
intros.
elim forall_elt_case with P x; intros.
destruct H1; auto.
destruct H1.
rewrite H1 in H; discriminate.
Qed.
Lemma forall_elt_false_elim :
∀ P x,
forall_elt P x = false ->
exists2 y, In y (hf_elts x) & P y = false.
intros.
elim forall_elt_case with P x; intros.
destruct H0.
rewrite H0 in H; discriminate.
destruct H0; trivial.
Qed.
Lemma exists_elt_true_intro :
∀ P y x,
In y (hf_elts x) ->
P y = true ->
exists_elt P x = true.
intros.
unfold exists_elt in |- *.
rewrite forall_elt_false_intro with (fun x => negb (P x)) y x; trivial.
rewrite H0; trivial.
Qed.
Lemma exists_elt_true_elim :
∀ P x,
exists_elt P x = true ->
exists2 y, In y (hf_elts x) & P y = true.
intros.
elim forall_elt_false_elim with (fun x => negb (P x)) x; intros.
exists x0; trivial.
rewrite <- (negb_elim (P x0)).
rewrite H1; trivial.
fold (negb true) in |- *.
apply negb_sym; trivial.
symmetry in |- *; trivial.
Qed.
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.
Proof.
unfold Eq_hf.
destruct x as (lx); simpl; intros.
apply andb_true_intro; split; apply forall_elt_true_intro; intros.
elim H with (1 := H1); intros.
apply exists_elt_true_intro with x; auto.
elim H0 with (1 := H1); intros.
apply exists_elt_true_intro with x; auto.
Qed.
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'.
Proof.
unfold Eq_hf.
destruct x as (lx); simpl in |- *; intros.
elim andb_prop with (1 := H); clear H; intros.
specialize forall_elt_true_elim with (1 := H) (2 := H0); intros.
apply exists_elt_true_elim with (P := fun y' => eq_hf x' y').
trivial.
Qed.
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'.
Proof.
unfold Eq_hf.
destruct x as (lx); destruct y as (ly); simpl in |- *; intros.
elim andb_prop with (1 := H); clear H; intros.
specialize forall_elt_true_elim with (1 := H1) (2 := H0); intros.
change lx with (hf_elts (HF lx)).
apply exists_elt_true_elim with (P := fun x1 => eq_hf x1 y').
trivial.
Qed.
Instance eq_hf_refl : Reflexive Eq_hf.
red; intro.
elim x using hf_ind2; intros.
apply eq_hf_intro; intros.
exists x'; auto.
exists y'; auto.
Qed.
Instance eq_hf_sym : Symmetric Eq_hf.
red; intros x.
elim x using hf_ind2; destruct y; intros.
apply eq_hf_intro; intros.
elim eq_hf_elim2 with (1 := H0) (2 := H1); intros.
exists x0; auto.
elim eq_hf_elim1 with (1 := H0) (2 := H1); intros.
exists x0; auto.
Qed.
Instance eq_hf_trans : Transitive Eq_hf.
red; intros x.
elim x using hf_ind2; destruct y; destruct z; intros.
apply eq_hf_intro; intros.
elim eq_hf_elim1 with (1 := H0) (2 := H2); intros.
elim eq_hf_elim1 with (1 := H1) (2 := H3); intros.
exists x1; eauto.
elim eq_hf_elim2 with (1 := H1) (2 := H2); intros.
elim eq_hf_elim2 with (1 := H0) (2 := H3); intros.
exists x1; eauto.
Qed.
Instance eq_hf_equiv : Equivalence Eq_hf. constructor; auto with *.
Qed.
Instance eq_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq bool) eq_hf.
repeat red; intros.
apply bool_1.
fold (Eq_hf x x0) (Eq_hf y y0).
rewrite H; rewrite H0; reflexivity.
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.
intros.
unfold In_hf, in_hf.
apply exists_elt_true_intro with x'; auto.
Qed.
Lemma in_hf_elim : ∀ x y,
In_hf x y ->
exists2 x', In x' (hf_elts y) & Eq_hf x x'.
unfold In_hf, in_hf.
intros.
apply exists_elt_true_elim with (1:=H).
Qed.
Lemma in_hf_reg_l: ∀ a a' b,
Eq_hf a a' -> In_hf a b -> In_hf a' b.
intros.
elim in_hf_elim with (1:=H0); intros.
apply in_hf_intro with x; trivial.
transitivity a; trivial; symmetry; trivial.
Qed.
Lemma in_hf_reg_r :
∀ a x y,
Eq_hf x y ->
In_hf a x ->
In_hf a y.
intros.
elim in_hf_elim with (1:=H0); intros.
elim eq_hf_elim1 with (1:=H) (2:=H1); intros.
apply in_hf_intro with x1; trivial.
transitivity x0; trivial.
Qed.
Instance In_hf_morph : Proper (Eq_hf ==> Eq_hf ==> iff) In_hf.
split; intros.
apply in_hf_reg_l with x; trivial.
apply in_hf_reg_r with x0; trivial.
symmetry in H, H0.
apply in_hf_reg_l with y; trivial.
apply in_hf_reg_r with y0; trivial.
Qed.
Instance in_hf_morph : Proper (Eq_hf ==> Eq_hf ==> @eq _) in_hf.
repeat red; intros.
apply bool_1.
fold (In_hf x x0) (In_hf y y0).
rewrite H; rewrite H0; reflexivity.
Qed.
Lemma In_hf_head : ∀ x y l,
Eq_hf x y ->
In_hf x (HF (y::l)).
intros.
apply in_hf_intro with y; simpl; auto.
Qed.
Lemma In_hf_tail : ∀ x y l,
In_hf x (HF l) ->
In_hf x (HF (y::l)).
intros.
elim in_hf_elim with (1:=H); intros.
apply in_hf_intro with x0; simpl; auto.
Qed.
Lemma In_hf_elim : ∀ x y l,
In_hf x (HF (y::l)) ->
Eq_hf x y \/ In_hf x (HF l).
Proof.
intros.
elim in_hf_elim with (1:=H); simpl; intros.
destruct H0.
subst x0; auto.
right; apply in_hf_intro with x0; trivial.
Qed.
Lemma In_app_left : ∀ x l1 l2,
In_hf x (HF l1) ->
In_hf x (HF (l1 ++ l2)).
Proof.
induction l1; simpl; intros.
inversion H.
elim In_hf_elim with (1:=H); intros.
apply In_hf_head; trivial.
apply In_hf_tail; auto.
Qed.
Lemma In_app_right : ∀ x l1 l2,
In_hf x (HF l2) ->
In_hf x (HF (l1 ++ l2)).
Proof.
induction l1; simpl; intros; auto.
apply In_hf_tail; auto.
Qed.
Lemma In_app_elim : ∀ x l1 l2,
In_hf x (HF (l1 ++ l2)) ->
In_hf x (HF l1) \/ In_hf x (HF l2).
induction l1; simpl; intros; auto.
elim In_hf_elim with (1:=H); intros.
left.
apply In_hf_head; trivial.
elim IHl1 with (1:=H0); intros; auto.
left.
apply In_hf_tail; trivial.
Qed.
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.
unfold Incl_hf; split; intros.
rewrite <- H0; rewrite <- H in H2; auto.
rewrite H0; rewrite H in H2; auto.
Qed.
Lemma incl_hf_sound : ∀ x y,
incl_hf x y = true -> Incl_hf x y.
unfold incl_hf, Incl_hf.
intros.
elim in_hf_elim with (1:=H0); intros.
specialize forall_elt_true_elim with (1:=H) (2:=H1); intros.
apply in_hf_reg_l with x0; trivial.
symmetry; trivial.
Qed.
Lemma incl_hf_complete : ∀ x y,
Incl_hf x y -> incl_hf x y = true.
unfold incl_hf, Incl_hf; intros.
apply forall_elt_true_intro; intros.
apply H.
apply in_hf_intro with y0; trivial; reflexivity.
Qed.
Lemma Eq_hf_intro : ∀ x y,
Incl_hf x y -> Incl_hf y x -> Eq_hf x y.
intros.
apply eq_hf_intro; intros.
apply in_hf_elim.
apply H.
apply in_hf_intro with x'; trivial; reflexivity.
elim (in_hf_elim y' x); intros.
exists x0; trivial; symmetry; trivial.
apply H0.
apply in_hf_intro with y'; trivial; reflexivity.
Qed.
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)).
Proof.
intros.
apply Eq_hf_intro; red; simpl in |- *; intros.
elim In_hf_elim with (1:=H1); intros.
apply In_hf_head; transitivity x1; trivial.
apply In_hf_tail; apply in_hf_reg_r with (HF l1); trivial.
elim In_hf_elim with (1:=H1); intros.
apply In_hf_head; transitivity x2; trivial.
symmetry; trivial.
apply In_hf_tail; apply in_hf_reg_r with (HF l2); trivial.
symmetry; trivial.
Qed.
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')).
intros.
apply Eq_hf_intro; red; intros.
elim In_app_elim with (1:=H1); intros.
apply In_app_left.
apply in_hf_reg_r with (HF l1); auto.
apply In_app_right.
apply in_hf_reg_r with (HF l2); auto.
elim In_app_elim with (1:=H1); intros.
apply In_app_left.
apply in_hf_reg_r with (HF l1'); auto.
symmetry; auto.
apply In_app_right.
apply in_hf_reg_r with (HF l2'); auto.
symmetry; auto.
Qed.
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.
Proof.
destruct x as (x).
intro Pnil.
elim x; intros; trivial.
change l with (hf_elts (HF l)).
apply X0.
apply In_hf_head; reflexivity.
red; intros; apply In_hf_tail; trivial.
apply X; intros.
apply X0; trivial.
apply In_hf_tail; trivial.
red; intros; apply In_hf_tail; auto.
Qed.
Cancelling redundancies
Lemma cancel_repeat : ∀ a l,
In_hf a (HF l) -> Eq_hf (HF(a::l)) (HF l).
intros.
apply Eq_hf_intro; red; intros.
elim In_hf_elim with (1:=H0); intros; auto.
rewrite H1; trivial.
apply In_hf_tail; trivial.
Qed.
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)).
unfold cons_hf.
intros.
case_eq (in_hf x (HF l)); intro.
symmetry; apply cancel_repeat; trivial.
reflexivity.
Qed.
Lemma In_hf_head_hf : ∀ x y l,
Eq_hf x y ->
In_hf x (HF (cons_hf y l)).
Proof.
intros.
rewrite cons_hf_cons.
apply In_hf_head; trivial.
Qed.
Lemma In_hf_tail_hf : ∀ x y l,
In_hf x (HF l) ->
In_hf x (HF (cons_hf y l)).
Proof.
intros.
rewrite cons_hf_cons.
apply In_hf_tail; trivial.
Qed.
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).
intros.
rewrite cons_hf_cons in H.
apply In_hf_elim; trivial.
Qed.
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)).
Proof.
intros.
do 2 rewrite cons_hf_cons.
apply Eq_hf_cons; trivial.
Qed.
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)).
Proof.
induction l1; simpl; intros.
inversion H.
elim In_hf_elim with (1:=H); intros.
apply In_hf_head_hf; trivial.
apply In_hf_tail_hf; auto.
Qed.
Lemma In_app_hf_right : ∀ x l1 l2,
In_hf x (HF l2) ->
In_hf x (HF (app_hf l1 l2)).
Proof.
induction l1; simpl; intros; auto.
apply In_hf_tail_hf; auto.
Qed.
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).
induction l1; simpl; intros; auto.
elim In_hf_elim_hf with (1:=H); intros.
left.
apply In_hf_head; trivial.
elim IHl1 with (1:=H0); intros; auto.
left.
apply In_hf_tail; trivial.
Qed.
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).
reflexivity.
Qed.
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).
Proof.
destruct x.
induction elts; simpl; intros; auto.
rewrite fold_set_unfold.
case_eq (in_hf a (HF elts)); intro.
change elts with (hf_elts (HF elts)).
apply H0; trivial.
apply In_hf_head; reflexivity.
simpl in IHelts; apply (IHelts acc); intros; trivial.
apply H0; trivial.
apply In_hf_tail; trivial.
apply H1; trivial.
apply In_hf_tail; trivial.
change elts with (hf_elts (HF elts)).
apply H1; trivial.
apply In_hf_head; reflexivity.
unfold In_hf; rewrite H2; discriminate.
simpl in IHelts; apply (IHelts acc); intros; trivial.
apply H0; trivial.
apply In_hf_tail; trivial.
apply H1; trivial.
apply In_hf_tail; trivial.
Qed.
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.
Proof.
intro.
elim x using hf_ind2; intros.
unfold canonical in |- *; fold canonical in |- *.
induction l; simpl in |- *; intros.
compute; reflexivity.
rewrite fold_set_unfold.
case_eq (in_hf a (HF l)); intro.
apply eq_hf_trans with (HF l); auto with *.
symmetry; apply cancel_repeat; trivial.
apply Eq_hf_cons; auto with *.
Qed.
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.
Proof.
unfold singl in |- *; do 2 red; intros.
apply Eq_hf_cons_hf; trivial.
reflexivity.
Qed.
Instance pair_morph : morph2 pair.
Proof.
unfold pair in |- *; do 3 red; intros.
repeat apply Eq_hf_cons_hf; trivial.
reflexivity.
Qed.
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.
Proof.
unfold eq_hf_fun in |- *; intros.
symmetry in |- *.
apply H.
apply in_hf_reg_l with y1; trivial.
symmetry in |- *; trivial.
Qed.
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.
Proof.
unfold eq_hf_fun in |- *; intros.
transitivity (f2 y1); auto.
apply H; trivial.
reflexivity.
Qed.
Lemma eq_hf_fun_left : ∀ x f1 f2,
eq_hf_fun x f1 f2 -> eq_hf_fun x f1 f1.
Proof.
unfold eq_hf_fun in |- *; intros.
transitivity (f2 y2); auto.
symmetry in |- *.
apply H.
apply in_hf_reg_l with y1; trivial.
reflexivity.
Qed.
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.
compute in |- *; intros; discriminate.
Qed.
Lemma empty_ext : ∀ a, (∀ x, ~ x ∈ a) -> a == empty.
intros.
apply Eq_hf_intro; red; intros.
elim H with a0; trivial.
elim empty_elim with a0; trivial.
Qed.
Lemma singl_intro : ∀ x y, x == y -> x ∈ singl y.
unfold singl in |- *; auto.
Qed.
Lemma singl_elim : ∀ x a, x ∈ singl a -> x == a.
unfold singl in |- *; intros.
elim In_hf_elim_hf with (1 := H); intros; auto.
discriminate H0.
Qed.
Lemma singl_ext :
∀ y x,
x ∈ y ->
(∀ z, z ∈ y -> z == x) ->
y == singl x.
Proof.
intros; apply Eq_hf_intro; red; intros.
apply singl_intro; auto.
apply in_hf_reg_l with x; trivial.
symmetry in |- *; apply singl_elim; trivial.
Qed.
Lemma pair_elim : ∀ x a b,
x ∈ pair a b -> x == a \/ x == b.
intros.
unfold pair in H.
elim In_hf_elim_hf with (1 := H); intros; auto.
right.
elim In_hf_elim_hf with (1 := H0); intros; auto.
discriminate H1.
Qed.
Lemma pair_intro1 : ∀ x a b, x == a -> x ∈ pair a b.
Proof.
unfold pair;auto.
Qed.
Lemma pair_intro2 : ∀ x a b, x == b -> x ∈ pair a b.
Proof.
unfold pair;auto.
Qed.
Lemma union_intro : ∀ x y z, x ∈ y -> y ∈ z -> x ∈ union z.
Proof.
intros x y z H.
unfold union.
pattern z, (fold_set _ (fun y0 l => hf_elts y0 +++ l) z nil).
apply fold_set_ind; intros.
discriminate.
apply H2.
rewrite cancel_repeat in H3; auto.
elim In_hf_elim with (1:=H3); intros.
apply In_app_hf_left.
rewrite hf_elts_ext.
rewrite <- H4; trivial.
apply In_app_hf_right.
rewrite hf_elts_ext in H4.
auto.
Qed.
Lemma union_elim : ∀ x z, x ∈ union z -> exists2 y, x ∈ y & y ∈ z.
unfold union.
intros x z.
pattern z, (fold_set _ (fun y l => hf_elts y +++ l) z nil).
apply fold_set_ind; intros.
discriminate.
destruct H1; trivial.
exists x0; trivial.
rewrite cancel_repeat; auto.
elim In_app_hf_elim with (1:=H2); intros.
rewrite hf_elts_ext in H3.
exists x'; trivial.
apply In_hf_head; reflexivity.
elim H1 with (1:=H3); intros.
exists x0; trivial.
apply In_hf_tail.
rewrite hf_elts_ext; trivial.
Qed.
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.
intros.
apply Eq_hf_intro; red; intros.
elim H0 with (1:=H1); intros.
apply union_intro with x; trivial.
elim union_elim with (1:=H1); intros.
eauto.
Qed.
Instance union_morph : morph1 union.
do 2 red; intros.
apply union_ext; intros.
apply union_intro with y0; trivial.
rewrite H; trivial.
elim union_elim with (1 := H0); intros.
exists x1; trivial.
rewrite <- H; trivial.
Qed.
Lemma union_singl : ∀ x, union (singl x) == x.
intros.
symmetry; apply union_ext; intros.
apply singl_elim in H0.
rewrite <- H0; trivial.
exists x; trivial.
apply singl_intro; reflexivity.
Qed.
power properties
Lemma power_intro :
∀ x y, Incl_hf x y -> x ∈ power y.
unfold power.
set (g := fun y0 (pow:list hf ->list hf) p => pow p ++ pow (y0 :: p)).
set (h := fun p => HF(rev p) :: nil).
intros x y.
assert (∀ x l, Incl_hf (HF (rev l)) x ->
Incl_hf x (HF(rev l ++ hf_elts y)) ->
x ∈ HF(fold_set _ g y h l)).
clear x.
pattern y, (fold_set _ g y h).
apply fold_set_ind; intros.
unfold h; simpl.
apply In_hf_head.
apply Eq_hf_intro; trivial.
red; intros.
elim In_app_elim with (1:=H0 _ H1); intros; auto.
elim empty_elim with a; trivial.
apply H1; trivial.
red; intros.
elim In_app_elim with (1:=H3 _ H4); intros.
apply In_app_left; trivial.
apply In_app_right.
rewrite hf_elts_ext in H5.
elim In_hf_elim with (1:=H5); intros; trivial.
rewrite H6; trivial.
unfold g; simpl.
case_eq (in_hf x' x); intros.
apply In_app_right.
apply H1.
red; simpl; intros.
elim In_app_elim with (1:=H5); intros; auto.
elim In_hf_elim with (1:=H6); simpl; intros.
rewrite H7; trivial.
elim empty_elim with a; trivial.
simpl.
rewrite app_ass; simpl.
trivial.
apply In_app_left.
apply H1; trivial.
red; intros.
elim In_app_elim with (1:=H3 _ H5); simpl; intros.
apply In_app_left; trivial.
apply In_app_right.
elim In_hf_elim with (1:=H6); intros; auto.
rewrite H7 in H5; unfold In_hf in H5; rewrite H5 in H4; discriminate.
intro; apply H; simpl.
red; intros.
elim empty_elim with a; trivial.
rewrite hf_elts_ext; trivial.
Qed.
Lemma power_elim : ∀ x y z, x ∈ power y -> z ∈ x -> z ∈ y.
unfold power.
set (g := fun y0 (pow:list hf ->list hf) p => pow p ++ pow (y0 :: p)).
set (h := fun p => HF(rev p) :: nil).
intros x y.
assert (∀ l,
x ∈ HF(fold_set _ g y h l) ->
∀ z, z ∈ x -> ~ z ∈ (HF(rev l)) -> z ∈ y).
pattern y, (fold_set _ g y h).
apply fold_set_ind; intros.
unfold h in H.
elim H1.
apply in_hf_reg_r with (2:=H0).
apply singl_elim.
assumption.
apply In_hf_tail.
rewrite hf_elts_ext.
eauto.
unfold g in H2.
elim In_app_elim with (1:=H2);intros.
apply In_hf_tail; rewrite hf_elts_ext.
apply H1 with l; trivial.
case_eq (eq_hf z x'); intro.
apply In_hf_head; trivial.
apply In_hf_tail; rewrite hf_elts_ext.
apply H1 with (1:=H5); trivial.
simpl; red; intros; apply H4.
elim In_app_elim with (1:=H7); intros; trivial.
replace (eq_hf z x') with true in H6; try discriminate.
symmetry; apply singl_elim.
assumption.
intros.
apply H with (l:=@nil hf); trivial.
red; intros; discriminate.
Qed.
Lemma power_ext :
∀ p a,
(∀ x, (∀ y, y ∈ x -> y ∈ a) -> x ∈ p) ->
(∀ x y, x ∈ p -> y ∈ x -> y ∈ a) ->
p == power a.
intros.
apply Eq_hf_intro; red; intros.
apply power_intro; red; intros; eauto.
apply H; intros.
eapply power_elim; eauto.
Qed.
Lemma power_morph : morph1 power.
do 2 red; intros.
apply power_ext; intros.
apply power_intro.
rewrite H; trivial.
rewrite <- H.
apply power_elim with (1 := H0); trivial.
Qed.
Lemma subset_intro_gen : ∀ a (P:hf->bool) x,
x ∈ a -> (∀ x', x==x' -> P x' = true) -> x ∈ subset a P.
unfold subset.
intros a P x in_a in_P; revert in_a.
set (g := fun y l => if P y then y :: l else l).
pattern a, (fold_set _ g a nil).
apply fold_set_ind; simpl; intros; auto.
apply H1; trivial.
rewrite cancel_repeat in in_a; auto.
unfold g.
elim In_hf_elim with (1:=in_a);intros.
rewrite in_P; trivial.
apply In_hf_head; trivial.
destruct (P x'); auto.
apply In_hf_tail; auto.
Qed.
Lemma subset_intro : ∀ a (P:hf->bool) x,
hf_pred_morph a P ->
x ∈ a -> P x = true -> x ∈ subset a P.
intros.
apply subset_intro_gen; trivial.
intros.
red in H.
apply H with (2:=H2); trivial.
Qed.
Lemma subset_elim1 : ∀ a (P:hf->bool) x, x ∈ subset a P -> x ∈ a.
unfold subset.
intros a P x.
set (g := fun y l => if P y then y :: l else l).
pattern a, (fold_set _ g a nil).
apply fold_set_ind; simpl; intros; auto.
rewrite cancel_repeat; auto.
unfold g in H2.
destruct (P x').
elim In_hf_elim with (1:=H2); intros.
apply In_hf_head; trivial.
apply In_hf_tail; auto.
apply In_hf_tail; auto.
Qed.
Lemma subset_elim2_gen : ∀ a (P:hf->bool) x,
x ∈ subset a P ->
exists2 x', x==x' & P x' = true.
unfold subset.
intros a P x.
set (g := fun y l => if P y then y :: l else l).
pattern a, (fold_set _ g a nil).
apply fold_set_ind; simpl; intros; auto.
discriminate.
unfold g in H2.
case_eq (P x'); intro.
rewrite H3 in H2.
elim In_hf_elim with (1:=H2); intros; auto.
exists x'; trivial.
rewrite H3 in H2; auto.
Qed.
Lemma subset_elim2 : ∀ a (P:hf->bool) x,
hf_pred_morph a P ->
x ∈ subset a P ->
P x = true.
unfold subset.
intros a P x Pmorph.
set (g := fun y l => if P y then y :: l else l).
pattern a, (fold_set _ g a nil).
apply fold_set_ind; simpl; intros; auto.
discriminate.
unfold g in H2.
case_eq (P x'); intro.
rewrite H3 in H2.
elim In_hf_elim with (1:=H2); intros; auto.
apply Pmorph with x'; auto.
symmetry; trivial.
rewrite H3 in H2; auto.
Qed.
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.
intros.
apply Eq_hf_intro; red; intros.
apply subset_intro; auto.
apply H0.
apply subset_elim1 with (1:=H3); trivial.
apply subset_elim2 with (2:=H3); trivial.
Qed.
Lemma subset_morph_ext : ∀ x1 x2 y1 y2,
x1 == x2 -> eq_hf_pred x1 y1 y2 -> subset x1 y1 == subset x2 y2.
intros.
assert (hf_pred_morph x1 y1).
red; intros.
red in H0.
rewrite H0 with y3 y3; trivial.
rewrite <- H0 with y0 y3; trivial.
apply in_hf_reg_l with y0; auto.
reflexivity.
assert (hf_pred_morph x2 y2).
red; intros.
red in H0.
rewrite <- H0 with y0 y3; trivial.
rewrite H0 with y0 y0; trivial.
apply in_hf_reg_r with x2; auto.
symmetry; trivial.
reflexivity.
apply in_hf_reg_r with x2; auto.
symmetry; trivial.
apply subset_ext; intros; trivial.
apply subset_intro; trivial.
apply in_hf_reg_r with x2; auto.
symmetry; trivial.
rewrite H0 with x x; trivial.
apply in_hf_reg_r with x2; auto.
symmetry; trivial.
reflexivity.
apply in_hf_reg_r with x1; auto.
apply subset_elim1 with (1:=H3).
rewrite <- H0 with x x.
apply subset_elim2 with (2:=H3); trivial.
apply subset_elim1 with (1:=H3).
reflexivity.
Qed.
Lemma subset_empty1 : ∀ P, subset empty P == empty.
intros.
apply empty_ext; red; intros.
apply subset_elim1 in H.
elim empty_elim with x; trivial.
Qed.
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.
intros.
apply singl_ext; intros.
apply subset_intro_gen; trivial; intros.
apply -> H1; trivial.
rewrite <- H2; trivial.
elim subset_elim2_gen with (1:=H2); intros.
transitivity x0; trivial.
symmetry; apply <- H1; trivial.
rewrite <- H3.
apply subset_elim1 in H2; trivial.
Qed.
replacement properties
Lemma repl_intro : ∀ a f y x,
eq_hf_fun a f f ->
y ∈ a -> x == f y -> x ∈ repl a f.
Proof.
unfold repl.
intros a f y x.
destruct a as (a); simpl.
elim a; simpl; intros.
elim empty_elim with y; trivial.
elim In_hf_elim with (1:=H1); intros.
apply In_hf_head.
rewrite H2; auto.
apply In_hf_tail.
apply H; trivial.
red; intros; apply H0; trivial.
apply In_hf_tail; trivial.
Qed.
Lemma repl_elim : ∀ a f x,
eq_hf_fun a f f ->
x ∈ repl a f -> exists2 y, y ∈ a & x == f y.
Proof.
unfold repl.
intros a f x.
destruct a as (a); elim a; simpl; intros.
elim empty_elim with x; trivial.
elim In_hf_elim with (1:=H1); intros.
exists a0; trivial.
apply In_hf_head; reflexivity.
elim H with (2:=H2); intros.
exists x0; trivial.
apply In_hf_tail; trivial.
red; intros; apply H0; trivial.
apply In_hf_tail; trivial.
Qed.
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.
intros.
apply Eq_hf_intro; red; intros.
elim H1 with (1:=H2); intros.
apply repl_intro with x0 ;trivial.
elim repl_elim with (2:=H2); intros; trivial.
apply in_hf_reg_l with (f x0); auto.
symmetry; trivial.
Qed.
Lemma repl_morph :
∀ x1 x2 f1 f2,
x1 == x2 ->
eq_hf_fun x1 f1 f2 ->
repl x1 f1 == repl x2 f2.
unfold eq_hf_fun, repl.
intros.
apply eq_hf_intro; simpl; intros.
elim in_map_inv with (1 := H1); intros.
elim eq_hf_elim1 with (1 := H) (2 := H2); intros.
exists (f2 x0).
apply in_map; trivial.
rewrite H3.
apply H0; auto.
apply in_hf_intro with x; trivial; reflexivity.
elim in_map_inv with (1 := H1); intros.
elim eq_hf_elim2 with (1 := H) (2 := H2); intros.
exists (f1 x0).
apply in_map; trivial.
rewrite H3.
apply H0; auto.
apply in_hf_intro with x0; trivial; reflexivity.
Qed.
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.
Proof.
intros; unfold couple in |- *; symmetry in |- *.
apply union_ext; intros.
elim pair_elim with (1 := H0); intro y_eq; rewrite y_eq in H; trivial.
apply pair_intro1.
apply singl_elim; trivial.
elim pair_elim with (1 := H); intro.
exists (singl a).
apply singl_intro; auto.
apply pair_intro1; reflexivity.
exists (pair a b).
apply pair_intro2; trivial.
apply pair_intro2; reflexivity.
Qed.
Instance couple_morph : morph2 couple.
unfold couple; do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
Qed.
Instance fst_morph : morph1 fst.
unfold fst; do 2 red; intros.
apply union_morph.
apply subset_morph_ext.
apply union_morph; trivial.
red in |- *; intros.
rewrite H; rewrite H1; trivial.
Qed.
Lemma fst_def : ∀ x y, fst (couple x y) == x.
unfold fst.
intros.
assert (hf_pred_morph (union (couple x y))
(fun x0 => in_hf (singl x0) (couple x y))).
red; intros.
change (singl y2 ∈ couple x y).
rewrite <- H0; trivial.
symmetry.
apply union_ext; intros.
apply in_hf_reg_r with y0; trivial.
specialize subset_elim2 with (1:=H) (2:=H1); clear H1; intro.
unfold couple in H1.
elim pair_elim with (1:=H1); clear H1; intros.
apply singl_elim.
apply in_hf_reg_r with (singl y0); auto.
apply singl_intro; reflexivity.
symmetry; apply singl_elim.
apply in_hf_reg_r with (pair x y).
symmetry; trivial.
apply pair_intro1; reflexivity.
exists x; trivial.
apply subset_intro; trivial.
apply union_intro with (singl x).
apply singl_intro; reflexivity.
unfold couple; apply pair_intro1; reflexivity.
unfold couple; apply pair_intro1; reflexivity.
Qed.
Instance snd_morph : morph1 snd.
unfold snd; do 2 red; intros.
apply union_morph.
apply subset_morph_ext.
apply union_morph; trivial.
red in |- *; intros.
rewrite H; rewrite H1; trivial.
Qed.
Lemma snd_def : ∀ x y, snd (couple x y) == y.
intros; unfold snd in |- *.
assert (hf_pred_morph (union (couple x y))
(fun y0 => eq_hf (pair (fst (couple x y)) y0) (union (couple x y)))).
red; intros.
change (pair (fst (couple x y)) y2 == union (couple x y)).
rewrite <- H0; trivial.
transitivity (union (singl y)).
apply union_morph.
apply singl_ext; intros.
apply subset_intro; trivial.
rewrite union_couple_eq.
apply pair_intro2; reflexivity.
rewrite fst_def.
apply eq_hf_sym.
apply union_couple_eq.
specialize subset_elim2 with (1 := H) (2:=H0); intro.
generalize H1.
rewrite fst_def.
clear H0; intro.
rewrite union_couple_eq in H0.
elim pair_elim with z x y; intros; trivial.
rewrite H2 in H0 |- *; clear H2.
symmetry.
elim pair_elim with y x x; intros; trivial.
apply in_hf_reg_r with (pair x y).
symmetry; trivial.
apply pair_intro2; reflexivity.
apply in_hf_reg_r with (pair x z); trivial.
apply pair_intro2; reflexivity.
symmetry; apply union_ext; intros.
apply in_hf_reg_r with y0; trivial.
apply singl_elim; trivial.
exists y; trivial.
apply singl_intro; reflexivity.
Qed.
Lemma snd_ext : ∀ p x y,
p == couple x y ->
y == snd p.
intros.
rewrite H; rewrite snd_def; reflexivity.
Qed.
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.
Proof.
intros; unfold couple in |- *; symmetry in |- *.
apply union_ext; intros.
elim pair_elim with (1 := H0); intro y_eq; rewrite y_eq in H; trivial.
apply pair_intro1.
apply singl_elim; trivial.
elim pair_elim with (1 := H); intro.
exists (singl a).
apply singl_intro; auto.
apply pair_intro1; reflexivity.
exists (pair a b).
apply pair_intro2; trivial.
apply pair_intro2; reflexivity.
Qed.
Instance couple_morph : morph2 couple.
unfold couple; do 3 red; intros.
rewrite H; rewrite H0; reflexivity.
Qed.
Instance fst_morph : morph1 fst.
unfold fst; do 2 red; intros.
apply union_morph.
apply subset_morph_ext.
apply union_morph; trivial.
red in |- *; intros.
rewrite H; rewrite H1; trivial.
Qed.
Lemma fst_def : ∀ x y, fst (couple x y) == x.
unfold fst.
intros.
assert (hf_pred_morph (union (couple x y))
(fun x0 => in_hf (singl x0) (couple x y))).
red; intros.
change (singl y2 ∈ couple x y).
rewrite <- H0; trivial.
symmetry.
apply union_ext; intros.
apply in_hf_reg_r with y0; trivial.
specialize subset_elim2 with (1:=H) (2:=H1); clear H1; intro.
unfold couple in H1.
elim pair_elim with (1:=H1); clear H1; intros.
apply singl_elim.
apply in_hf_reg_r with (singl y0); auto.
apply singl_intro; reflexivity.
symmetry; apply singl_elim.
apply in_hf_reg_r with (pair x y).
symmetry; trivial.
apply pair_intro1; reflexivity.
exists x; trivial.
apply subset_intro; trivial.
apply union_intro with (singl x).
apply singl_intro; reflexivity.
unfold couple; apply pair_intro1; reflexivity.
unfold couple; apply pair_intro1; reflexivity.
Qed.
Instance snd_morph : morph1 snd.
unfold snd; do 2 red; intros.
apply union_morph.
apply subset_morph_ext.
apply union_morph; trivial.
red in |- *; intros.
rewrite H; rewrite H1; trivial.
Qed.
Lemma snd_def : ∀ x y, snd (couple x y) == y.
intros; unfold snd in |- *.
assert (hf_pred_morph (union (couple x y))
(fun y0 => eq_hf (pair (fst (couple x y)) y0) (union (couple x y)))).
red; intros.
change (pair (fst (couple x y)) y2 == union (couple x y)).
rewrite <- H0; trivial.
transitivity (union (singl y)).
apply union_morph.
apply singl_ext; intros.
apply subset_intro; trivial.
rewrite union_couple_eq.
apply pair_intro2; reflexivity.
rewrite fst_def.
apply eq_hf_sym.
apply union_couple_eq.
specialize subset_elim2 with (1 := H) (2:=H0); intro.
generalize H1.
rewrite fst_def.
clear H0; intro.
rewrite union_couple_eq in H0.
elim pair_elim with z x y; intros; trivial.
rewrite H2 in H0 |- *; clear H2.
symmetry.
elim pair_elim with y x x; intros; trivial.
apply in_hf_reg_r with (pair x y).
symmetry; trivial.
apply pair_intro2; reflexivity.
apply in_hf_reg_r with (pair x z); trivial.
apply pair_intro2; reflexivity.
symmetry; apply union_ext; intros.
apply in_hf_reg_r with y0; trivial.
apply singl_elim; trivial.
exists y; trivial.
apply singl_intro; reflexivity.
Qed.
Lemma snd_ext : ∀ p x y,
p == couple x y ->
y == snd p.
intros.
rewrite H; rewrite snd_def; reflexivity.
Qed.
regularity
Lemma raw_choose_elt : ∀ x, {y | In y (hf_elts x)}+{x==empty}.
intros ([|h l]); simpl; [right;compute;reflexivity|left;exists h; auto].
Qed.
Lemma choose_elt : ∀ x, {y | y ∈ x}+{x==empty}.
intros ([|h l]); [right;compute;reflexivity|left;exists h].
apply in_hf_intro with h; simpl; auto; reflexivity.
Qed.
Lemma regularity_ax: ∀ a a0, a0 ∈ a ->
exists2 b, b ∈ a & ~(exists2 c, c ∈ a & c ∈ b).
induction a0 using hf_ind2; intros.
set (a0 := HF l) in *.
pose (A := subset a0 (fun y => in_hf y a)).
destruct (choose_elt A).
destruct s.
subst A.
specialize subset_elim1 with (1:=i); intro.
apply in_hf_elim in H1.
destruct H1.
rewrite H2 in i; clear H2 x.
assert (x0 ∈ a).
apply subset_elim2 with (2:=i).
red; intros.
rewrite H3 in H4; trivial.
eauto.
exists a0; trivial.
red; destruct 1.
assert (x ∈ A).
apply subset_intro; trivial.
red; intros.
rewrite H4 in H5; trivial.
rewrite e in H3; elim empty_elim with (1:=H3).
Qed.