proposition: Lemma MI_mult_corr_R : forall (e f:expr) (x y:R), II e x -> II f y -> II (MI_mult e f) (x[*]y).
proof: Proof. cut (forall x y:R, II (expr_int 0) y -> II (expr_int 0) (x[*]y)). cut (forall (e1 e2 f:expr) (x y:R), (forall (f:expr) (x y:R), II e2 x -> II f y -> II (MI_mult e2 f) (x[*]y)) -> II (expr_mult e1 e2) x -> II f y -> II (expr_mult e1 (MI_mult e2 f)) (x[*]y)). 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_mult e f) (x[*]y)). simple induction e; simple induction f; simpl in |- *; auto. simple induction z; simpl in |- *; auto. simple induction z0; induction z; simpl in |- *; auto. simple induction z; simpl in |- *; auto. simple induction z; simpl in |- *; auto. induction f; simpl in |- *; auto. simple induction z; simpl in |- *; auto. simple induction z0; simpl in |- *; auto. simple induction z; simpl in |- *; auto. simple induction z; simpl in |- *; auto. simple induction z; simpl in |- *; auto. intros; apply interpR_mult with x y; algebra. intros; apply interpR_wd with (zring (i * j):R). apply interpR_int; algebra. inversion X. inversion X0. Step_final (zring i[*]zring j:R). intros. inversion X0. try (rewrite H in X2; rewrite H1 in X3; rewrite H0 in H2). apply interpR_wd with (x0[*](y0[*]y)); algebra. apply interpR_mult with x0 (y0[*]y); algebra. Step_final (x0[*]y0[*]y). intros. inversion X. try (rewrite H in H0; rewrite H1 in H0). apply interpR_wd with (zring 0:R). apply interpR_int; algebra. astepl ([0]:R). astepl (x[*][0]). Step_final (x[*]zring 0). Qed.
imports: CoRN.algebra.CRings CoRN.tactics.AlgReflection