proposition: Lemma subst_sp_ok : 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 (subst_in_sp pa pb sp) interp.
proof: Proof. intros A B H pa pb sp interp HA HB HSP. unfold subst_in_sp. unfold sp_ok. intros p Hp. apply SPWEqP.MP.Dec.F.mem_2 in Hp. do 2 rewrite SPWEqP.MP.Dec.F.union_iff in Hp. elim Hp; intro HInAux; clear Hp. assert (HSPM : sp_ok (fst_sp (partition_sp_1 pb sp)) interp). intros p' Hp'. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. unfold partition_sp_1 in Hp'. apply SP.partition_spec1 in Hp'; try apply proper_6. apply SPWEqP.MP.Dec.F.filter_1 in Hp'; try apply proper_6. unfold sp_ok in HSP. apply HSP; try assumption. apply SPWEqP.MP.Dec.F.mem_1; assumption. clear HSP. elim HInAux; intro HIn; clear HInAux. assert (HSPF : sp_ok (fst_sp (partition_sp_2 pb (fst_sp (partition_sp_1 pb sp)))) interp). intros p' Hp'. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. unfold partition_sp_1 in Hp'. apply SP.partition_spec1 in Hp'; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_1 in Hp'; try apply proper_8. unfold sp_ok in HSPM. apply HSPM; try assumption. apply SPWEqP.MP.Dec.F.mem_1; assumption. clear HSPM. assert (HSPF' : sp_ok (SP.fold (subst_in_sp_aux_1 pa) (fst_sp (partition_sp_2 pb (fst_sp (partition_sp_1 pb sp)))) SP.empty) interp). apply SPWEqP.MP.fold_rec_nodep; try apply sp_ok_empty. clear HIn. intros x a HInRec HSPRec. intros p' Hp'. unfold subst_in_sp_aux_1 in *. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. rewrite SPWEqP.MP.Dec.F.add_iff in Hp'. elim Hp'; intro HIn; clear Hp'. destruct HIn as [HEq1 HEq2]. rewrite <- HEq1; rewrite <- HEq2. unfold new_pair_1. clear HSPRec; clear a. elim (Pos.min_spec pa (sndpp(x))); intro Hmin. destruct Hmin as [HLt Hmin]. assert (Hmax : Pos.max pa (sndpp(x)) = (sndpp(x))) by (apply Pos.max_r; apply Pos.lt_le_incl; assumption). assert (HF : fstpp(pa, sndpp(x)) = pa) by (unfold fstpp; assumption). assert (HS : sndpp(pa, sndpp(x)) = sndpp(x)) by (unfold sndpp; assumption). rewrite HF; rewrite HS. assert (Hpb : fstpp(x) = pb). unfold partition_sp_2 in HInRec. apply SP.partition_spec1 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_2 in HInRec; try apply proper_8. apply Ndec.Peqb_complete. assumption. intro HEq4. unfold sp_ok in HSPF. apply SPWEqP.MP.Dec.F.mem_1 in HInRec. apply (HSPF x) in HInRec. apply HInRec. rewrite Hpb; rewrite <- HEq4; rewrite HA; rewrite HB; rewrite H; reflexivity. destruct Hmin as [HLe Hmin]. assert (Hmax : Pos.max pa (sndpp(x)) = pa) by (apply Pos.max_l; assumption). assert (HF : fstpp(pa, sndpp(x)) = sndpp(x)) by (unfold fstpp; assumption). assert (HS : sndpp(pa, sndpp(x)) = pa) by (unfold sndpp; assumption). rewrite HF; rewrite HS. assert (Hpb : fstpp(x) = pb). unfold partition_sp_2 in HInRec. apply SP.partition_spec1 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_2 in HInRec; try apply proper_8. apply Ndec.Peqb_complete. assumption. intro HEq4. unfold sp_ok in HSPF. apply SPWEqP.MP.Dec.F.mem_1 in HInRec. apply (HSPF x) in HInRec. apply HInRec. rewrite Hpb; rewrite HEq4; rewrite HA; rewrite HB; rewrite H; reflexivity. unfold sp_ok in HSPRec. apply HSPRec. apply SPWEqP.MP.Dec.F.mem_1; assumption. clear HSPF; assert (HSPF := HSPF'); clear HSPF'. unfold sp_ok in HSPF. apply HSPF. apply SPWEqP.MP.Dec.F.mem_1; assumption. assert (HSPS : sp_ok (snd_sp (partition_sp_2 pb (fst_sp (partition_sp_1 pb sp)))) interp). intros p' Hp'. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. unfold partition_sp_1 in Hp'. apply SP.partition_spec2 in Hp'; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_1 in Hp'; try apply proper_9. unfold sp_ok in HSPM. apply HSPM; try assumption. apply SPWEqP.MP.Dec.F.mem_1; assumption. clear HSPM. assert (HSPS' : sp_ok (SP.fold (subst_in_sp_aux_2 pa) (snd_sp (partition_sp_2 pb (fst_sp (partition_sp_1 pb sp)))) SP.empty) interp). apply SPWEqP.MP.fold_rec_nodep; try apply sp_ok_empty. clear HIn. intros x a HInRec HSPRec. intros p' Hp'. unfold subst_in_sp_aux_2 in *. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. rewrite SPWEqP.MP.Dec.F.add_iff in Hp'. elim Hp'; intro HIn; clear Hp'. destruct HIn as [HEq1 HEq2]. rewrite <- HEq1; rewrite <- HEq2. unfold new_pair_2. clear HSPRec; clear a. elim (Pos.min_spec (fstpp(x)) pa); intro Hmin. destruct Hmin as [HLt Hmin]. assert (Hmax : Pos.max (fstpp(x)) pa = pa) by (apply Pos.max_r; apply Pos.lt_le_incl; assumption). assert (HF : fstpp(fstpp(x), pa) = fstpp(x)) by (unfold fstpp; assumption). assert (HS : sndpp(fstpp(x), pa) = pa) by (unfold sndpp; assumption). rewrite HF; rewrite HS. assert (Hpb : sndpp(x) = pb). assert (HIn : SP.In x (fst_sp (partition_sp_1 pb sp))). unfold partition_sp_2 in HInRec. apply SP.partition_spec2 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_1 in HInRec; try apply proper_9. assumption. unfold partition_sp_2 in HInRec. apply SP.partition_spec2 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_2 in HInRec; try apply proper_9. unfold partition_sp_1 in HIn. apply SP.partition_spec1 in HIn; try apply proper_6. apply SPWEqP.MP.Dec.F.filter_2 in HIn; try apply proper_6. apply orb_true_iff in HIn. elim HIn; intro HEqb; clear HIn. apply Peqb_true_eq in HEqb. apply negb_true_iff in HInRec. apply Pos.eqb_neq in HInRec. rewrite HEqb in HInRec. intuition. apply Peqb_true_eq in HEqb. assumption. intro HEq4. unfold sp_ok in HSPS. apply SPWEqP.MP.Dec.F.mem_1 in HInRec. apply (HSPS x) in HInRec. apply HInRec. rewrite Hpb; rewrite HEq4; rewrite HA; rewrite HB; rewrite H; reflexivity. destruct Hmin as [HLe Hmin]. assert (Hmax : Pos.max (fstpp(x)) pa = fstpp(x)) by (apply Pos.max_l; assumption). assert (HF : fstpp(fstpp(x), pa) = pa) by (unfold fstpp; assumption). assert (HS : sndpp(fstpp(x), pa) = fstpp(x)) by (unfold sndpp; assumption). rewrite HF; rewrite HS. assert (Hpb : sndpp(x) = pb). assert (HIn : SP.In x (fst_sp (partition_sp_1 pb sp))). unfold partition_sp_2 in HInRec. apply SP.partition_spec2 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_1 in HInRec; try apply proper_9. assumption. unfold partition_sp_2 in HInRec. apply SP.partition_spec2 in HInRec; try apply proper_8. apply SPWEqP.MP.Dec.F.filter_2 in HInRec; try apply proper_9. unfold partition_sp_1 in HIn. apply SP.partition_spec1 in HIn; try apply proper_6. apply SPWEqP.MP.Dec.F.filter_2 in HIn; try apply proper_6. apply orb_true_iff in HIn. elim HIn; intro HEqb; clear HIn. apply Peqb_true_eq in HEqb. apply negb_true_iff in HInRec. apply Pos.eqb_neq in HInRec. rewrite HEqb in HInRec. intuition. apply Peqb_true_eq in HEqb. assumption. intro HEq4. unfold sp_ok in HSPS. apply SPWEqP.MP.Dec.F.mem_1 in HInRec. apply (HSPS x) in HInRec. apply HInRec. rewrite Hpb; rewrite <- HEq4; rewrite HA; rewrite HB; rewrite H; reflexivity. unfold sp_ok in HSPRec. apply HSPRec. apply SPWEqP.MP.Dec.F.mem_1; assumption. clear HSPS; assert (HSPS := HSPS'); clear HSPS'. unfold sp_ok in HSPS. apply HSPS. apply SPWEqP.MP.Dec.F.mem_1; assumption. assert (HIn := HInAux); clear HInAux. assert (HSPK : sp_ok (snd_sp (partition_sp_1 pb sp)) interp). intros p' Hp'. apply SPWEqP.MP.Dec.F.mem_2 in Hp'. unfold partition_sp_1 in Hp'. apply SP.partition_spec2 in Hp'; try apply proper_6. apply SPWEqP.MP.Dec.F.filter_1 in Hp'; try apply proper_7. unfold sp_ok in HSP. apply HSP; try assumption. apply SPWEqP.MP.Dec.F.mem_1; assumption. unfold sp_ok in HSPK. apply HSPK; try assumption. apply SPWEqP.MP.Dec.F.mem_1; assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets