proposition: Lemma decode_word_plus : forall n m (v : ByteString), WordOpt.decode_word' (n + m) v = (`(w, v') <- WordOpt.decode_word' (m + n) v; Some (eq_rect _ word w _ (Plus.plus_comm _ _), v')).
proof: Proof. induction n; simpl; intros. - revert v; induction m; simpl; intros. + repeat f_equal; apply Eqdep_dec.eq_rect_eq_dec; intros; eauto using Peano_dec.eq_nat_dec. + destruct (ByteString_dequeue v) as [ [? ?] | ]; simpl; eauto. rewrite IHm, !DecodeBindOpt_assoc; apply DecodeBindOpt_under_bind; intros. simpl; eauto. repeat f_equal; clear. eapply SW_word_eq_rect_eq. - etransitivity. apply DecodeBindOpt_under_bind; intros. set_evars; rewrite IHn, !DecodeBindOpt_assoc. unfold H; reflexivity. simpl; replace (WordOpt.decode_word' (m + S n) v) with (`(w', v') <- WordOpt.decode_word' (S (m + n)) v; Some (eq_rect _ word w' _ (plus_n_Sm _ _), v')). + simpl; repeat (rewrite !DecodeBindOpt_assoc; apply DecodeBindOpt_under_bind; intros). simpl; repeat f_equal; erewrite SW_word_eq_rect_eq; rewrite <- transport_pp; f_equal. + simpl; rewrite !DecodeBindOpt_assoc. etransitivity. apply DecodeBindOpt_under_bind; intros. set_evars; rewrite !DecodeBindOpt_assoc; simpl. unfold H; reflexivity. simpl. pose proof (IHn (S m) v); simpl in H. rewrite !DecodeBindOpt_assoc in H; simpl. destruct (ByteString_dequeue v) as [ [? ?] | ]; simpl in *. setoid_rewrite DecodeBindOpt_assoc in H; simpl. destruct (decode_word' (m + n) b0) as [ [? ?] | ]; simpl in *. assert (n + S m = m + S n) by omega. assert (eq_rect _ (fun n => option (word n * ByteString)) (decode_word' (n + S m) v) (m + S n) H0 = eq_rect _ (fun n => option (word n * ByteString)) (Some (eq_rect (S (m + n)) word (SW_word b w) (n + S m) (plus_comm (S m) n), b1)) (m + S n) H0) by (intros; rewrite H; reflexivity). rewrite Some_eq_rect_eq in H1. rewrite <- transport_pp in H1. erewrite Eqdep_dec.eq_proofs_unicity with (p1 := (plus_n_Sm m n)); intros; try omega. match goal with H: _ = ?a' |- ?a = _ => replace a with a' by reflexivity end. assert (n + S m = m + S n) by omega. rewrite <- eq_rect_decode_word with (H := H0), H; simpl. destruct H0; reflexivity. assert (n + S m = m + S n) by omega. rewrite <- eq_rect_decode_word with (H := H0), H; simpl. destruct H0; reflexivity. assert (n + S m = m + S n) by omega. rewrite <- eq_rect_decode_word with (H := H0), H; simpl. destruct H0; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality