Library AMM11262.ascii_format.example2
Now we find the witness, in a town with 5 inhabitants; ie, n=2
Definition town_2:= 1 ++ 2 ++ 3 ++ 4 ++ 5 ++ empty.
Remark population_2 : cardinal town_2 = 2*2 +1.
Proof.
reflexivity.
Qed.
Definition familiarity_2 (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.
Remark familiarity_2_sym:forall m n : elt, familiarity_2 m n -> familiarity_2 n m.
Proof.
intros [|[|[|[|[|[|m']]]]]] [|[|[|[|[|[|n']]]]]]; trivial.
Qed.
Remark familiarity_2_extensional:forall (m : elt) (n p : E.t), E.eq n p -> familiarity_2 m n -> familiarity_2 m p.
Proof.
intros m n p H1 H2; compute in H1; rewrite <- H1; assumption.
Qed.
Remark subsets_2: forall B : t, Subset B town_2 -> cardinal B = 2 ->
{B [=] 1++2++empty}+{B[=]1++3++empty}+{B[=]1++4++empty}+{B [=] 1++5++empty}+{B[=]2++3++empty}+
{B[=]2++4++empty}+{B[=]2++5++empty}+{B[=]3++4++empty}+{B [=] 3++5++empty}+{B[=]4++5++empty}.
Proof.
intros B H_sub H_card.
destruct (In_dec 1 B) as [H1|H1].
do 6 left.
assert (H_card_rem:cardinal (remove 1 B)=1);
[ rewrite <- (remove_cardinal_1 H1) in H_card; apply eq_add_S; assumption|].
destruct (In_dec 2 (remove 1 B)) as [H12|H12].
do 3 left.
rewrite <- (add_remove H1).
rewrite <- (add_remove H12).
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 (remove 1 B)) as [H13|H13].
do 2 left; right.
rewrite <- (add_remove H1).
rewrite <- (add_remove H13).
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 (remove 1 B)) as [H14|H14].
left; right.
rewrite <- (add_remove H1).
rewrite <- (add_remove H14).
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 (remove 1 B)) as [H15|H15].
right.
rewrite <- (add_remove H1).
rewrite <- (add_remove H15).
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:cardinal (remove 2 B)=1);
[ rewrite <- (remove_cardinal_1 H2) in H_card; apply eq_add_S; assumption|].
assert (H21:=fun HH : In 1 (remove 2 B) => H1 (remove_3 HH)).
destruct (In_dec 3 (remove 2 B)) as [H23|H23].
do 5 left; right.
rewrite <- (add_remove H2).
rewrite <- (add_remove H23).
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 (remove 2 B)) as [H24|H24].
do 4 left; right.
rewrite <- (add_remove H2).
rewrite <- (add_remove H24).
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 (remove 2 B)) as [H25|H25].
do 3 left; right.
rewrite <- (add_remove H2).
rewrite <- (add_remove H25).
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:cardinal (remove 3 B)=1);
[ rewrite <- (remove_cardinal_1 H3) in H_card; apply eq_add_S; assumption|].
assert (H31:=fun HH : In 1 (remove 3 B) => H1 (remove_3 HH)).
assert (H32:=fun HH : In 2 (remove 3 B) => H2 (remove_3 HH)).
destruct (In_dec 4 (remove 3 B)) as [H34|H34].
do 2 left; right.
rewrite <- (add_remove H3).
rewrite <- (add_remove H34).
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 (remove 3 B)) as [H35|H35].
left; right.
rewrite <- (add_remove H3).
rewrite <- (add_remove H35).
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:cardinal (remove 4 B)=1);
[ rewrite <- (remove_cardinal_1 H4) in H_card; apply eq_add_S; assumption|].
assert (H41:=fun HH : In 1 (remove 4 B) => H1 (remove_3 HH)).
assert (H42:=fun HH : In 2 (remove 4 B) => H2 (remove_3 HH)).
assert (H43:=fun HH : In 3 (remove 4 B) => H3 (remove_3 HH)).
destruct (In_dec 5 (remove 4 B)) as [H45|H45].
right.
rewrite <- (add_remove H4).
rewrite <- (add_remove H45).
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:cardinal (remove 5 B)=1);
[ rewrite <- (remove_cardinal_1 H5) in H_card; apply eq_add_S; assumption|].
assert (H51:=fun HH : In 1 (remove 5 B) => H1 (remove_3 HH)).
assert (H52:=fun HH : In 2 (remove 5 B) => H2 (remove_3 HH)).
assert (H53:=fun HH : In 3 (remove 5 B) => H3 (remove_3 HH)).
assert (H54:=fun HH : In 4 (remove 5 B) => 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: forall B : t, Subset B town_2 -> cardinal B = 2 ->
{d : elt |In d (diff town_2 B) /\ (forall b : elt, In b B -> familiarity_2 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_2 familiarity_2 familiarity_2_sym familiarity_2_extensional acquintance_2).
Definition social_citizen_2:=AMM11262 town_2 2 population_2 familiarity_2
familiarity_2_sym familiarity_2_extensional acquintance_2.
End example_five_inhabitants.
Extraction "social2" social_citizen_2.