proposition: Theorem eval_inductive_prop_floor_fun : forall {T} A B P (opsA : operations A) (opsB : operations B), (forall a1 a2, (forall x : T, a1 x = a2 x) -> forall b, P a1 b -> P a2 b) -> (forall o a b, no_floor_op o = true -> P a b -> P (fun x => unary opsA o (a x)) (unary opsB o b)) -> (forall o a1 a2 b1 b2, P a1 b1 -> P a2 b2 -> P (fun x => binary opsA o (a1 x) (a2 x)) (binary opsB o b1 b2)) -> forall inpA inpB, (forall n, P (fun x => nth n (inpA x) (unknown opsA)) (nth n inpB (unknown opsB))) -> forall prog, no_floor_prog prog = true -> forall n, P (fun x => nth n (eval_generic opsA prog (inpA x)) (unknown opsA)) (nth n (eval_generic opsB prog inpB) (unknown opsB)).
proof: Proof. intros T A B P opsA opsB HP Hun Hbin inpA inpB Hinp prog Hprog n. apply HP with (fun x => nth n (fold_right (fun y x => eval_generic_body opsA x y) (inpA x) (rev prog)) (unknown opsA)). intros x. now rewrite rev_formula. rewrite rev_formula. generalize n. clear n. revert Hprog; rewrite -no_floor_prog_rev. induction (rev prog). intros _. exact Hinp. rewrite no_floor_prog_cons. intros H1. assert (H2 : no_floor_term a = true). now revert H1; case no_floor_term. assert (H3 : no_floor_prog l = true). now revert H1; case no_floor_term; try discriminate. intros [|n]. 2: now apply IHl. now destruct a as [n|o n|o n1 n2] ; [ idtac | apply Hun | apply Hbin ] ; try apply IHl. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog