proposition: Lemma NormR_corr : forall (e:expr) (x:R), II e x -> II (NormR e) x.
proof: Proof. intro; induction e; intros; simpl in |- *. apply (interpR_plus R val unop binop pfun (expr_mult (expr_var v) expr_one) expr_zero x ([0]:R) x). algebra. apply (interpR_mult R val unop binop pfun (expr_var v) expr_one x ([1]:R) x); algebra. apply (interpR_int R val unop binop pfun 1); algebra. apply (interpR_int R val unop binop pfun 0); algebra. assumption. inversion X. try (rewrite H in X0; rewrite H1 in X1; rewrite H0 in H2). apply interpR_wd with (x0[+]y). apply PP_plus_corr_R; auto. auto. inversion X. try (rewrite H in X0; rewrite H1 in X1; rewrite H0 in H2). apply interpR_wd with (x0[*]y). apply PP_mult_corr_R; auto. auto. assumption. inversion X. try (rewrite H in H2; rewrite H1 in X0; rewrite H0 in H2). apply (interpR_plus R val unop binop pfun (expr_mult (expr_unop u (NormR e)) expr_one) expr_zero x ( [0]:R) x). algebra. apply (interpR_mult R val unop binop pfun (expr_unop u (NormR e)) expr_one x ([1]:R) x); algebra. apply (interpR_unop R val unop binop pfun (NormR e) u x0); algebra. apply (interpR_int R val unop binop pfun 1); algebra. apply (interpR_int R val unop binop pfun 0); algebra. inversion X. try (rewrite H in H3; rewrite H1 in X0; rewrite H2 in X1; rewrite H0 in H3). apply (interpR_plus R val unop binop pfun (expr_mult (expr_binop b (NormR e1) (NormR e2)) expr_one) expr_zero x ([0]:R) x). algebra. apply (interpR_mult R val unop binop pfun (expr_binop b (NormR e1) (NormR e2)) expr_one x ([1]:R) x); algebra. apply (interpR_binop R val unop binop pfun (NormR e1) (NormR e2) b x0 y); algebra. apply (interpR_int R val unop binop pfun 1); algebra. apply (interpR_int R val unop binop pfun 0); algebra. inversion X. try ((generalize Hx H2; clear Hx H2; rewrite H; intros Hx H2); rewrite H1 in X0; rewrite H0 in H2). apply (interpR_plus R val unop binop pfun (expr_mult (expr_part p (NormR e)) expr_one) expr_zero x ( [0]:R) x). algebra. apply (interpR_mult R val unop binop pfun (expr_part p (NormR e)) expr_one x ([1]:R) x); algebra. apply (interpR_part R val unop binop pfun (NormR e) p x0) with (Hx := Hx); algebra. apply (interpR_int R val unop binop pfun 1); algebra. apply (interpR_int R val unop binop pfun 0); algebra. Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection