proposition: Lemma format_body_monotone : forall rec rec' : funType [DomainName; CacheFormat] (B * CacheFormat), refineFun rec rec' -> refineFun (fDom := [DomainName; CacheFormat]) (fun (domain : DomainName) (env0 : CacheFormat) => If string_dec domain "" Then format_ascii terminal_char env0 Else ( position <- { position | forall p, position = Some p -> In p (getE env0 domain)}; Ifopt position as position Then `(ptr1b, env') <- format_word (proj1_sig (fst position)) env0; `(ptr2b, env'0) <- format_word (snd position) env'; ret (mappend ptr1b ptr2b, env'0) Else (`(label, domain') <- {labeldomain' : string * string | (domain = (fst labeldomain' ++ String "." (snd labeldomain'))%string \/ labeldomain' = (domain, ""%string)) /\ ValidLabel (fst labeldomain') /\ (forall label' post' : string, domain = (label' ++ post')%string -> ValidLabel label' -> (String.length label' <= String.length (fst labeldomain'))%nat)}; `(lenb, env') <- format_nat 8 (String.length label) env0; `(labelb, env'0) <- format_string label env'; `(domainb, env'1) <- rec domain' env'0; ret (mappend (mappend lenb labelb) domainb, Ifopt peekE env0 as curPtr Then addE_G env'1 (domain, curPtr) Else env'1)))) (fun (domain : DomainName) (env0 : CacheFormat) => If string_dec domain "" Then format_ascii terminal_char env0 Else ( position <- { position | forall p, position = Some p -> In p (getE env0 domain)}; Ifopt position as position Then `(ptr1b, env') <- format_word (proj1_sig (fst position)) env0; `(ptr2b, env'0) <- format_word (snd position) env'; ret (mappend ptr1b ptr2b, env'0) Else (`(label, domain') <- {labeldomain' : string * string | (domain = (fst labeldomain' ++ String "." (snd labeldomain'))%string \/ labeldomain' = (domain, ""%string)) /\ ValidLabel (fst labeldomain') /\ (forall label' post' : string, domain = (label' ++ post')%string -> ValidLabel label' -> (String.length label' <= String.length (fst labeldomain'))%nat)}; `(lenb, env') <- format_nat 8 (String.length label) env0; `(labelb, env'0) <- format_string label env'; `(domainb, env'1) <- rec' domain' env'0; ret (mappend (mappend lenb labelb) domainb, Ifopt peekE env0 as curPtr Then addE_G env'1 (domain, curPtr) Else env'1)))).
proof: Proof. simpl; intros; unfold Bind2. apply General.refine_if; intros; rewrite H0; simpl. reflexivity. apply SetoidMorphisms.refine_bind. reflexivity. intro. apply SetoidMorphisms.refine_If_Opt_Then_Else_Proper. * intro; f_equiv; intro. * f_equiv; intro. unfold Bind2; f_equiv; intro. setoid_rewrite H; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt