proposition: Lemma identify_varieties_ok : forall ss st interp, ss_ok ss interp -> st_ok st interp -> ss_ok (identify_varieties ss st) interp.
proof: Proof. intros ss st interp HSS HST. apply (let P interp ss st newss := ss_ok ss interp -> st_ok st interp -> ss_ok newss interp in identify_varieties_ind (P interp)); try assumption. intros. assumption. clear HSS; clear HST; clear ss; clear st. intros ss st varieties s1 s2 Hs1s2 auxsetofsets auxset newss H HSS HST. assert (Hs1 := Hs1s2). assert (Hs2 := Hs1s2). apply pick_varieties_ok_1 in Hs1. apply pick_varieties_ok_2 in Hs2. apply SSWEqP.MP.Dec.F.remove_3 in Hs2. apply H; try assumption; clear H. intros s Hmem cp Hmemcp. unfold newss in Hmem; clear newss. elim (SS.E.eq_dec auxset s); intro HEq. assert (HEq' : memCP cp auxset = memCP cp s) by (apply memCPProper; trivial). rewrite <- HEq in *; rewrite <- HEq' in *; clear HEq; clear HEq'; clear s. unfold varieties in Hs1s2; clear varieties. unfold pick_varieties in Hs1s2. case_eq (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some _ => true | None => false end) ss); try (intro HEW; rewrite HEW in *; discriminate). intros e1 HEW; rewrite HEW in *; clear HEW. unfold pick_varieties_aux in *. case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (SS.remove e1 ss)); try (intro HEW; rewrite HEW in *; discriminate). intros e2 HEW; rewrite HEW in *. injection Hs1s2; intros He2s2 He1s1. rewrite He2s2 in *; rewrite He1s1 in *; clear He2s2; clear He1s1; clear Hs1s2; clear e2; clear e1. case_eq (pick_variety (S.inter s1 s2) st). clear HEW; intro HEW. unfold pick_variety in HEW. apply STexists_mem_4 in HEW; try (intros x y Hxy; destruct Hxy as [Hxyfst Hxysnd]; rewrite Hxyfst; rewrite Hxysnd; reflexivity); try (apply proper_00). destruct HEW as [x [HmemST1 HmemST2]]. apply HST in HmemST1. apply coinc_n with (interp_CP x interp); try assumption. unfold pred_conj. apply mca_pick_variety_aux_pca with s1 s2 ss; assumption. intro HEW2; unfold exists_witness in *; apply SS.choose_spec1 in HEW. apply SSWEqP.MP.Dec.F.filter_2 in HEW; try apply proper_1. rewrite HEW2 in *; discriminate. rewrite SSWP.Dec.F.add_neq_b in Hmem; try assumption. apply HSS with s. unfold auxsetofsets in *. apply SSWEqP.MP.Dec.F.mem_2 in Hmem. do 2 (apply SSWEqP.MP.Dec.F.remove_3 in Hmem). apply SSWEqP.MP.Dec.F.mem_1. assumption. assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets