proposition: Theorem split_expr_correct : forall d vars vars' e lp lc, (forall n, eval (nth n lc d) vars = eval (nth n lc d) vars') -> match split_expr e lp lc with | Sconst => eval e vars = eval e vars' | Scomposed lp' lc' => forall n, eval (nth n lc' d) vars = eval (nth n lc' d) vars' end.
proof: Proof. intros d vars vars'. induction e as [n|o|o e1 IHe1|o e1 IHe1 e2 IHe2] ; intros lp lc Hc ; simpl ; try easy. specialize (IHe1 lp lc Hc). destruct split_expr as [|lp' lc']. now apply f_equal. apply IHe1. specialize (IHe2 lp lc Hc). destruct split_expr as [|lp2 lc2]. specialize (IHe1 lp lc Hc). destruct split_expr as [|lp1 lc1]. now apply f_equal2. now apply eval_nth_rcons_unique. specialize (IHe1 lp2 lc2 IHe2). destruct split_expr as [|lp1 lc1]. now apply eval_nth_rcons_unique. apply IHe1. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree