proposition: Lemma MM_plus_corr_R : forall (e f:expr) (x y:R), II e x -> II f y -> II (MM_plus e f) (x[+]y).
proof: Proof. cut (forall (i j:Z) (x y:R), II (expr_int i) x -> II (expr_int j) y -> II (expr_int (i + j)) (x[+]y)). cut (forall (e f:expr) (x y:R), II e x -> II f y -> II (expr_plus e f) (x[+]y)). intros H H0 e; elim e. simpl in |- *; auto. intros z f; elim f; simpl in |- *; auto. simpl in |- *; auto. intros e1 H1 e2 H2. elim e1; simpl in |- *; auto. intros n f. elim f; simpl in |- *; auto. intros f1 H3 f2 H4. elim f1; simpl in |- *; auto. intro m. cut (eq_nat n m = true -> n = m). elim (eq_nat n m); simpl in |- *; auto. intros. inversion X. try (rewrite H6 in X1; rewrite H8 in X2; rewrite H7 in H9). inversion X0. try (rewrite H10 in X3; rewrite H12 in X4; rewrite H11 in H13). apply interpR_wd with ((y0[+]y1)[*]x0). apply MV_mult_corr_R; auto. astepl (x0[*](y0[+]y1)). astepl (x0[*]y0[+]x0[*]y1). cut (x0[=]x1). intro. Step_final (x0[*]y0[+]x1[*]y1). apply refl_interpR with val unop binop pfun (expr_var n). assumption. rewrite (H5 (refl_equal true)). assumption. intros; apply eq_nat_corr; auto. intros u e0 H3 f. elim f; simpl in |- *; auto. intros e3 H4 e4 H5. elim e3; simpl in |- *; auto. intros u0 e5 H6. cut (andb (eq_nat u u0) (eq_expr e0 e5) = true -> u = u0). cut (andb (eq_nat u u0) (eq_expr e0 e5) = true -> e0 = e5). elim andb; simpl in |- *; auto. intros H' H''. intros. inversion X. try (rewrite -> H7 in X1; rewrite H9 in X2; rewrite H8 in H10). inversion X0. try (rewrite H11 in X3; rewrite H13 in X4; rewrite H12 in H14). apply interpR_wd with ((y0[+]y1)[*]x0). apply MV_mult_corr_R; auto. astepr (x0[*]y0[+]x1[*]y1). astepl (y0[*]x0[+]y1[*]x0). apply bin_op_wd_unfolded. algebra. astepr (y1[*]x1). apply mult_wdr. apply refl_interpR with val unop binop pfun (expr_unop u e0). auto. rewrite H'. rewrite H''. auto. auto. auto. intro. elim (andb_prop _ _ H7); intros. apply eq_expr_corr; auto. intro. elim (andb_prop _ _ H7); intros. apply eq_nat_corr; auto. intros u e0 H3 e3 H4 f. elim f; simpl in |- *; auto. intros e4 H5 e5 H6. elim e4; simpl in |- *; auto. intros u0 e6 H7 e7 H8. cut (andb (eq_nat u u0) (andb (eq_expr e0 e6) (eq_expr e3 e7)) = true -> u = u0). cut (andb (eq_nat u u0) (andb (eq_expr e0 e6) (eq_expr e3 e7)) = true -> e0 = e6). cut (andb (eq_nat u u0) (andb (eq_expr e0 e6) (eq_expr e3 e7)) = true -> e3 = e7). elim andb; simpl in |- *; auto. intros H' H'' H'''. intros. inversion X. try (rewrite H9 in X1; rewrite H11 in X2; rewrite H10 in H12). inversion X0. try (rewrite H13 in X3; rewrite H15 in X4; rewrite H14 in H16). apply interpR_wd with ((y0[+]y1)[*]x0). apply MV_mult_corr_R; auto. astepr (x0[*]y0[+]x1[*]y1). astepl (y0[*]x0[+]y1[*]x0). apply bin_op_wd_unfolded. algebra. astepr (y1[*]x1). apply mult_wdr. apply refl_interpR with val unop binop pfun (expr_binop u e0 e3). auto. rewrite H'. rewrite H''. rewrite H'''. auto. auto. auto. auto. intro. elim (andb_prop _ _ H9); intros. elim (andb_prop _ _ H11); intros. apply eq_expr_corr; auto. intro. elim (andb_prop _ _ H9); intros. elim (andb_prop _ _ H11); intros. apply eq_expr_corr; auto. intro. elim (andb_prop _ _ H9); intros. apply eq_nat_corr; auto. intros f e0 H3. intro f0. elim f0; simpl in |- *; auto. intros e3 H4 e4 H5. elim e3; simpl in |- *; auto. intros f1 e5 H6. cut (andb (eq_nat f f1) (eq_expr e0 e5) = true -> f = f1). cut (andb (eq_nat f f1) (eq_expr e0 e5) = true -> e0 = e5). elim (andb (eq_nat f f1) (eq_expr e0 e5)); simpl in |- *; auto. intros. inversion X. try (rewrite H9 in X1; rewrite H11 in X2; rewrite H10 in H12). inversion X0. try (rewrite H13 in X3; rewrite H15 in X4; rewrite H14 in H16). apply interpR_wd with ((y0[+]y1)[*]x0). apply MV_mult_corr_R; auto. astepr (x0[*]y0[+]x1[*]y1). astepl (y0[*]x0[+]y1[*]x0). apply bin_op_wd_unfolded. algebra. astepr (y1[*]x1). apply mult_wdr. apply refl_interpR with val unop binop pfun (expr_part f e0). auto. rewrite H7. rewrite H8; auto. auto. intro. elim (andb_prop _ _ H7); intros. apply eq_expr_corr; auto. intro. elim (andb_prop _ _ H7); intros. apply eq_nat_corr; auto. simpl in |- *; auto. intros u e0 H1 f. elim f; simpl in |- *; auto. intros u e0 H1 e1 H2 f. elim f; simpl in |- *; auto. intros u e0 H1 f. elim f; simpl in |- *; auto. intros; apply interpR_plus with x y; algebra. intros. inversion X. try (rewrite H1 in H0; rewrite H in H0). inversion X0. try (rewrite H2 in H3; rewrite H4 in H3). apply interpR_wd with (zring (i + j):R). apply interpR_int; algebra. Step_final (zring i[+]zring j:R). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection