proposition: Lemma extract_interp_main: forall bs1 bsres (i n0: N), check_extract bs1 bsres i (n0 + i) = true -> @RAWBITVECTOR_LIST.bv_extr i n0 (N.of_nat (length bs1)) (map (Lit.interp rho) bs1) = map (Lit.interp rho) bsres.
proof: Proof. intro bs1. induction bs1 as [ | xbs1 xsbs1 IHbs1]. - intros. simpl. unfold check_extract in H. simpl in H. unfold RAWBITVECTOR_LIST.bv_extr. case_eq (nat_of_N i). intros. simpl. case_eq (nat_of_N n0). intros. simpl. case_eq ((0 <? n0 + i)%N); intros. rewrite H2 in H. now contradict H. rewrite H2 in H. case_eq bsres. intros. now simpl. intros. rewrite H3 in H. now contradict H. intros. case_eq bsres. intros. apply (f_equal (N.of_nat)) in H1. apply (f_equal (N.of_nat)) in H0. rewrite N2Nat.id in H1, H0. rewrite H1, H0 in H. simpl in H. now contradict H0. intros. rewrite H2 in H. case ((0 <? n0 + i)%N) in H; now contradict H. intros. case_eq (N.to_nat n0). intros. apply (f_equal (N.of_nat)) in H1. apply (f_equal (N.of_nat)) in H0. rewrite N2Nat.id in H1, H0. rewrite H1, H0 in H. simpl in H. now contradict H0. intros. apply (f_equal (N.of_nat)) in H1. apply (f_equal (N.of_nat)) in H0. rewrite N2Nat.id in H1, H0. rewrite H1, H0 in H. simpl in H. now contradict H0. - intros. unfold check_extract in H. case_eq ((N.of_nat (Datatypes.length (xbs1 :: xsbs1)) <? n0 + i)%N). intros. rewrite H0 in H. now contradict H. intros. rewrite H0 in H. case_eq ( forallb2 eq_carry_lit (lit_to_carry (extract_lit (xbs1 :: xsbs1) (N.to_nat i) (N.to_nat (n0 + i)))) bsres); intros. apply prop_eq_carry_lit2 in H1. rewrite prop_interp_carry3 in H1. simpl in H1. simpl. unfold RAWBITVECTOR_LIST.bv_extr in *. simpl in *. case_eq (N.to_nat i); intros; rewrite H2 in H1. case_eq (N.to_nat (n0 + i)); intros; rewrite H3 in H1. rewrite <- H1. rewrite H0. easy. rewrite H0. simpl in H1. rewrite <- H1. simpl. apply f_equal. now rewrite extract_interp_zero. case_eq (N.to_nat (n0 + i)); intros; rewrite H3 in H1. rewrite H0. rewrite <- H1. easy. rewrite H0. now rewrite extract_interp_all. rewrite H1 in H. now contradict H. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance