proposition: Lemma collect_diffs : forall (A B : COLTpoint) (H : A <> B) pa pb sp (interp : positive -> COLTpoint), interp pa = A -> interp pb = B -> sp_ok sp interp -> sp_ok (SP.add (pa, pb) sp) interp.
proof: Proof. intros A B HDiff pa pb sp interp HA HB HSP. unfold sp_ok. intros p Hp. apply SPWEqP.MP.Dec.F.mem_2 in Hp. apply SPWEqP.MP.Dec.F.add_iff in Hp. elim Hp; intro HpE. destruct HpE as [HEq1 HEq2]. destruct p as [fstp sndp]. simpl in *. elim (Pos.min_spec pa pb); intro Hmin1; elim (Pos.min_spec fstp sndp); intro Hmin2; destruct Hmin1 as [Hpapb1 Hmin1]; destruct Hmin2 as [Hfpsp1 Hmin2]; elim (Pos.max_spec pa pb); intro Hmax1; elim (Pos.max_spec fstp sndp); intro Hmax2; destruct Hmax1 as [Hpapb2 Hmax1]; destruct Hmax2 as [Hfpsp2 Hmax2]. rewrite Hmin1 in *; rewrite Hmin2 in *; rewrite Hmax1 in *;rewrite Hmax2 in *. rewrite <- HEq1; rewrite <- HEq2; rewrite HA in *; rewrite HB in *; assumption. rewrite <- Pos.ltb_lt in Hfpsp1; rewrite Pos.ltb_antisym in Hfpsp1; rewrite negb_true_iff in Hfpsp1; rewrite Pos.leb_nle in Hfpsp1; contradiction. rewrite <- Pos.ltb_lt in Hpapb1; rewrite Pos.ltb_antisym in Hpapb1; rewrite negb_true_iff in Hpapb1; rewrite Pos.leb_nle in Hpapb1; contradiction. rewrite <- Pos.ltb_lt in Hfpsp1; rewrite Pos.ltb_antisym in Hfpsp1; rewrite negb_true_iff in Hfpsp1; rewrite Pos.leb_nle in Hfpsp1; contradiction. rewrite <- Pos.ltb_lt in Hfpsp2; rewrite Pos.ltb_antisym in Hfpsp2; rewrite negb_true_iff in Hfpsp2; rewrite Pos.leb_nle in Hfpsp2; contradiction. rewrite Hmin1 in *; rewrite Hmin2 in *; rewrite Hmax1 in *;rewrite Hmax2 in *. rewrite <- HEq1; rewrite <- HEq2; rewrite HA in *; rewrite HB in *; assumption. rewrite <- Pos.ltb_lt in Hfpsp2; rewrite Pos.ltb_antisym in Hfpsp2; rewrite negb_true_iff in Hfpsp2; rewrite Pos.leb_nle in Hfpsp2; contradiction. rewrite <- Pos.ltb_lt in Hpapb1; rewrite Pos.ltb_antisym in Hpapb1; rewrite negb_true_iff in Hpapb1; rewrite Pos.leb_nle in Hpapb1; contradiction. rewrite <- Pos.ltb_lt in Hpapb2; rewrite Pos.ltb_antisym in Hpapb2; rewrite negb_true_iff in Hpapb2; rewrite Pos.leb_nle in Hpapb2; contradiction. rewrite <- Pos.ltb_lt in Hpapb2; rewrite Pos.ltb_antisym in Hpapb2; rewrite negb_true_iff in Hpapb2; rewrite Pos.leb_nle in Hpapb2; contradiction. rewrite Hmin1 in *; rewrite Hmin2 in *; rewrite Hmax1 in *;rewrite Hmax2 in *. rewrite <- HEq1; rewrite <- HEq2; rewrite HA in *; rewrite HB in *; intuition. rewrite <- Pos.ltb_lt in Hfpsp1; rewrite Pos.ltb_antisym in Hfpsp1; rewrite negb_true_iff in Hfpsp1; rewrite Pos.leb_nle in Hfpsp1; contradiction. rewrite <- Pos.ltb_lt in Hpapb2; rewrite Pos.ltb_antisym in Hpapb2; rewrite negb_true_iff in Hpapb2; rewrite Pos.leb_nle in Hpapb2; contradiction. rewrite <- Pos.ltb_lt in Hpapb2; rewrite Pos.ltb_antisym in Hpapb2; rewrite negb_true_iff in Hpapb2; rewrite Pos.leb_nle in Hpapb2; contradiction. rewrite <- Pos.ltb_lt in Hfpsp2; rewrite Pos.ltb_antisym in Hfpsp2; rewrite negb_true_iff in Hfpsp2; rewrite Pos.leb_nle in Hfpsp2; contradiction. rewrite Hmin1 in *; rewrite Hmin2 in *; rewrite Hmax1 in *;rewrite Hmax2 in *. rewrite <- HEq1; rewrite <- HEq2; rewrite HA in *; rewrite HB in *; intuition. unfold sp_ok in *. apply HSP. apply SPWEqP.MP.Dec.F.mem_1. assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets