proposition: Theorem extract_list_correct : forall le vars, match extract_list le (length vars) with | Eabort => True | Eprog lp lc => forall k, k < length le -> eval_real_nth k lp vars lc = eval (nth k le (Econst (Int 0))) vars end.
proof: Proof. intros le vars. unfold extract_list. destruct max_arity_list eqn:Ha ; [ |exact I]. destruct fold_split as (lp, lc) eqn:Hf. generalize (decompose_correct vars nil (le ++ lp) lc). destruct decompose as [lp'|] ; [ |easy]. assert ((forall (vars0 : list R) (n : nat), eval (nth n lc (Econst (Int 0))) vars0 = eval (nth n lc (Econst (Int 0))) nil) /\ forall k : nat, k < length le -> nth k (eval_real nil (map (fun c : expr => eval c (vars ++ map (fun c0 : expr => eval c0 nil) lc)) (le ++ lp) ++ vars ++ map (fun c : expr => eval c nil) lc)) 0%R = eval (nth k le (Econst (Int 0))) vars) as [H1 H2]. 2: { intros H. apply H in H1. unfold eval_real_nth. now rewrite H1. } revert lp lc Hf lp'. induction le ; intros lp lc. { intros [= <- <-]. split ; [ |easy]. now intros vars0 [|n]. } simpl fold_split. simpl in Ha. apply andb_prop in Ha. destruct Ha as [Ha1 Ha2]. destruct fold_split as (lp0, lc0) eqn:Hf'. intros Hf lp'. destruct (IHle Ha2 lp0 lc0 eq_refl lp') as [IH1 _]. clear IHle. generalize (fun v => split_expr_correct (Econst (Int 0)) v nil a lp0 lc0). intros Hs. destruct split_expr as [|lp1 lc1] ; injection Hf as <- <- ; split. - intros vars0 n. apply eval_nth_rcons_unique. now apply Hs. easy. - intros [|k] Hk ; simpl. { now apply max_arity_correct. } destruct (rcons_unique_correct a lc0) as [l' ->]. simpl in Hk. rewrite <-Nat.succ_lt_mono in Hk. rewrite app_nth1. 2: { rewrite map_length, app_length. lia. } rewrite map_nth with (d := Econst (Int 0)). rewrite app_nth1 by easy. apply max_arity_correct. now apply max_arity_nth. - intros vars0. now apply Hs. - intros [|k] Hk ; simpl. { now apply max_arity_correct. } simpl in Hk. rewrite <-Nat.succ_lt_mono in Hk. rewrite app_nth1. 2: { rewrite map_length, app_length. lia. } rewrite map_nth with (d := Econst (Int 0)). rewrite app_nth1 by easy. apply max_arity_correct. now apply max_arity_nth. Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree