proposition: Lemma refineADT_BuildADT_Rep_refine_All {n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist (B := @consDef oldRep) consSigs) (methDefs : ilist (B := @methDef oldRep) methSigs) (refined_consDefs : ilist (B := @consDef newRep) consSigs) (refined_methDefs : ilist (B := @methDef newRep) methSigs) : refine_Constructors consDefs refined_consDefs -> refine_Methods methDefs refined_methDefs -> refineADT (BuildADT consDefs methDefs) (BuildADT refined_consDefs refined_methDefs).
proof: Proof. intros; eapply refineADT_Build_ADT_Rep with (AbsR := AbsR). - induction H; simpl. + intro; inversion mutIdx. + intro; revert IHrefine_Constructors H; clear. revert consSig constr_body refined_constr_body consSigs consDefs refined_consDefs; pattern n, mutIdx. match goal with |- ?P n mutIdx => simpl; apply (Fin.caseS P); simpl; intros; eauto end. - induction H0; simpl. + intro; inversion obsIdx. + intro; revert IHrefine_Methods H0; clear. revert methSig meth_body refined_meth_body methSigs methDefs refined_methDefs consSigs; pattern n', obsIdx. match goal with |- ?P n' obsIdx => simpl; apply (Fin.caseS P); simpl; intros; eauto end. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.ADTRefinement.Refinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms