proposition: Lemma identify_lines_ok : forall ss sp interp, ss_ok ss interp -> sp_ok sp interp -> ss_ok (identify_lines ss sp) interp.
proof: Proof. intros ss sp interp HSS HSP. apply (let P interp ss sp newss := ss_ok ss interp -> sp_ok sp interp -> ss_ok newss interp in identify_lines_ind (P interp)); try assumption. intros. assumption. clear HSS; clear HSP; clear ss; clear sp. intros ss sp suitablepairofsets s1 s2 Hs1s2 auxsetofsets auxset newss H HSS HSP. assert (Hs1 := Hs1s2). assert (Hs2 := Hs1s2). apply pick_lines_ok_1 in Hs1. apply pick_lines_ok_2 in Hs2. apply SSWEqP.MP.Dec.F.remove_3 in Hs2. apply H; try assumption; clear H. intros s Hmem p1 p2 p3 Hmemp. do 2 (rewrite andb_true_iff in Hmemp). destruct Hmemp as [[Hmemp1 Hmemp2] Hmemp3]. unfold newss in Hmem; clear newss. elim (SS.E.eq_dec auxset s); intro HEq. rewrite <- HEq in *; clear HEq; clear s. unfold suitablepairofsets in Hs1s2; clear suitablepairofsets. unfold pick_lines in Hs1s2. case_eq (exists_witness (fun s : SS.elt => match pick_lines_aux s (SS.remove s ss) sp with | Some _ => true | None => false end) ss); try (intro HEW; rewrite HEW in *; discriminate). intros e1 HEW; rewrite HEW in *; clear HEW. unfold pick_lines_aux in *. case_eq (exists_witness (fun s2 : SS.elt => pick_line (S.inter e1 s2) sp) (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_line (S.inter s1 s2) sp). clear HEW; intro HEW. unfold pick_line in HEW. apply SPWEqP.exists_mem_4 in HEW; try (apply proper_00). destruct HEW as [x [HmemSP HmemS]]. rewrite andb_true_iff in HmemS; destruct HmemS as [Hmemfsts Hmemsnds]. apply HSP in HmemSP. apply SWP.Dec.F.mem_2 in Hmemfsts. apply S.inter_spec in Hmemfsts. destruct Hmemfsts as [Hfss1 Hfss2]. apply SWP.Dec.F.mem_2 in Hmemsnds. apply S.inter_spec in Hmemsnds. destruct Hmemsnds as [Hsss1 Hsss2]. unfold auxset in *. apply CTcol3 with (interp (fstpp(x))) (interp (sndpp(x))); try assumption. apply SWP.Dec.F.mem_2 in Hmemp1. apply SWP.Dec.F.union_1 in Hmemp1. elim (Hmemp1); intro HInp1. apply HSS with s1. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; assumption. apply HSS with s2. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; assumption. apply SWP.Dec.F.mem_2 in Hmemp2. apply SWP.Dec.F.union_1 in Hmemp2. elim (Hmemp2); intro HInp2. apply HSS with s1. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; assumption. apply HSS with s2. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; assumption. apply SWP.Dec.F.mem_2 in Hmemp3. apply SWP.Dec.F.union_1 in Hmemp3. elim (Hmemp3); intro HInp3. apply HSS with s1. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; assumption. apply HSS with s2. apply SSWP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff). repeat split; apply SWP.Dec.F.mem_1; 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. do 2 (rewrite andb_true_iff). repeat split; assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets