proposition: Theorem decompose_correct : forall vars p lp lc, (forall vars n, eval (nth n lc (Econst (Int 0))) vars = eval (nth n lc (Econst (Int 0))) nil) -> let lc' := map (fun c => eval c nil) lc in match decompose (length vars) p lp lc with | None => True | Some lp' => eval_real lp' (vars ++ lc') = eval_real p ((map (fun c => eval c (vars ++ lc')) lp) ++ (vars ++ lc')) end.
proof: Proof. intros vars p lp lc Hc lc'. revert p. induction lp as [|h t IH]. easy. intros p. simpl. assert (H: forall n e, nth n (t ++ map Evar (seq 0 (length vars)) ++ lc) (Econst (Int 0)) = e -> nth n (map (fun c : expr => eval c (vars ++ lc')) t ++ vars ++ lc') 0%R = eval e (vars ++ lc')). intros n e. destruct (Nat.lt_ge_cases n (length t)) as [H1|H1]. rewrite app_nth1 by apply H1. intros H. rewrite app_nth1 by now rewrite map_length. change 0%R with ((fun c => eval c (vars ++ lc')) (Econst (Int 0))). rewrite map_nth. now rewrite H. rewrite app_nth2 by apply H1. rewrite (@app_nth2 _ _ _ _ n) ; rewrite map_length. 2: exact H1. destruct (Nat.lt_ge_cases (n - length t) (length vars)) as [H2|H2]. rewrite app_nth1 by now rewrite map_length, seq_length. rewrite app_nth1 by apply H2. rewrite nth_indep with (d' := Evar 0) by now rewrite map_length, seq_length. rewrite map_nth, seq_nth, Nat.add_0_l by apply H2. intros <-. simpl. now rewrite app_nth1 by apply H2. rewrite app_nth2 ; rewrite map_length, seq_length. 2: exact H2. rewrite app_nth2 by apply H2. intros H. unfold lc'. change 0%R with ((fun c => eval c nil) (Econst (Int 0))). rewrite map_nth, H. rewrite <- H at 2. now rewrite Hc, H. destruct find_expr eqn:H0. { generalize (find_expr_correct h (length vars) t lc). rewrite H0. specialize (IH (Forward n :: p)). destruct decompose; [| easy]. rewrite IH. intros H1. apply H in H1. rewrite <-H1. unfold eval_real. simpl. now unfold eval_generic_body. } clear H0. destruct h as [n|o|o e1|o e1 e2] ; try easy. - specialize (IH (Forward (length t + n) :: p)). destruct decompose ; try easy. rewrite IH. simpl. unfold eval_generic_body. rewrite app_nth2 ; rewrite map_length. apply (f_equal (fun v => eval_real p (nth v _ _ :: _))). lia. lia. - generalize (find_expr_correct e1 (length vars) t lc). destruct find_expr as [n1|] ; try easy. intros H1. specialize (IH (Unary o n1 :: p)). destruct decompose ; try easy. rewrite IH. simpl. unfold eval_generic_body. apply (f_equal (fun v => eval_real p (unary_real o v :: _))). now apply H. - generalize (find_expr_correct e1 (length vars) t lc). destruct find_expr as [n1|] ; try easy. intros H1. generalize (find_expr_correct e2 (length vars) t lc). destruct find_expr as [n2|] ; try easy. intros H2. specialize (IH (Binary o n1 n2 :: p)). destruct decompose ; try easy. rewrite IH. simpl. unfold eval_generic_body. apply (f_equal2 (fun v1 v2 => eval_real p (binary_real o v1 v2 :: _))). now apply H. now apply H. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree