proposition: Lemma identify_lengths_ok : forall ss interp, ss_ok ss interp -> ss_ok (identify_lengths ss) interp.
proof: Proof. intros ss interp HSS. apply (let P ss newss := ss_ok ss interp -> ss_ok newss interp in identify_lengths_ind P); try assumption. intros. assumption. clear HSS ss. intros ss suitablepairofsets s1 s2 Hs1s2 auxsetofsets auxset newss H HSS. assert (Hs1 := Hs1s2). assert (Hs2 := Hs1s2). apply pick_lengths_ok_1 in Hs1. apply pick_lengths_ok_2 in Hs2. apply SSPWEqP.MP.Dec.F.remove_3 in Hs2. apply H; clear H. intros s Hmem p1 p2 p3 p4 Hmemp. unfold newss in Hmem; clear newss. elim (SSP.E.eq_dec auxset s); intro HEq. rewrite <- HEq in *; clear HEq Hmem s. unfold suitablepairofsets in Hs1s2; clear suitablepairofsets. unfold pick_lengths in Hs1s2. case_eq (exists_witness (fun s : SSP.elt => match pick_lengths_aux s (SSP.remove s ss) with | Some _ => true | None => false end) ss); [|intro HEW; rewrite HEW in Hs1s2; discriminate Hs1s2]. intros e1 HEW; rewrite HEW in *; clear HEW. unfold pick_lengths_aux in *. case_eq (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter e1 s2))) (SSP.remove e1 ss)); [|intro HEW; rewrite HEW in Hs1s2; discriminate Hs1s2]. intros e2 HEW; rewrite HEW in *. injection Hs1s2; intros He2s2 He1s1. rewrite He2s2, He1s1 in *; clear He2s2 He1s1 Hs1s2 e2 e1. apply SSP.choose_spec1, SSPWEqP.MP.Dec.F.filter_2 in HEW; [|apply proper_1]. apply eq_sym, negb_sym, not_true_iff_false in HEW. rewrite SP.is_empty_spec, SPWP.cardinal_Empty in HEW. apply SPWP.cardinal_inv_2b in HEW. destruct HEW as [(e1,e2) He]. apply SP.inter_spec in He. destruct He as [Hes1 Hes2]. rewrite andb_true_iff in Hmemp. destruct Hmemp as [Hmemp1 Hmemp2]. cut (forall p q, SP.mem (p, q) auxset = true -> CTCong (interp e1) (interp e2) (interp p) (interp q)). intro Haux. apply CTcong_trans with (interp e1) (interp e2); [apply CTcong_sym|]; apply Haux; assumption. intros p q Hmemp. apply SPWP.Dec.F.mem_2, SPWP.Dec.F.union_1 in Hmemp. rewrite SSPWP.Dec.F.mem_iff in *. rewrite 2 SPWP.Dec.F.mem_iff in *. destruct Hmemp; [apply (HSS s1 Hs1)|apply (HSS s2 Hs2)]; apply andb_true_iff; split; assumption. rewrite SSPWP.Dec.F.add_neq_b in Hmem; [|assumption]. apply SSPWEqP.MP.Dec.F.mem_2 in Hmem. do 2 (apply SSPWEqP.MP.Dec.F.remove_3 in Hmem). apply SSPWEqP.MP.Dec.F.mem_1 in Hmem. apply (HSS s); assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets