proposition: Lemma xexprF2interpF : forall (x:F) (e:xexprF x), interpF (xforgetF _ e) x.
proof: Proof. intros x e. induction e. apply (interpF_var i); algebra. apply (interpF_int k); algebra. apply (interpF_plus (xforgetF _ e1) (xforgetF _ e2) x y (x[+]y)); algebra. apply (interpF_mult (xforgetF _ e1) (xforgetF _ e2) x y (x[*]y)); algebra. apply (interpF_unop (xforgetF _ e) f x (unop f x)); algebra. apply (interpF_binop (xforgetF _ e1) (xforgetF _ e2) f x y (binop f x y)); algebra. eapply (interpF_part (xforgetF _ e) f x (pfun f x Hx)). apply eq_reflexive_unfolded. algebra. apply (interpF_div (xforgetF _ e1) (xforgetF _ e2) x y (x[/]y[//]nzy) nzy); algebra. apply (interpF_int 0); algebra. apply (interpF_int 1); Step_final ([1]:F). apply (interpF_int (Z_of_nat n)); algebra. apply (interpF_mult (xforgetF _ e) (expr_int (-1)) x (zring (-1)) [--]x); auto. Step_final (zring (-1)[*]x). apply (interpF_int (-1)); algebra. apply (interpF_plus (xforgetF _ e1) (xforgetF _ (xexprF_inv _ e2)) x [--]y (x[-]y)); algebra. apply (interpF_mult (xforgetF _ e2) (expr_int (-1)) y (zring (-1)) [--]y); auto. Step_final (zring (-1)[*]y). apply (interpF_int (-1)); algebra. induction n. apply (interpF_int 1); Step_final ([1]:F). apply (interpF_mult (xforgetF _ e) (expr_power n (xforgetF _ e)) x ( x[^]n) (x[^]S n)); algebra. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection