proposition: Lemma collect_cols : forall (A B C : COLTpoint) (HCol : CTCol A B C) pa pb pc ss (interp : positive -> COLTpoint), interp pa = A -> interp pb = B -> interp pc = C -> ss_ok ss interp -> ss_ok (SS.add (S.add pa (S.add pb (S.add pc S.empty))) ss) interp.
proof: Proof. intros A B C HCol pa pb pc ss interp HA HB HC HSS. unfold ss_ok. intros s Hs. intros p1 p2 p3 Hmem. apply SSWEqP.MP.Dec.F.mem_2 in Hs. apply SSWEqP.MP.Dec.F.add_iff in Hs. do 2 (rewrite andb_true_iff in Hmem). destruct Hmem as [[Hmem1 Hmem2] Hmem3]. elim Hs; intro HsE. assert (HmemR : forall p, S.mem p (S.add pa (S.add pb (S.add pc S.empty))) = S.mem p s) by (intros; apply SWP.Dec.F.mem_m; auto). rewrite <- HmemR in Hmem1. rewrite <- HmemR in Hmem2. rewrite <- HmemR in Hmem3. clear HmemR. elim (Pos.eq_dec pa p1); intro Hpap1. rewrite Hpap1 in *; rewrite HA. elim (Pos.eq_dec p1 p2); intro Hp1p2. rewrite Hp1p2 in *; rewrite HA. apply CTcol_trivial_1. rewrite SWP.Dec.F.add_neq_b in Hmem2. elim (Pos.eq_dec pb p2); intro Hpbp2. rewrite Hpbp2 in *; rewrite HB. elim (Pos.eq_dec p3 p1); intro Hp3p1; elim (Pos.eq_dec p3 p2); intro Hp3p2. rewrite Hp3p2; rewrite HB; apply CTcol_trivial_2. rewrite Hp3p1; rewrite HA; apply CTcol_permutation_1; apply CTcol_trivial_1. rewrite Hp3p2; rewrite HB; apply CTcol_trivial_2. do 2 (rewrite SWP.Dec.F.add_neq_b in Hmem3). rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite <- Hmem3; rewrite HC; assumption. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem2. rewrite <- SWP.singleton_equal_add in Hmem2. apply SWP.Dec.F.mem_iff in Hmem2. apply SWP.Dec.F.singleton_1 in Hmem2. rewrite <- Hmem2 in *; rewrite HC. elim (Pos.eq_dec p3 p1); intro Hp3p1; elim (Pos.eq_dec p3 p2); intro Hp3p2. rewrite Hp3p2 in *; rewrite Hmem2 in *; rewrite HC; apply CTcol_trivial_2. rewrite Hp3p1 in *; rewrite HA; apply CTcol_permutation_1; apply CTcol_trivial_1. rewrite Hp3p2 in *; rewrite Hmem2 in *; rewrite HC; apply CTcol_trivial_2. rewrite SWP.Dec.F.add_neq_b in Hmem3. elim (Pos.eq_dec p3 pb); intro Hp3pb. rewrite Hp3pb in *; rewrite HB; apply CTcol_permutation_5; assumption. rewrite SWP.Dec.F.add_neq_b in Hmem3. rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite Hmem3 in *; contradiction. intuition. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem1. elim (Pos.eq_dec p1 pb); intro Hp1pb. rewrite Hp1pb in *; rewrite HB. elim (Pos.eq_dec pa p2); intro Hpap2. rewrite Hpap2 in *; rewrite HA. elim (Pos.eq_dec p3 p2); intro Hp3p2; elim (Pos.eq_dec p3 pb); intro Hp3pb. rewrite Hp3pb; rewrite HB; apply CTcol_permutation_1; apply CTcol_trivial_1. rewrite Hp3p2; rewrite HA; apply CTcol_trivial_2. rewrite Hp3pb; rewrite HB; apply CTcol_permutation_1; apply CTcol_trivial_1. do 2 (rewrite SWP.Dec.F.add_neq_b in Hmem3). rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite <- Hmem3; rewrite HC; apply CTcol_permutation_4; assumption. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem2. elim (Pos.eq_dec p2 pb); intro Hp2pb. rewrite Hp2pb; rewrite HB; apply CTcol_trivial_1. rewrite SWP.Dec.F.add_neq_b in Hmem2. rewrite <- SWP.singleton_equal_add in Hmem2. apply SWP.Dec.F.mem_iff in Hmem2. apply SWP.Dec.F.singleton_1 in Hmem2. rewrite <- Hmem2 in *; rewrite HC. elim (Pos.eq_dec p3 p1); intro Hp3p1; elim (Pos.eq_dec p3 p2); intro Hp3p2. rewrite Hp3p2 in *; rewrite Hmem2 in *; rewrite HC; apply CTcol_trivial_2. rewrite Hp3p1 in *; rewrite Hp1pb; rewrite HB; apply CTcol_permutation_1; apply CTcol_trivial_1. rewrite Hp3p2 in *; rewrite Hmem2 in *; rewrite HC; apply CTcol_trivial_2. elim (Pos.eq_dec p3 pa); intro Hp3pa. rewrite Hp3pa; rewrite HA; apply CTcol_permutation_1; assumption. rewrite SWP.Dec.F.add_neq_b in Hmem3. elim (Pos.eq_dec p3 pb); intro Hp3pb. rewrite Hp3pb in *; rewrite HB; apply CTcol_permutation_5; apply CTcol_trivial_1. rewrite SWP.Dec.F.add_neq_b in Hmem3. rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite Hmem3 in *; contradiction. intuition. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem1. rewrite <- SWP.singleton_equal_add in Hmem1. apply SWP.Dec.F.mem_iff in Hmem1. apply SWP.Dec.F.singleton_1 in Hmem1. rewrite <- Hmem1 in *; rewrite HC. elim (Pos.eq_dec pa p2); intro Hpap2. rewrite Hpap2 in *; rewrite HA. elim (Pos.eq_dec p3 p2); intro Hp3p2; elim (Pos.eq_dec p3 pb); intro Hp3pb. rewrite Hp3pb; rewrite HB; apply CTcol_permutation_2; assumption. rewrite Hp3p2; rewrite HA; apply CTcol_trivial_2. rewrite Hp3pb; rewrite HB; apply CTcol_permutation_2; assumption. do 2 (rewrite SWP.Dec.F.add_neq_b in Hmem3). rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite <- Hmem3; rewrite HC; apply CTcol_permutation_1; apply CTcol_trivial_1. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem2. elim (Pos.eq_dec p2 pb); intro Hp2pb. rewrite Hp2pb; rewrite HB. elim (Pos.eq_dec p3 pa); intro Hp3pa; elim (Pos.eq_dec p3 pb); intro Hp3pb. rewrite Hp3pa; rewrite HA; apply CTcol_permutation_3; assumption. rewrite Hp3pa; rewrite HA; apply CTcol_permutation_3; assumption. rewrite Hp3pb; rewrite HB; apply CTcol_trivial_2. do 2 (rewrite SWP.Dec.F.add_neq_b in Hmem3). rewrite <- SWP.singleton_equal_add in Hmem3. apply SWP.Dec.F.mem_iff in Hmem3. apply SWP.Dec.F.singleton_1 in Hmem3. rewrite <- Hmem3 in *; rewrite HC; apply CTcol_permutation_1; apply CTcol_trivial_1. intuition. intuition. intuition. rewrite SWP.Dec.F.add_neq_b in Hmem2. rewrite <- SWP.singleton_equal_add in Hmem2. apply SWP.Dec.F.mem_iff in Hmem2. apply SWP.Dec.F.singleton_1 in Hmem2. rewrite <- Hmem2 in *; rewrite HC; apply CTcol_trivial_1. intuition. intuition. intuition. intuition. unfold ss_ok in *. apply HSS with s. apply SSWEqP.MP.Dec.F.mem_1. assumption. rewrite Hmem1; rewrite Hmem2; rewrite Hmem3; reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets