proposition: Lemma AxiomatizeMethodPostSpec_OK av {RepSpec RepImpl} AbsR {numRepArgs} cod dom codWrap domWrap : forall args DecomposeRepPost meth, exists is_ret_adt : bool, forall (in_out : list (Value av * option av)) (ret : Value av), (exists (r : RepImpl) (r' : RepSpec), AbsR r' r /\ @AxiomatizeMethodPostSpec' dom cod RepSpec RepImpl av numRepArgs AbsR codWrap domWrap args (DecomposeRepPost r) (meth r') in_out ret) -> if is_ret_adt then exists a : av, ret = ADT a else exists w : W, ret = SCA av w.
proof: Proof. destruct cod. - exists (gWrapTag codWrap); simpl; revert args DecomposeRepPost meth. induction dom; simpl in *; intros. + destruct H as [r [r' [r'' [v' [? [? [? [? [? ? ] ] ] ] ] ] ] ] ]; subst. pose proof (gWrapTagConsistent codWrap); find_if_inside; eauto. + destruct H as [r [r' [? [x ? ] ] ] ]; subst. eapply (IHdom (snd domWrap) ((@wrap _ _ (gWrap (fst domWrap)) x, None) :: args) (fun r r' => (DecomposeRepPost r r')) (fun r => meth r x) in_out); eauto. - exists false; simpl; revert args DecomposeRepPost meth. induction dom; simpl in *; intros. + destruct H as [r [r' [r'' [? [? [? [? [? ? ] ] ] ] ] ] ] ]; subst; eauto. + destruct H as [r [r' [? [x ? ] ] ] ]; subst; eauto. eapply (IHdom (snd domWrap) ((@wrap _ _ (gWrap (fst domWrap)) x, None) :: args) (fun r r' => DecomposeRepPost r r') (fun r => meth r x) in_out); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction