proposition: Lemma check_add_list:forall bs1 bs2 bsres c, let n := length bsres in (length bs1 = n)%nat -> (length bs2 = n)%nat -> check_add bs1 bs2 bsres c -> (RAWBITVECTOR_LIST.add_list_ingr (map (Lit.interp rho) bs1) (map (Lit.interp rho) bs2) (interp_carry c)) = (map (Lit.interp rho) bsres).
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1]. - intros. simpl in H1. case_eq bs2. intros. rewrite H2 in H1. simpl. case_eq bsres. intros. rewrite H3 in H1. now simpl. intros. rewrite H3 in H1. now contradict H1. intros. rewrite H2 in H1. now contradict H1. - intros. case_eq bs2. intros. rewrite H2 in H1. simpl in H1. now contradict H1. intros. rewrite H2 in H1. case_eq bsres. intros. rewrite H3 in H1. simpl in H1. now contradict H1. intros. rewrite H3 in H1. simpl in H1. case_eq ( Lit.is_pos i0). intros. rewrite H4 in H1. case_eq ( t_form .[ Lit.blit i0]); intros; rewrite H5 in H1; try now contradict H. case_eq ( Lit.is_pos i1). intros. rewrite H6 in H1. case_eq ( t_form .[ Lit.blit i1]); intros; rewrite H7 in H1; try now contradict H. unfold is_true in H1. rewrite andb_true_iff in H1. destruct H1. unfold n in *. rewrite H3 in H. rewrite H2, H3 in H0. inversion H. inversion H0. specialize (@IHbs1 l l0 ((Cor (Cand (Clit xbs1) (Clit i)) (Cand (Cxor (Clit xbs1) (Clit i)) c))) H10 H11 H8). simpl in *. unfold RAWBITVECTOR_LIST.of_bits in IHbs1. case_eq (RAWBITVECTOR_LIST.add_carry (Lit.interp rho xbs1) (Lit.interp rho i) (interp_carry c)). intros r c0 Heqrc. pose proof (rho_interp (Lit.blit i0)). rewrite H5 in H9. simpl in H9. pose proof (rho_interp (Lit.blit i1)). rewrite H7 in H12. simpl in H12. unfold Lit.interp at 3. rewrite H4. unfold Var.interp. rewrite H9. rewrite <- IHbs1. simpl. cut (r = xorb (Lit.interp rho i1) (Lit.interp rho i2)). cut (c0 = (Lit.interp rho xbs1 && Lit.interp rho i || xorb (Lit.interp rho xbs1) (Lit.interp rho i) && interp_carry c)). intros. now rewrite H13, H14. case ((Lit.interp rho xbs1)) in *. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. easy. inversion Heqrc. easy. case ((interp_carry c)) in *. inversion Heqrc. easy. inversion Heqrc. easy. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. easy. inversion Heqrc. easy. case ((interp_carry c)) in *. inversion Heqrc. easy. inversion Heqrc. easy. rewrite andb_true_iff in H1. destruct H1. rewrite orb_true_iff in H1. destruct H1; rewrite andb_true_iff in H1; destruct H1. rewrite eqb_spec in H1, H14. rewrite H1, H14 in *. apply prop_eq_carry_lit in H13. rewrite <- H13. case ((Lit.interp rho xbs1)) in *. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. rewrite eqb_spec in H1, H14. rewrite H1, H14 in *. apply prop_eq_carry_lit in H13. rewrite <- H13. case ((Lit.interp rho xbs1)) in *. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((Lit.interp rho i)) in *. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. case ((interp_carry c)) in *. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. inversion Heqrc. unfold Lit.interp, Var.interp. rewrite H6, H12. easy. intros. rewrite H6 in H1. now contradict H1. intros. rewrite H4 in H1. now contradict H1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance