proposition: Lemma CorrectEncoder_sequence {S : Type} (format1 format2 : FormatM S T) (encode1 encode2 : EncodeM S T) (encode1_correct : CorrectEncoder format1 encode1) (encode1_consistent : forall s env tenv' tenv'', format1 s env ∋ tenv' -> format2 s (snd tenv') ∋ tenv'' -> exists tenv3 tenv4, encode1 s env = Some tenv3 /\ format2 s (snd tenv3) ∋ tenv4) (encode2_correct : CorrectEncoder format2 encode2) : CorrectEncoder (format1 ++ format2) (sequence_Encode encode1 encode2).
proof: Proof. unfold CorrectEncoder, sequence_Encode, sequence_Format, compose, DecodeBindOpt, BindOpt in *; intuition; intros. - destruct (encode1 a env) as [ [t1 xxenv] | ] eqn: ? ; simpl in *; try discriminate. destruct (encode2 a xxenv) as [ [t2 xxxenv] | ] eqn: ? ; simpl in *; try discriminate; injections. repeat computes_to_econstructor; eauto. - unfold Bind2 in *; computes_to_inv; destruct v; destruct v0; simpl in *. destruct (encode1 a env) as [ [t1 xxenv] | ] eqn: ? ; simpl in *; try discriminate; eauto. eapply H2; try eassumption. destruct (encode2 a xxenv) as [ [t2' xxxenv] | ] eqn: ? ; simpl in *; try discriminate; injections. specialize (encode1_consistent _ _ _ _ H4 H4'); destruct_ex; split_and. rewrite H6 in Heqo; injections; simpl in *. destruct x0; exfalso; eauto. Qed.
imports: Fiat.Computation Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Common.Notations Fiat.Narcissus.Formats.Base.FMapFormat Fiat.Narcissus.Formats.Base.LaxTerminalFormat