proposition: Lemma bijection_decode_correct' {S V T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (proj : S -> V) (inj : V -> option S) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view_format : FormatM V T) (decode_V : DecodeM (V * T) T) (decode_V_OK : CorrectDecoder monoid View_Predicate View_Predicate eq view_format decode_V P view_format) (view_OK : forall s, Source_Predicate s -> inj (proj s) = Some s) (view_OK' : forall v s, inj v = Some s -> proj s = v) (View_Predicate_OK : forall s, Source_Predicate s -> View_Predicate (proj s)) (View_Predicate_OK' : forall v s, View_Predicate v -> inj v = Some s -> Source_Predicate s) : CorrectDecoder monoid Source_Predicate Source_Predicate eq (Projection_Format view_format proj) (Compose_Decode' decode_V (fun s => match inj (fst s) with | Some s' => Some (s', snd s) | None => None end)) P (Projection_Format view_format proj).
proof: Proof. eapply injection_decode_correct'. - apply projection_decode_correct; eauto. - simpl; intros. subst. eexists. intuition eauto. - eauto. - intros. apply (EquivFormat_sym (EquivFormat_Projection_Format _ _)). erewrite view_OK'; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs