proposition: Lemma length_check_shsl: forall bs1 bs2 bsres , check_shl bs1 bs2 bsres = true -> length bs1 = length bs2 -> length bs1 = length bsres.
proof: Proof. intro bs1. induction bs1; intros. - case_eq bs2; simpl; intros. + subst. unfold check_shl in H. simpl in H. case_eq bsres; simpl; intros; subst; easy. + rewrite H1 in H. unfold check_shl in H. simpl in H. now contradict H. - simpl in *. unfold check_shl in H. simpl in H. case_eq bs2; simpl; intros; subst. simpl in H. now contradict H. simpl in *. inversion H0. rewrite H2, Nat.eqb_refl in H. case_eq (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (a :: bs1) (b :: l))) bsres); intros. + apply prop_eq_carry_lit2 in H1. rewrite prop_interp_carry3 in H1. simpl in H1. assert (length (map (Lit.interp rho) (shl_lit_be (a :: bs1) (b :: l))) = length (map (Lit.interp rho) bsres)). { now rewrite H1. } rewrite !map_length in H3. rewrite <- (length_shl_be (a :: bs1) (b :: l)) in H3. now simpl in *. + 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