proposition: Lemma implies_binop : tests -> forall x y, binop_tests x (bitsFromInt16 x) y (bitsFromInt16 y).
proof: Proof. move => H x y. have H': unop_tests x by apply implies_unop. move: H'=> /andP [_ /andP [_ /andP [_ /andP [_ /andP [H1 _]]]]]. case Hc: (toNat (bitsFromInt16 x) <= wordsize); rewrite Hc in H1. have Hb: (binop_tests x (bitsFromInt16 x) y (bitsFromInt16 y)) && (shift_tests x (toNat (bitsFromInt16 x)) y (bitsFromInt16 y)). move: H1=> /forallInt16P H1. move: (H1 (fun y => (binop_tests x (bitsFromInt16 x) y (bitsFromInt16 y)) && (shift_tests x (toNat (bitsFromInt16 x)) y (bitsFromInt16 y))))=> H2. apply H2=> y'. by apply idP. by move: Hb=> /andP [-> _]. move: H1=> /forallInt16P H1. move: (H1 (fun y => binop_tests x (bitsFromInt16 x) y (bitsFromInt16 y)))=> H2. apply H2=> y'. by apply idP. Qed.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits) ExtrOcamlBasic