(************************************************************************)
(* Copyright 2007 Milad Niqui                                           *)
(* This file is distributed under the terms of the                      *)
(* GNU Lesser General Public License Version 2.1                        *)
(* A copy of the license can be found at                                *)
(*                  <http://www.gnu.org/licenses/lgpl.txt>              *)
(************************************************************************)

Require Import AMM11262.
Import NatSet GeneralProperties.

Section example_three_inhabitants.
(** Now we find the witness, in a town with three inhabitants; ie, n=1 *)

Definition town_1:= 1++ 2 ++ 3 ++ empty.

Remark population_1 : cardinal town_1 = 2*1 +1.
Proof.
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
 reflexivity.
Qed.

Definition familiarity_1 (m n:elt):Prop := 
  match m,n with
  | 1,2 => True
  | 2,1 => True
  | 2,3 => True
  | 3,2 => True
  | _,_ => False
  end.

Remark familiarity_1_sym:forall m n : elt, familiarity_1 m n -> familiarity_1 n m.
Proof.
(* Goal: forall (m n : elt) (_ : familiarity_1 m n), familiarity_1 n m *)
 intros [|[|[|[|m']]]] [|[|[|[|n']]]]; trivial.
Qed. 

Remark familiarity_1_extensional:forall (m : elt) (n p : E.t), E.eq n p -> familiarity_1 m n -> familiarity_1 m p.
Proof.
(* Goal: forall (m : elt) (n p : E.t) (_ : E.eq n p) (_ : familiarity_1 m n), familiarity_1 m p *)
 intros m n p H1 H2; compute in H1; rewrite <- H1; assumption. 
Qed.

Remark subsets_1: forall B : t, Subset B town_1 -> cardinal B = 1 -> {B [=] 1++empty}+{B[=]2++empty}+{B[=]3++empty}.
Proof.
(* Goal: forall (B : t) (_ : Subset B town_1) (_ : @Logic.eq nat (cardinal B) (S O)), @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
 intros B H_sub H_card.
(* Goal: sumor (sumbool (Equal B (add (S O) empty)) (Equal B (add (S (S O)) empty))) (Equal B (add (S (S (S O))) empty)) *)
 destruct (In_dec 1 B) as [H1|H1].
  (* IN 1 B *)
  left; left;
  rewrite <- (add_remove H1); generalize (remove_cardinal_1 H1); rewrite H_card; intro H_eq;
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
  rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity...
  (* ~ In 1 B *)
(* Goal: sumor (sumbool (Equal B (add (S O) empty)) (Equal B (add (S (S O)) empty))) (Equal B (add (S (S (S O))) empty)) *)
  destruct (In_dec 2 B) as [H2|H2].
   (* In 2 B *)
   left; right;
   rewrite <- (add_remove H2); generalize (remove_cardinal_1 H2); rewrite H_card; intro H_eq;
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
   rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity...
   (* ~ In 2 B *)
(* Goal: sumor (sumbool (Equal B (add (S O) empty)) (Equal B (add (S (S O)) empty))) (Equal B (add (S (S (S O))) empty)) *)
   destruct (In_dec 3 B) as [H3|H3].
    (* In 3 B *)
    right;
    rewrite <- (add_remove H3); generalize (remove_cardinal_1 H3); rewrite H_card; intro H_eq;
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
    rewrite (empty_is_empty_1 (cardinal_inv_1 (eq_add_S _ _ H_eq))); reflexivity...
    (* ~ In 3 B *)
(* Goal: sumor (sumbool (Equal B (add (S O) empty)) (Equal B (add (S (S O)) empty))) (Equal B (add (S (S (S O))) empty)) *)
    apply False_rec.
(* Goal: False *)
    destruct (cardinal_inv_2 H_card) as [b Hb].
(* Goal: False *)
    destruct (NatSet.E.eq_dec b 1) as [Hb1|Hb1].
(* Goal: False *)
(* Goal: False *)
     apply H1; rewrite <- Hb1; assumption.
(* Goal: False *)
     destruct (NatSet.E.eq_dec b 2) as [Hb2|Hb2].
(* Goal: False *)
(* Goal: False *)
     apply H2; rewrite <- Hb2; assumption.
(* Goal: False *)
     destruct (NatSet.E.eq_dec b 3) as [Hb3|Hb3].
(* Goal: False *)
(* Goal: False *)
      apply H3; rewrite <- Hb3; assumption.

(* Goal: False *)
      assert (Hb_town:=H_sub _ Hb).
(* Goal: False *)
      unfold town_1 in Hb_town.
(* Goal: False *)
      destruct (proj1 (FM.add_iff _ _ b) Hb_town) as [Hb1_town|Hb1_town].
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
       apply Hb1; rewrite Hb1_town; reflexivity.
(* Goal: False *)
       destruct (proj1 (FM.add_iff _ _ b) Hb1_town) as [Hb2_town|Hb2_town].
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
        apply Hb2; rewrite Hb2_town; reflexivity.
(* Goal: False *)
        destruct (proj1 (FM.add_iff _ _ b) Hb2_town) as [Hb3_town|Hb3_town].
(* Goal: @Logic.eq nat (cardinal town_1) (Nat.add (Nat.mul (S (S O)) (S O)) (S O)) *)
         apply Hb3; rewrite Hb3_town; reflexivity.
(* Goal: False *)
         apply (proj1 (FM.empty_iff b) Hb3_town).
Qed.
      

Remark acquintance_1: forall B : t, Subset B town_1 -> cardinal B = 1 -> 
          {d : elt |In d (diff town_1 B) /\ (forall b : elt, In b B -> familiarity_1 d b)}.
Proof.
(* Goal: forall (B : t) (_ : Subset B town_1) (_ : @Logic.eq nat (cardinal B) (S O)), @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
 intros B H_sub H_card.
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
 destruct (subsets_1 B H_sub H_card) as [[HB1|HB2]|HB3].
  (* B={1} *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
  exists 2; split.
(* Goal: In (S (S O)) (diff town_1 B) *)
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S (S O)) b *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
   rewrite HB1; apply mem_2; trivial.
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S (S O)) b *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
   intro b; rewrite HB1; intro Hb.
(* Goal: familiarity_1 (S (S O)) b *)
   destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
(* Goal: familiarity_1 (S (S O)) b *)
(* Goal: familiarity_1 (S (S O)) b *)
    compute in H; rewrite <- H; simpl; trivial.
(* Goal: familiarity_1 (S (S O)) b *)
    apply False_ind; apply (proj1 (FM.empty_iff b) H).
  (* B={2} *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
  exists 1; split.
(* Goal: In (S O) (diff town_1 B) *)
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S O) b *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
   rewrite HB2; apply mem_2; trivial.
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S O) b *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
   intro b; rewrite HB2; intro Hb.
(* Goal: familiarity_1 (S (S O)) b *)
   destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
(* Goal: familiarity_1 (S (S O)) b *)
(* Goal: familiarity_1 (S (S O)) b *)
    compute in H; rewrite <- H; simpl; trivial.
(* Goal: familiarity_1 (S (S O)) b *)
    apply False_ind; apply (proj1 (FM.empty_iff b) H).
  (* B={3} *)
(* Goal: @sig elt (fun d : elt => and (In d (diff town_1 B)) (forall (b : elt) (_ : In b B), familiarity_1 d b)) *)
  exists 2; split.
(* Goal: In (S (S O)) (diff town_1 B) *)
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S (S O)) b *)
   rewrite HB3; apply mem_2; trivial.
(* Goal: forall (b : elt) (_ : In b B), familiarity_1 (S (S O)) b *)
   intro b; rewrite HB3; intro Hb.
(* Goal: familiarity_1 (S (S O)) b *)
   destruct (proj1 (FM.add_iff _ _ b) Hb) as [H|H].
(* Goal: familiarity_1 (S (S O)) b *)
(* Goal: familiarity_1 (S (S O)) b *)
    compute in H; rewrite <- H; simpl; trivial.
(* Goal: familiarity_1 (S (S O)) b *)
    apply False_ind; apply (proj1 (FM.empty_iff b) H).
Defined.

Check (AMM11262 town_1 1 population_1 familiarity_1 familiarity_1_sym familiarity_1_extensional acquintance_1).

Definition social_citizen_1:=AMM11262 town_1 1 population_1 familiarity_1 
                                      familiarity_1_sym familiarity_1_extensional acquintance_1.


End example_three_inhabitants.

Extraction "social1" social_citizen_1.
