proposition: Lemma CPToSSOKAux {m m' : nat} : forall (cp : cartesianPower positive (S (S m))) (cp' : cartesianPower positive (S (S m'))) e s, S.Equal (CPToSS cp) s -> memCPAux m' cp' s = true -> InCP e cp' -> InCP e cp.
proof: Proof. induction m'. induction m; intros cp cp' e s HEq Hmem HIn. unfold InCP in *. simpl in *. apply andb_true_iff in Hmem. destruct Hmem as [Hmem1 Hmem2]. assert (HmemEq : S.mem (fst cp') (S.add (fst cp) (S.add (snd cp) S.empty)) = S.mem (fst cp') s) by (apply SWP.FM.mem_m; trivial); simpl in *;rewrite <- HmemEq in Hmem1; clear HmemEq. assert (HmemEq : S.mem (snd cp') (S.add (fst cp) (S.add (snd cp) S.empty)) = S.mem (snd cp') s) by (apply SWP.FM.mem_m; trivial); simpl in *;rewrite <- HmemEq in Hmem2; clear HmemEq; clear HEq. rewrite SWP.Dec.F.add_b in Hmem1. rewrite <- SWP.Dec.F.singleton_b in Hmem1. assert (HmemEq : S.mem (fst cp') (S.add (snd cp) S.empty) = S.mem (fst cp') (S.singleton (snd cp))) by (apply SWP.FM.mem_m; trivial; apply SWP.singleton_equal_add); simpl in *;rewrite HmemEq in Hmem1; clear HmemEq. rewrite SWP.Dec.F.add_b in Hmem2. rewrite <- SWP.Dec.F.singleton_b in Hmem2. assert (HmemEq : S.mem (snd cp') (S.add (snd cp) S.empty) = S.mem (snd cp') (S.singleton (snd cp))) by (apply SWP.FM.mem_m; trivial; apply SWP.singleton_equal_add); simpl in *;rewrite HmemEq in Hmem2; clear HmemEq. apply orb_true_iff in Hmem1. apply orb_true_iff in Hmem2. elim HIn; clear HIn; intro HIn. subst. elim Hmem1; clear Hmem1; clear Hmem2; intro HEq; apply SWP.Dec.F.mem_2 in HEq; apply SWP.Dec.F.singleton_1 in HEq; auto. elim HIn; clear HIn; intro HIn. subst. elim Hmem2; clear Hmem1; clear Hmem2; intro HEq; apply SWP.Dec.F.mem_2 in HEq; apply SWP.Dec.F.singleton_1 in HEq; auto. intuition. elim HIn; clear HIn; intro HIn. assert (HmemEq : memCPAux 0 cp' (CPToSS cp) = memCPAux 0 cp' s) by (apply memCPAuxProperOK; trivial); rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm. subst. assert (HIn : InCP (headCP cp') cp') by (unfold InCP; simpl; auto). assert (H := memCPAuxOK 0 cp' (CPToSS cp) (headCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem. apply memCPToSSOK. assumption. unfold InCP in HIn. simpl in HIn. elim HIn; clear HIn; intro HIn. assert (HmemEq : memCPAux 0 cp' (CPToSS cp) = memCPAux 0 cp' s) by (apply memCPAuxProperOK; trivial); rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm. subst. assert (HIn : InCP (tailCP cp') cp') by (unfold InCP; simpl; auto). assert (H := memCPAuxOK 0 cp' (CPToSS cp) (tailCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem. apply memCPToSSOK. assumption. intuition. intros cp cp' e s HEq Hmem HIn. apply InCPOK in HIn. elim HIn; clear HIn; intro HIn. subst. assert (HmemEq : memCPAux (S m') cp' (CPToSS cp) = memCPAux (S m') cp' s) by (apply memCPAuxProperOK; trivial); rewrite <- HmemEq in Hmem; clear HmemEq; clear HEq; clear IHm'. assert (HIn : InCP (headCP cp') cp') by (unfold InCP; simpl; auto). assert (H := memCPAuxOK (S m') cp' (CPToSS cp) (headCP cp') Hmem HIn); clear HIn; clear Hmem; rename H into Hmem. apply memCPToSSOK. assumption. apply IHm' with (tailCP cp') s; try assumption. apply memCPAuxTlOK; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets