proposition: Lemma CorrectEncoder_Compose (format : FormatM S' T) (encode : EncodeM S' T) (f : S -> S' -> Prop) (f' : S -> option S') (f'_refines_f_1 : forall s s', f' s = Some s' -> f s s') (f'_refines_f_2 : forall s, f' s = None -> forall s', ~ f s s') (f'_sound_choice : forall s s', f' s = Some s' -> forall x env benv, format x env ∋ benv -> f s x -> format s' env ∋ benv) : CorrectEncoder format encode -> CorrectEncoder (Compose_Format format f) (Compose_Encode encode f').
proof: Proof. unfold CorrectEncoder, Compose_Encode, Compose_Format in *; split; intros. - apply unfold_computes. destruct (f' a) eqn: ?; simpl in *; try discriminate. eapply H in H0; eexists; intuition eauto. - rewrite unfold_computes; intro; destruct_ex; split_and. destruct (f' a) eqn: ?; simpl in *; try discriminate. eapply H4; eauto. eapply f'_refines_f_2; eauto. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs