# Library AMM11262.unicode_format.utf_example2

Require Import utf_AMM11262.
Import NatSet GeneralProperties.

Section example_five_inhabitants.
Now we find the witness, in a town with 5 inhabitants; ie, n=2

Definition town_2:= {1}∪({2}∪({3}∪({4}∪({5}∪)))).

Remark population₂ : |town_2| = 2×2 +1.
Proof.
reflexivity.
Qed.

Definition familiarity₂ (m n:elt):Prop :=
match m,n with
| 1,2=> True
| 1,3 => True
| 1,4 => True
| 1,5 => True
| 2,1 => True
| 2,5 => True
| 3,1 => True
| 3,4 => True
| 3,5 => True
| 4,1 => True
| 4,3 => True
| 5,1 => True
| 5,2 => True
| 5,3 => True
| _,_ => False
end.
Infix "ℛ₂" := familiarity₂ (at level 70, no associativity).

Remark familiarity₂_sym: m n, m ℛ₂ n n ℛ₂ m.
Proof.
intros [|[|[|[|[|[|m']]]]]] [|[|[|[|[|[|n']]]]]]; trivial.
Qed.

Remark familiarity₂_extensional: m n p, np m ℛ₂ n m ℛ₂ p.
Proof.
intros m n p H1 H2; compute in H1; rewrite <- H1; assumption.
Qed.

Remark subsets_2: B, Btown_2 |B| = 2
(((((((((B {1}∪({2}∪)\/ B{1}∪({3}∪)) B{1}∪({4}∪)) B {1}∪({5}∪)) B{2}∪({3}∪))
B{2}∪({4}∪)) B{2}∪({5}∪)) B{3}∪({4}∪)) B {3}∪({5}∪)) B{4}∪({5}∪)).
Proof.
intros B H_sub H_card.
destruct (In_dec 1 B) as [H1|H1].
do 6 left.
assert (H_card_rem:|B\{1}|=1);
[ rewrite <- (remove_cardinal_1 H1) in H_card; apply eq_add_S; assumption|].
destruct (In_dec 2 (B\{1})) as [H12|H12].
do 3 left.
generalize (remove_cardinal_1 H12).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 3 (B\{1})) as [H13|H13].
do 2 left; right.
generalize (remove_cardinal_1 H13).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 4 (B\{1})) as [H14|H14].
left; right.
generalize (remove_cardinal_1 H14).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 5 (B\{1})) as [H15|H15].
right.
generalize (remove_cardinal_1 H15).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
apply False_rec.
assert (H11:=(@remove_1 B _ _ (refl_equal 1))).
destruct (cardinal_inv_2 H_card_rem) as [b Hb].
destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
apply H11; rewrite Hb1 in Hb; assumption.
destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
apply H12; rewrite <- Hb2; assumption.
destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
apply H13; rewrite <- Hb3; assumption.
destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4].
apply H14; rewrite <- Hb4; assumption.
destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5].
apply H15; rewrite <- Hb5; assumption.

assert (H_sub':=@subset_remove_3 _ _ 1 H_sub).
assert (Hb_town:=H_sub' _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply Hb1; rewrite Hb1_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply Hb2; rewrite Hb2_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply Hb3; rewrite Hb3_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply Hb4; rewrite Hb4_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply Hb5; rewrite Hb5_town; reflexivity.
apply (proj1 (FM.empty_iff b) Hb5_town)...
destruct (In_dec 2 B) as [H2|H2].
assert (H_card_rem:|B\{2}|=1);
[ rewrite <- (remove_cardinal_1 H2) in H_card; apply eq_add_S; assumption|].
assert (H21:=fun HH : 1∈(B\{2}) => H1 (remove_3 HH)).
destruct (In_dec 3 (B\{2})) as [H23|H23].
do 5 left; right.
generalize (remove_cardinal_1 H23).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 4 (B\{2})) as [H24|H24].
do 4 left; right.
generalize (remove_cardinal_1 H24).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 5 (B\{2})) as [H25|H25].
do 3 left; right.
generalize (remove_cardinal_1 H25).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
apply False_rec.
assert (H22:=(@remove_1 B _ _ (refl_equal 2))).
destruct (cardinal_inv_2 H_card_rem) as [b Hb].
destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
apply H21; rewrite Hb1 in Hb; assumption.
destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
apply H22; rewrite Hb2 in Hb; assumption.
destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
apply H23; rewrite <- Hb3; assumption.
destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4].
apply H24; rewrite <- Hb4; assumption.
destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5].
apply H25; rewrite <- Hb5; assumption.

assert (H_sub':=@subset_remove_3 _ _ 2 H_sub).
assert (Hb_town:=H_sub' _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply Hb1; rewrite Hb1_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply Hb2; rewrite Hb2_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply Hb3; rewrite Hb3_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply Hb4; rewrite Hb4_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply Hb5; rewrite Hb5_town; reflexivity.
apply (proj1 (FM.empty_iff b) Hb5_town)...
destruct (In_dec 3 B) as [H3|H3].
assert (H_card_rem:|B\{3}|=1);
[ rewrite <- (remove_cardinal_1 H3) in H_card; apply eq_add_S; assumption|].
assert (H31:=fun HH : 1∈(B\{3}) => H1 (remove_3 HH)).
assert (H32:=fun HH : 2∈(B\{3}) => H2 (remove_3 HH)).
destruct (In_dec 4 (B\{3})) as [H34|H34].
do 2 left; right.
generalize (remove_cardinal_1 H34).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
destruct (In_dec 5 (B\{3})) as [H35|H35].
left; right.
generalize (remove_cardinal_1 H35).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
apply False_rec.
assert (H33:=(@remove_1 B _ _ (refl_equal 3))).
destruct (cardinal_inv_2 H_card_rem) as [b Hb].
destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
apply H31; rewrite Hb1 in Hb; assumption.
destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
apply H32; rewrite Hb2 in Hb; assumption.
destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
apply H33; rewrite Hb3 in Hb; assumption.
destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4].
apply H34; rewrite <- Hb4; assumption.
destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5].
apply H35; rewrite <- Hb5; assumption.

assert (H_sub':=@subset_remove_3 _ _ 3 H_sub).
assert (Hb_town:=H_sub' _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply Hb1; rewrite Hb1_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply Hb2; rewrite Hb2_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply Hb3; rewrite Hb3_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply Hb4; rewrite Hb4_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply Hb5; rewrite Hb5_town; reflexivity.
apply (proj1 (FM.empty_iff b) Hb5_town)...
destruct (In_dec 4 B) as [H4|H4].
assert (H_card_rem:|B\{4}|=1);
[ rewrite <- (remove_cardinal_1 H4) in H_card; apply eq_add_S; assumption|].
assert (H41:=fun HH : 1∈(B\{4}) => H1 (remove_3 HH)).
assert (H42:=fun HH : 2∈(B\{4}) => H2 (remove_3 HH)).
assert (H43:=fun HH : 3∈(B\{4}) => H3 (remove_3 HH)).
destruct (In_dec 5 (B\{4})) as [H45|H45].
right.
generalize (remove_cardinal_1 H45).
rewrite H_card_rem; intro H_eq2.
rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq2))); reflexivity...
apply False_rec.
assert (H44:=(@remove_1 B _ _ (refl_equal 4))).
destruct (cardinal_inv_2 H_card_rem) as [b Hb].
destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
apply H41; rewrite Hb1 in Hb; assumption.
destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
apply H42; rewrite Hb2 in Hb; assumption.
destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
apply H43; rewrite Hb3 in Hb; assumption.
destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4].
apply H44; rewrite Hb4 in Hb; assumption.
destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5].
apply H45; rewrite <- Hb5; assumption.

assert (H_sub':=@subset_remove_3 _ _ 4 H_sub).
assert (Hb_town:=H_sub' _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply Hb1; rewrite Hb1_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply Hb2; rewrite Hb2_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply Hb3; rewrite Hb3_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply Hb4; rewrite Hb4_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply Hb5; rewrite Hb5_town; reflexivity.
apply (proj1 (FM.empty_iff b) Hb5_town)...
apply False_rec.
destruct (In_dec 5 B) as [H5|H5].
assert (H_card_rem:|B\{5}|=1);
[ rewrite <- (remove_cardinal_1 H5) in H_card; apply eq_add_S; assumption|].
assert (H51:=fun HH : 1∈(B\{5}) => H1 (remove_3 HH)).
assert (H52:=fun HH : 2∈(B\{5}) => H2 (remove_3 HH)).
assert (H53:=fun HH : 3∈(B\{5}) => H3 (remove_3 HH)).
assert (H54:=fun HH : 4∈(B\{5}) => H4 (remove_3 HH)).
assert (H55:=(@remove_1 B _ _ (refl_equal 5))).
destruct (cardinal_inv_2 H_card_rem) as [b Hb].
assert (H_sub':=@subset_remove_3 _ _ 5 H_sub).
assert (Hb_town:=H_sub' _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply H51; rewrite <- Hb1_town in Hb; assumption.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply H52; rewrite <- Hb2_town in Hb; assumption.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply H53; rewrite <- Hb3_town in Hb; assumption.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply H54; rewrite <- Hb4_town in Hb; assumption.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply H55; rewrite <- Hb5_town in Hb; assumption.
apply (proj1 (FM.empty_iff b) Hb5_town)...
destruct (cardinal_inv_2 H_card) as [b Hb].
destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
apply H1; rewrite Hb1 in Hb; assumption.
destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
apply H2; rewrite Hb2 in Hb; assumption.
destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
apply H3; rewrite Hb3 in Hb; assumption.
destruct (NatSet.E.eq_dec b 4) as [Hb4|Hb4].
apply H4; rewrite Hb4 in Hb; assumption.
destruct (NatSet.E.eq_dec b 5) as [Hb5|Hb5].
apply H5; rewrite <- Hb5; assumption.

assert (Hb_town:=H_sub _ Hb).
unfold town_2 in Hb_town.
destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
apply Hb1; rewrite Hb1_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
apply Hb2; rewrite Hb2_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
apply Hb3; rewrite Hb3_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb3_town) as [Hb4_town|Hb4_town].
apply Hb4; rewrite Hb4_town; reflexivity.
destruct (proj1 (FM.add_iff _ _ b) Hb4_town) as [Hb5_town|Hb5_town].
apply Hb5; rewrite Hb5_town; reflexivity.
apply (proj1 (FM.empty_iff b) Hb5_town)...
Qed.

Remark acquintance_2: B, Btown_2 |B| = 2
d, d∈(town_2\B) ( b, bB d ℛ₂ b).
Proof.
intros B H_sub H_card.
destruct (subsets_2 B H_sub H_card) as [[[[[[[[[HB12|HB13]|HB14]|HB15]|HB23]|HB24]|HB25]|HB34]|HB35]|HB45].
exists 5; split.
rewrite HB12; apply mem_2; trivial.
intro b; rewrite HB12; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 4; split.
rewrite HB13; apply mem_2; trivial.
intro b; rewrite HB13; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 3; split.
rewrite HB14; apply mem_2; trivial.
intro b; rewrite HB14; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 2; split.
rewrite HB15; apply mem_2; trivial.
intro b; rewrite HB15; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 5; split.
rewrite HB23; apply mem_2; trivial.
intro b; rewrite HB23; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 1; split.
rewrite HB24; apply mem_2; trivial.
intro b; rewrite HB24; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 1; split.
rewrite HB25; apply mem_2; trivial.
intro b; rewrite HB25; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 1; split.
rewrite HB34; apply mem_2; trivial.
intro b; rewrite HB34; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 1; split.
rewrite HB35; apply mem_2; trivial.
intro b; rewrite HB35; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
exists 3; split.
rewrite HB45; apply mem_2; trivial.
intro b; rewrite HB45; intro Hb.
destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
compute in H; rewrite <- H; simpl; trivial.
destruct (proj1 (FM.add_iff _ _ b) H) as [H'|H'].
compute in H'; rewrite <- H'; simpl; trivial.
apply False_ind; apply (proj1 (FM.empty_iff b) H').
Defined.

Check (AMM11262 town_2 2 population₂ familiarity₂ familiarity₂_sym familiarity₂_extensional acquintance_2).

Definition social_citizen_2:=AMM11262 town_2 2 population₂ familiarity₂
familiarity₂_sym familiarity₂_extensional acquintance_2.

End example_five_inhabitants.

Extraction "social2" social_citizen_2.