我对 svg 语法非常陌生，我想知道如何将一条路径分成两条路径。实际上我有这样的东西：
M Xm Ym ... C Xc1 Yc1 Xc2 Yc2 Xc3 Yc3 (*) C Xd1 Yd1 Xd2 Yd2 Xd3 Yd3 C ...
(*) 是我要分割路径的地方
我想将其转换为两个路径，如下所示：
M Am Bm ... C Ac1 Bc1 Ac2 Bc2 Ac3 Bc3
和
M An Bn C Ad1 Bd1 Ad2 Bd2 Ad3 Bd3 ...
如何通过X和Y数字计算A和B数字？
我正在尝试为Coq 中的所有命题定义双重否定翻译，因此我可以证明在“直觉逻辑”中无法证明（或有非常硬的证明）的经典事实，但我认为这不可能使用Inductive或Fixpoint关键词。有Fixpoint，我需要匹配arbitary命题。（虽然我只需要一阶逻辑，即合取、析取、条件、否定forall和exists量词）我也不能使用Inductive. 这是我失败的方法
Inductive NN (P : Prop) : Prop :=
| nn_cond (P1 P2 : Prop) (Heq : P = P1 /\ P2) (H : NN P1 -> NN P2).
我最后需要证明一个Lemma类似的
Lemma NN__EM (P : Prop) : NN P <-> (excluded_middle -> P).
关于如何定义这样的定义的任何想法？