proposition: Corollary CorrectEncoder_Restrict_Format (format : FormatM S T) (encode : EncodeM S T) (P : S -> Prop) (decideable_P : DecideableEnsemble P) : CorrectEncoder format encode -> CorrectEncoder (Restrict_Format P format) (fun s => if (DecideableEnsembles.dec s) then encode s else fun _ => None).
proof: Proof. intros; replace (fun s : S => if DecideableEnsembles.dec s then encode s else fun _ : CacheFormat => None) with (Compose_Encode encode (fun s => if DecideableEnsembles.dec s then Some s else None)). eapply CorrectEncoder_Compose; intros; try (destruct (DecideableEnsembles.dec s) eqn: ?; first [discriminate | injections]); intuition eauto. - eapply dec_decides_P; eauto. - eapply Decides_false; subst; eauto. - subst; eauto. - apply functional_extensionality; intros; unfold Compose_Encode; find_if_inside; reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs