proposition: Lemma xexprR2interpR : forall (x:R) (e:xexprR x), interpR (xforgetR _ e) x.
proof: Proof. intros x e. induction e. apply (interpR_var i); algebra. apply (interpR_int k); algebra. apply (interpR_plus (xforgetR _ e1) (xforgetR _ e2) x y (x[+]y)); algebra. apply (interpR_mult (xforgetR _ e1) (xforgetR _ e2) x y (x[*]y)); algebra. apply (interpR_unop (xforgetR _ e) f x (unop f x)); algebra. apply (interpR_binop (xforgetR _ e1) (xforgetR _ e2) f x y (binop f x y)); algebra. eapply (interpR_part (xforgetR _ e) f x (pfun f x Hx)). apply eq_reflexive_unfolded. algebra. apply (interpR_int 0); algebra. apply (interpR_int 1); Step_final ([1]:R). apply (interpR_int (Z_of_nat n)); algebra. apply (interpR_mult (xforgetR _ e) (expr_int (-1)) x (zring (-1)) [--]x); auto. Step_final (zring (-1)[*]x). apply (interpR_int (-1)); algebra. apply (interpR_plus (xforgetR _ e1) (xforgetR _ (xexprR_inv _ e2)) x [--]y (x[-]y)); algebra. apply (interpR_mult (xforgetR _ e2) (expr_int (-1)) y (zring (-1)) [--]y); auto. Step_final (zring (-1)[*]y). apply (interpR_int (-1)); algebra. induction n. apply (interpR_int 1); Step_final ([1]:R). apply (interpR_mult (xforgetR _ e) (expr_power n (xforgetR _ e)) x ( x[^]n) (x[^]S n)); algebra. Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection