proposition: Lemma bijection_decode_correct {S V T} {cache : Cache} {P : CacheDecode -> Prop} {monoid : Monoid T} (proj : S -> V) (inj : V -> 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) = s) (view_OK' : forall v, proj (inj v) = v) (View_Predicate_OK : forall s, Source_Predicate s -> View_Predicate (proj s)) (View_Predicate_OK' : forall v, View_Predicate v -> Source_Predicate (inj v)) : CorrectDecoder monoid Source_Predicate Source_Predicate eq (Projection_Format view_format proj) (Compose_Decode decode_V (fun s => (inj (fst s), snd s))) P (Projection_Format view_format proj).
proof: Proof. eapply (bijection_decode_correct' _ (fun v => Some (inj v))); intuition eauto; injections; f_equal; intuition eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs