proposition: Lemma prop_check_neg: forall bs bsres n, (N.of_nat(length bs) = n)%N -> (N.of_nat(length bsres) = n)%N -> check_neg bs bsres = true -> RAWBITVECTOR_LIST.bv_neg (map (Lit.interp rho) bs) = map (Lit.interp rho) bsres.
proof: Proof. intros. unfold check_neg in H1. specialize (@check_add_list (map (fun l : int => Lit.neg l) bs) (map (fun _ : int => Lit._false) bs) bsres (Clit Lit._true)). intros. simpl in H2. cut ( Datatypes.length (map (fun l : int => Lit.neg l) bs) = Datatypes.length bsres ). intros. cut (Datatypes.length (map (fun _ : int => Lit._false) bs) = Datatypes.length bsres). intros. specialize (H2 H3 H4 H1). unfold BITVECTOR_LIST.bv_neg, RAWBITVECTOR_LIST.bv_neg. unfold RAWBITVECTOR_LIST.twos_complement. rewrite !map_map in H2. rewrite !map_map. rewrite mk_list_false_eq in H2. rewrite <- map_interp_neg in H2. rewrite Lit.interp_true in H2. rewrite <- H2. now rewrite map_length. easy. rewrite map_length. apply (f_equal (N.to_nat)) in H. apply (f_equal (N.to_nat)) in H0. rewrite Nat2N.id in H, H0. now rewrite H, H0. rewrite map_length. apply (f_equal (N.to_nat)) in H. apply (f_equal (N.to_nat)) in H0. rewrite Nat2N.id in H, H0. now rewrite H, H0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance