proposition: Lemma refine_Pick_Decoder_For {S T} {cache : Cache} {monoid : Monoid T} {Invariant} {FormatSpec} (decoderImpl : @CorrectDecoderFor S T cache monoid Invariant FormatSpec) : forall b ce cd, Equiv ce cd -> snd (proj1_sig decoderImpl) cd -> refine (Pick_Decoder_For Invariant FormatSpec b ce) (ret match fst (proj1_sig decoderImpl) b cd with | Some (a, _, _) => Some a | None => None end).
proof: Proof. intros. pose proof (proj2_sig (decoderImpl)). cbv beta in H1. destruct_ex; intuition. destruct H1 as [? ?]. intros v Comp_v; computes_to_inv; subst; apply PickComputes; intros. split; intros. - destruct (fst (proj1_sig decoderImpl) b cd) as [ [ [? ?] ?] | ] eqn: ?; try discriminate. injections. eapply H2 in Heqo; eauto. destruct Heqo as [? [? [? [? ?] ] ] ]. intuition. subst. eexists _, _, _ ; split; eauto. - destruct_ex; intuition; subst. eapply H1 in H5; eauto. destruct_ex; intuition. rewrite H5; simpl; congruence. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache