proposition: Lemma mca_pick_variety_aux_pca : forall m cp s1 s2 ss x interp, ss_ok ss interp -> SS.In s1 ss -> SS.In s2 ss -> memCPAux (S m) cp (S.union s1 s2) = true -> pick_variety_aux (S.inter s1 s2) x = true -> pred_conj_aux coinc (S (S m)) (interp_CP cp interp) (interp_CP x interp).
proof: Proof. induction m; intros cp s1 s2 ss x interp HSSOK HIn1 HIn2 Hmemcp Hhtspa. unfold pred_conj_aux. unfold nat_rect. split. assert (HIn : InCP (headCP cp) cp) by (unfold InCP; simpl; auto). assert (HElim : S.mem (headCP cp) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption). rewrite SWP.FM.union_b in HElim. apply orb_true_iff in HElim. elim HElim; clear HElim; intro HElim. apply ss_ok_inter_ok1 with ss s1 s2; assumption. apply ss_ok_inter_ok2 with ss s1 s2; assumption. split. assert (HIn : InCP (headCP (tailCP cp)) cp) by (unfold InCP; simpl; auto). assert (HElim : S.mem (headCP (tailCP cp)) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption). rewrite SWP.FM.union_b in HElim. apply orb_true_iff in HElim. elim HElim; clear HElim; intro HElim. apply ss_ok_inter_ok1 with ss s1 s2; assumption. apply ss_ok_inter_ok2 with ss s1 s2; assumption. assert (HIn : InCP (tailCP (tailCP cp)) cp) by (unfold InCP; simpl; auto). assert (HElim : S.mem (tailCP (tailCP cp)) (S.union s1 s2) = true) by (apply memCPAuxOK with 1 cp; assumption). rewrite SWP.FM.union_b in HElim. apply orb_true_iff in HElim. elim HElim; clear HElim; intro HElim. apply ss_ok_inter_ok1 with ss s1 s2; assumption. apply ss_ok_inter_ok2 with ss s1 s2; assumption. rewrite pcaHdTl. split. assert (HIn : InCP (headCP cp) cp) by (unfold InCP; simpl; auto). assert (HElim : S.mem (headCP cp) (S.union s1 s2) = true) by (apply memCPAuxOK with (S (S m)) cp; assumption). rewrite SWP.FM.union_b in HElim. apply orb_true_iff in HElim. elim HElim; clear HElim; intro HElim. apply ss_ok_inter_ok1 with ss s1 s2; assumption. apply ss_ok_inter_ok2 with ss s1 s2; assumption. rewrite <- interp_CPTlOK. apply IHm with s1 s2 ss; try assumption. apply memCPAuxTlOK. assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets