proposition: Lemma add_bytes_into_checksum_inj_l: forall (y00 y01 y10 y11 : word 8) chk, (y00 <> wzero _ \/ y01 <> wzero _) -> (y10 <> wzero _ \/ y11 <> wzero _) -> add_bytes_into_checksum y00 y01 chk = add_bytes_into_checksum y10 y11 chk -> y00 = y10 /\ y01 = y11.
proof: Proof. unfold add_bytes_into_checksum, add_w16_into_checksum; intros * nonz0 nonz1 H. apply (f_equal (fun x => (wnot chk) ^1+ x)) in H. rewrite !(OneC_plus_assoc (wnot chk)), !(OneC_plus_comm (wnot chk)), !OneC_plus_wnot in H. repeat lazymatch goal with | [ H: context[wones _ ^1+ ?w] |- _ ] => let heq := fresh "heq" in let hneq := fresh "hneq" in destruct (weqdec w (wzero _)) as [ heq | hneq ]; [ rewrite heq in H; setoid_rewrite OneC_plus_wones_wzero in H | setoid_rewrite (OneC_plus_wones w hneq) in H ] | [ H: _ +^+ _ = wzero _ |- _ ] => apply wzero_combine in H; destruct H; subst end; try solve [split; reflexivity]; try solve [match goal with | [ H: _ \/ _ |- _ ] => destruct H; try congruence end]; first [apply combine_inj; eassumption | solve [intuition] ]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation