proposition: Lemma prop_mult_step: forall a b res k k', (map interp_carry (mult_step a b res k k')) = RAWBITVECTOR_LIST.mult_bool_step (map (Lit.interp rho) a) (map (Lit.interp rho) b) (map interp_carry res) k k'.
proof: Proof. intros. revert a b res k. assert (false = (Lit.interp rho (Lit._false))) as Ha. { specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H. rewrite not_true_iff_false in H. now rewrite H. } assert (false = interp_carry (Clit Lit._false)). { unfold interp_carry. specialize (Lit.interp_false rho wf_rho). intros. unfold is_true in H. rewrite not_true_iff_false in H. now rewrite H. } assert ([] = map (interp_carry) []). { now simpl. } induction k' as [ | xk' xsk' IHk' ]. - intros. case a. simpl. rewrite H; apply prop_mult_step_k_h. intros. simpl. rewrite H. rewrite prop_mult_step_k_h. simpl. now rewrite map_nth. - intros. simpl. rewrite xsk', prop_mult_step_k_h, prop_and_with_bit. rewrite <- map_nth, <- Ha, <- H. case a. now simpl. simpl. intros. case l. now simpl. simpl. intros. case xk'. now simpl. intros. now rewrite map_firstn. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance