proposition: Lemma is_const_correct : forall e n, is_const e n = true -> forall l x1 x2, interp (set_nth 0 l n x1) e = interp (set_nth 0 l n x2) e.
proof: Proof. induction e using expr_ind'. simpl => k Hk l x1 x2. rewrite 2!nth_set_nth /=. now rewrite -ssrnat.eqnE (ssrbool.negbTE Hk). simpl => n Hc l x1 x2. apply apply_ext. intros m _. revert m. induction le. intros m. now rewrite nth_nil. apply andb_prop in Hc. intros [|m]. simpl. now apply H. simpl. apply IHle. apply H. apply Hc. easy. simpl => n. move /ssrbool.andP => [H1 H2] l x1 x2. rewrite (IHe2 n H2 l x1 x2). now apply: (IHe1 (S n) _ (interp (set_nth 0 l n x2) e2 :: l)). intros n. simpl is_const. move /ssrbool.andP => [H1 H2] l x1 x2. change (interp (set_nth 0 (set_nth 0 l n x1) 0 (interp (set_nth 0 l n x1) e2)) e1 = interp (set_nth 0 (set_nth 0 l n x2) 0 (interp (set_nth 0 l n x2) e2)) e1). move: H1. replace (orb (ssrnat.eqn n 0) (is_const e1 n)) with (orb (ssrnat.eqn n 0) (andb (negb (ssrnat.eqn n 0)) (is_const e1 n))). move /ssrbool.orP => [H1|]. rewrite set_set_nth (set_set_nth 0 l n x2). rewrite -ssrnat.eqnE H1. now rewrite (IHe2 n H2 l x1 x2). move /ssrbool.andP => [H1 H3]. rewrite set_set_nth (set_set_nth 0 l n x2). rewrite -ssrnat.eqnE (ssrbool.negbTE H1). rewrite (IHe2 n H2 l x1 x2). now apply IHe1. now case (ssrnat.eqn n 0). easy. simpl => n. move /ssrbool.andP => [H1 H2] l x1 x2. now rewrite (IHe1 n H1 l x1 x2) (IHe2 n H2 l x1 x2). simpl => n H l x1 x2. now rewrite (IHe n H l x1 x2). simpl => n. move /ssrbool.andP => [H1]. move /ssrbool.andP => [H2 H3] l x1 x2. rewrite (IHe2 n H2 l x1 x2) (IHe3 n H3 l x1 x2). apply RInt_ext => x _. apply (IHe1 _ H1 (x :: l)). Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct