proposition: Lemma subst_ss_ok : forall (A B : COLTpoint) (H : A = B) pa pb ss (interp : positive -> COLTpoint), interp pa = A -> interp pb = B -> ss_ok ss interp -> ss_ok (subst_in_ss pa pb ss) interp.
proof: Proof. intros A B H pa pb ss interp HA HB HSS. unfold subst_in_ss. unfold ss_ok. intros s Hs. intros p1 p2 p3 Hmem. apply SSWEqP.MP.Dec.F.mem_2 in Hs. rewrite SSWEqP.MP.Dec.F.union_iff in Hs. elim Hs; intro HIn; clear Hs. assert (HSSF : ss_ok (fst_ss (partition_ss pb ss)) interp). clear Hmem; clear p1; clear p2; clear p3. intros s' Hs'. intros. apply SSWEqP.MP.Dec.F.mem_2 in Hs'. unfold partition in Hs'. apply SS.partition_spec1 in Hs'; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_1 in Hs'; try apply proper_4. unfold ss_ok in HSS. apply HSS with s'; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. assert (HSSF' : ss_ok (SS.fold (subst_in_ss_aux pa pb) (fst_ss (partition_ss pb ss)) SS.empty) interp). apply SSWEqP.MP.fold_rec_nodep; try apply ss_ok_empty. intros x a HIn1 HSSa. clear Hmem; clear p1; clear p2; clear p3. intros s' Hs'. intros p1 p2 p3 Hmem. unfold subst_in_ss_aux in *. apply SSWEqP.MP.Dec.F.mem_2 in Hs'. rewrite SSWEqP.MP.Dec.F.add_iff in Hs'. elim Hs'; intro HIn2; clear Hs'. unfold subst_in_set in HIn2. clear HIn; clear s; assert (HEq := HIn2); clear HIn2; assert (HIn := HIn1); clear HIn1. elim (Pos.eq_dec pb p1); intro Hp1; elim (Pos.eq_dec pb p2); intro Hp2; elim (Pos.eq_dec pb p3); intro Hp3. subst. apply CTcol_trivial_1. subst. apply CTcol_trivial_1. subst. apply CTcol_permutation_4; apply CTcol_trivial_2. subst. do 2 (rewrite andb_true_iff in Hmem). destruct Hmem as [[Hmem1' Hmem2'] Hmem3']. assert (Hmem1 : S.mem p1 x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. elim (Pos.eq_dec pa p2); intro Hpap2. subst; rewrite HB; apply CTcol_trivial_1. assert (Hmem2 : S.mem p2 x = true). rewrite <- HEq in Hmem2'. rewrite SWP.Dec.F.add_neq_b in Hmem2'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem2'; assumption. elim (Pos.eq_dec pa p3); intro Hpap3. subst; rewrite HB; apply CTcol_permutation_4; apply CTcol_trivial_2. assert (Hmem3 : S.mem p3 x = true). rewrite <- HEq in Hmem3'. rewrite SWP.Dec.F.add_neq_b in Hmem3'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem3'; assumption. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. subst. apply CTcol_trivial_2. subst. do 2 (rewrite andb_true_iff in Hmem). destruct Hmem as [[Hmem1' Hmem2'] Hmem3']. assert (Hmem2 : S.mem p2 x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. elim (Pos.eq_dec pa p1); intro Hpap1. subst; rewrite HB; apply CTcol_trivial_1. assert (Hmem1 : S.mem p1 x = true). rewrite <- HEq in Hmem1'. rewrite SWP.Dec.F.add_neq_b in Hmem1'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem1'; assumption. elim (Pos.eq_dec pa p3); intro Hpap3. subst; rewrite HB; apply CTcol_trivial_2. assert (Hmem3 : S.mem p3 x = true). rewrite <- HEq in Hmem3'. rewrite SWP.Dec.F.add_neq_b in Hmem3'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem3'; assumption. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. subst. do 2 (rewrite andb_true_iff in Hmem). destruct Hmem as [[Hmem1' Hmem2'] Hmem3']. assert (Hmem3 : S.mem p3 x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. elim (Pos.eq_dec pa p1); intro Hpap1. subst; rewrite HB; apply CTcol_permutation_4; apply CTcol_trivial_2. assert (Hmem1 : S.mem p1 x = true). rewrite <- HEq in Hmem1'. rewrite SWP.Dec.F.add_neq_b in Hmem1'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem1'; assumption. elim (Pos.eq_dec pa p2); intro Hpap2. subst; rewrite HB; apply CTcol_trivial_2. assert (Hmem2 : S.mem p2 x = true). rewrite <- HEq in Hmem2'. rewrite SWP.Dec.F.add_neq_b in Hmem2'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem2'; assumption. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. do 2 (rewrite andb_true_iff in Hmem). destruct Hmem as [[Hmem1' Hmem2'] Hmem3']. elim (Pos.eq_dec pa p1); intro Hpap1; elim (Pos.eq_dec pa p2); intro Hpap2; elim (Pos.eq_dec pa p3); intro Hpap3. subst; apply CTcol_trivial_1. subst; apply CTcol_trivial_1. subst; apply CTcol_permutation_4; apply CTcol_trivial_2. subst. assert (Hmem1 : S.mem pb x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. assert (Hmem2 : S.mem p2 x = true). rewrite <- HEq in Hmem2'. rewrite SWP.Dec.F.add_neq_b in Hmem2'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem2'; assumption. assert (Hmem3 : S.mem p3 x = true). rewrite <- HEq in Hmem3'. rewrite SWP.Dec.F.add_neq_b in Hmem3'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem3'; assumption. rewrite <- HB. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. subst; apply CTcol_trivial_2. subst. assert (Hmem2 : S.mem pb x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. assert (Hmem1 : S.mem p1 x = true). rewrite <- HEq in Hmem1'. rewrite SWP.Dec.F.add_neq_b in Hmem1'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem1'; assumption. assert (Hmem3 : S.mem p3 x = true). rewrite <- HEq in Hmem3'. rewrite SWP.Dec.F.add_neq_b in Hmem3'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem3'; assumption. rewrite <- HB. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. subst. assert (Hmem3 : S.mem pb x = true). unfold partition in HIn. apply SS.partition_spec1 in HIn; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_2 in HIn; try assumption; apply proper_4. assert (Hmem1 : S.mem p1 x = true). rewrite <- HEq in Hmem1'. rewrite SWP.Dec.F.add_neq_b in Hmem1'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem1'; assumption. assert (Hmem2 : S.mem p2 x = true). rewrite <- HEq in Hmem2'. rewrite SWP.Dec.F.add_neq_b in Hmem2'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem2'; assumption. rewrite <- HB. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. assert (Hmem1 : S.mem p1 x = true). rewrite <- HEq in Hmem1'. rewrite SWP.Dec.F.add_neq_b in Hmem1'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem1'; assumption. assert (Hmem2 : S.mem p2 x = true). rewrite <- HEq in Hmem2'. rewrite SWP.Dec.F.add_neq_b in Hmem2'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem2'; assumption. assert (Hmem3 : S.mem p3 x = true). rewrite <- HEq in Hmem3'. rewrite SWP.Dec.F.add_neq_b in Hmem3'; try assumption. rewrite SWP.Dec.F.remove_neq_b in Hmem3'; assumption. unfold ss_ok in HSSF. apply HSSF with x. apply SSWEqP.MP.Dec.F.mem_1; assumption. do 2 (rewrite andb_true_iff); repeat split; assumption. unfold ss_ok in HSSa. apply HSSa with s'; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. clear HSSF; assert (HSSF := HSSF'); clear HSSF'. unfold ss_ok in HSSF. apply HSSF with s; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. assert (HSSS : ss_ok (snd_ss (partition_ss pb ss)) interp). clear Hmem; clear p1; clear p2; clear p3. intros s' Hs'. intros. apply SSWEqP.MP.Dec.F.mem_2 in Hs'. unfold partition in Hs'. apply SS.partition_spec2 in Hs'; try apply proper_4. apply SSWEqP.MP.Dec.F.filter_1 in Hs'; try apply proper_5. unfold ss_ok in HSS. apply HSS with s'; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. unfold ss_ok in HSSS. apply HSSS with s; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. Qed.
imports: Recdef NArith GeoCoq.Utils.sets