proposition: Theorem Vector_decode_correct : forall sz, CorrectDecoder monoid (fun ls => forall x, Vector.In x ls -> A_predicate x) (fun ls => forall x, Vector.In x ls -> A_predicate x) eq format_Vector (decode_Vector sz) A_cache_inv format_Vector.
proof: Proof. split. { intros env env' xenv l l' ext env_OK Eeq Ppred Penc. generalize dependent env. generalize dependent env'. generalize dependent xenv. generalize dependent l'. induction l. { intros. simpl in *. simpl in *; intuition; computes_to_inv; injections; simpl; rewrite mempty_left; eauto. eexists _, _; intuition eauto. computes_to_econstructor. } { intros; simpl in *. assert (A_predicate h) by (eapply Ppred; econstructor). unfold Bind2 in Penc; computes_to_inv; subst. destruct v; destruct v0; simpl in *. injections. destruct (proj1 A_decode_pf _ _ _ _ _ (mappend b0 ext) env_OK Eeq H Penc) as [ ? [? [? xenv_OK] ] ]. setoid_rewrite <- mappend_assoc; setoid_rewrite H0; simpl. split_and; subst. destruct (IHl (fun x H => Ppred x (Vector.In_cons_tl _ _ _ H)) b0 xenv _ H5 c) as [? [? ?] ]; intuition eauto. setoid_rewrite H4; simpl. eexists _, _; intuition; try congruence. simpl; unfold Bind2; eauto. } } { induction sz; simpl; intros. - injections; simpl; split; eauto; repeat eexists; simpl; intuition eauto. symmetry; apply mempty_left. inversion H1. - destruct (A_decode t env') as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate. destruct (decode_Vector sz b c) as [ [ [? ?] ?] | ] eqn: ? ; simpl in *; try discriminate; injections. eapply (proj2 A_decode_pf) in Heqo; eauto; destruct Heqo as [? [? ?] ]; destruct_ex; intuition; subst; eapply IHsz in Heqo0; eauto; destruct Heqo0 as [? [? ?] ]; destruct_ex; intuition; subst. simpl. eexists _, _; intuition eauto. computes_to_econstructor; eauto. computes_to_econstructor; eauto. rewrite mappend_assoc; reflexivity. inversion H5; subst; eauto. apply inj_pair2_eq_dec in H13; subst; eauto using eq_nat_dec. } Qed.
imports: Fiat.Narcissus.Common.Specs Coq.Arith.Peano_dec Coq.Logic.Eqdep_dec Coq.Lists.List