proposition: Lemma NormF_corr : forall (e:expr) (x:F), II e x -> II (NormF e) x.
proof: Proof. intro; elim e; intros; simpl in |- *. apply (interpF_div F val unop binop pfun (expr_plus (expr_mult (expr_var v) expr_one) expr_zero) expr_one x ([1]:F) x (ring_non_triv F)). algebra. apply (interpF_plus F val unop binop pfun (expr_mult (expr_var v) expr_one) expr_zero x ([0]:F) x). algebra. apply (interpF_mult F val unop binop pfun (expr_var v) expr_one x ([1]:F) x); algebra. apply (interpF_int F val unop binop pfun 1); algebra. apply (interpF_int F val unop binop pfun 0); algebra. apply (interpF_int F val unop binop pfun 1); algebra. apply (interpF_div F val unop binop pfun (expr_int z) expr_one x ( [1]:F) x (ring_non_triv F)). algebra. algebra. apply (interpF_int F val unop binop pfun 1); algebra. inversion X1. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpF_wd with (x0[+]y). apply FF_plus_corr_F; auto. auto. inversion X1. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpF_wd with (x0[*]y). apply FF_mult_corr_F; auto. auto. inversion X1. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpF_wd with (x0[/]y[//]nzy). apply FF_div_corr_F; auto. auto. inversion X0. try (rewrite H in H2; rewrite H1 in X1; rewrite H0 in H2). apply (interpF_div F val unop binop pfun (expr_plus (expr_mult (expr_unop u (NormF e0)) expr_one) expr_zero) expr_one x ([1]:F) x (ring_non_triv F)). algebra. apply (interpF_plus F val unop binop pfun (expr_mult (expr_unop u (NormF e0)) expr_one) expr_zero x ( [0]:F) x). algebra. apply (interpF_mult F val unop binop pfun (expr_unop u (NormF e0)) expr_one x ([1]:F) x); algebra. apply (interpF_unop F val unop binop pfun (NormF e0) u x0); algebra. apply (interpF_int F val unop binop pfun 1); algebra. apply (interpF_int F val unop binop pfun 0); algebra. apply (interpF_int F val unop binop pfun 1); algebra. inversion X1. try (rewrite H in H3; rewrite H1 in X2; rewrite H2 in X3; rewrite H0 in H3). apply (interpF_div F val unop binop pfun (expr_plus (expr_mult (expr_binop b (NormF e0) (NormF e1)) expr_one) expr_zero) expr_one x ([1]:F) x (ring_non_triv F)). algebra. apply (interpF_plus F val unop binop pfun (expr_mult (expr_binop b (NormF e0) (NormF e1)) expr_one) expr_zero x ([0]:F) x). algebra. apply (interpF_mult F val unop binop pfun (expr_binop b (NormF e0) (NormF e1)) expr_one x ([1]:F) x); algebra. apply (interpF_binop F val unop binop pfun (NormF e0) (NormF e1) b x0 y); algebra. apply (interpF_int F val unop binop pfun 1); algebra. apply (interpF_int F val unop binop pfun 0); algebra. apply (interpF_int F val unop binop pfun 1); algebra. inversion X0. try ((generalize Hx H2; clear Hx H2; rewrite H; intros Hx H2); rewrite H1 in X1; rewrite H0 in H2). apply (interpF_div F val unop binop pfun (expr_plus (expr_mult (expr_part p (NormF e0)) expr_one) expr_zero) expr_one x ([1]:F) x (ring_non_triv F)). algebra. apply (interpF_plus F val unop binop pfun (expr_mult (expr_part p (NormF e0)) expr_one) expr_zero x ( [0]:F) x). algebra. apply (interpF_mult F val unop binop pfun (expr_part p (NormF e0)) expr_one x ([1]:F) x); algebra. apply (interpF_part F val unop binop pfun (NormF e0) p x0) with (Hx := Hx); algebra. apply (interpF_int F val unop binop pfun 1); algebra. apply (interpF_int F val unop binop pfun 0); algebra. apply (interpF_int F val unop binop pfun 1); algebra. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection