proposition: Lemma option_format_correct {S T} {cache : Cache} {cacheAddNat : CacheAdd cache nat} (monoid : Monoid T) {P : CacheDecode -> Prop} {P_invT P_invE : (CacheDecode -> Prop) -> Prop} (P_inv_pf : cache_inv_Property P (fun P => P_invT P /\ P_invE P)) (Some_Predicate : S -> Prop) (None_Predicate : Prop) (b' : bool) (predicate := fun a_opt => decides (negb b') (a_opt = None) /\ match a_opt with | Some s => Some_Predicate s | None => None_Predicate end) (format_Some : FormatM S T) (format_None : FormatM () T) (decode_Some : DecodeM (S * T) T) (decode_None : DecodeM (() * T) T) (decode_Some_pf : cache_inv_Property P P_invT -> CorrectDecoder monoid Some_Predicate Some_Predicate eq format_Some decode_Some P format_Some) (decode_None_pf : cache_inv_Property P P_invE -> CorrectDecoder monoid (fun _ => None_Predicate) (fun _ => None_Predicate) (fun u _ => True) format_None decode_None P format_None) : CorrectDecoder monoid predicate predicate eq (format_option format_Some format_None) (option_decode monoid decode_Some decode_None b') P (format_option format_Some format_None).
proof: Proof. eapply format_decode_correct_alt. 2: instantiate (1 := predicate). Focus 7. { eapply injection_decode_correct with (inj := fun v => match v with | inl vs => Some vs | inr _ => None end). eapply option_format_correct' with (b'0 := b') (Source_Predicate := fun s => match s with | Some s => _ s | None => _ end); eauto. - simpl; intros. instantiate (1 := fun s v => match s with | Some s => match v with | Some vs => s = vs | None => False end | None => match v with | Some vs => False | None => True end end). simpl; destruct s; destruct v; eauto. - intros. unfold predicate; destruct v; destruct b'; intuition eauto; simpl; try congruence. - intros. instantiate (1 := fun v_opt => match v_opt with | Some vs => format_Some vs | _ => format_None () end); simpl. destruct v; eauto. destruct u; apply unfold_computes; eauto. } all: idtac. - unfold flip, pointwise_relation; intros. unfold predicate; intuition eauto. - unfold flip, pointwise_relation, impl; intros. unfold predicate in *; intuition eauto. - unfold flip, pointwise_relation; intros; intuition eauto. subst; destruct a0; eauto. destruct a; destruct a0; intuition; try congruence. - unfold flip, pointwise_relation; intros; intuition eauto. unfold EquivFormat; intros; reflexivity. - unfold flip, pointwise_relation; intros; intuition eauto. unfold Compose_Decode, option_decode, option_decode'. destruct b'; simpl. destruct (decode_Some a a0) as [ [ [? ?] ?] | ]; simpl; eauto. destruct (decode_None a a0) as [ [ [? ?] ?] | ]; simpl; eauto. - unfold flip, pointwise_relation; intros; intuition eauto. unfold EquivFormat; intros. unfold format_option; destruct s; simpl. reflexivity. reflexivity. Qed.
imports: Fiat.Common Fiat.Computation Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats