proposition: Lemma measure_format_length_Spec n : (forall (a : A) b ctx ctx', computes_to (format_A a ctx) (b, ctx') -> bin_measure b = n) -> forall l b ctx ctx', computes_to (format_list l ctx) (b, ctx') -> bin_measure b = n * (length l).
proof: Proof. induction l; simpl; intros. - computes_to_inv; injections. pose proof (mappend_measure mempty mempty) as H'; rewrite mempty_left in H'. simpl bin_measure in H'; simpl mempty in H'; omega. - unfold Bind2 in *; computes_to_inv; injections. destruct v; destruct v0; simpl in *. rewrite mappend_measure. apply H in H0; rewrite H0. apply IHl in H0'; rewrite H0'. rewrite Mult.mult_succ_r. auto with arith. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Base.FixFormat Coq.Lists.List