proposition: Lemma Notation_Friendly_refinedUnderDelegates (RepT : Type) {DelegateIDs n n'} (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig n') (consDefs : ilist consSigs) (methDefs : ilist methSigs) (DelegateSigs : Fin.t DelegateIDs -> ADTSig) (rep : (Fin.t DelegateIDs -> Type) -> Type) (refinedConstructors : forall (DelegateReps : Fin.t DelegateIDs -> Type) (DelegateConsImpls : forall idx (cidx : ConstructorIndex (DelegateSigs idx)), constructorType (DelegateReps idx) (ConstructorDom _ cidx)) (DelegateMethImpls : forall idx (midx : MethodIndex (DelegateSigs idx)), methodType (DelegateReps idx) (fst (MethodDomCod _ midx)) (snd (MethodDomCod _ midx))), ilist (B := fun Sig : consSig => constructorType (rep DelegateReps) (consDom Sig)) consSigs) (refinedMethods : forall (DelegateReps : Fin.t DelegateIDs -> Type) (DelegateConsImpls : forall idx (cidx : ConstructorIndex (DelegateSigs idx)), constructorType (DelegateReps idx) (ConstructorDom _ cidx)) (DelegateMethImpls : forall idx (midx : MethodIndex (DelegateSigs idx)), methodType (DelegateReps idx) (fst (MethodDomCod _ midx)) (snd (MethodDomCod _ midx))), ilist (B := fun Sig : methSig => methodType (rep DelegateReps) (methDom Sig) (methCod Sig)) methSigs) (DelegateSpecs : forall idx, ADT (DelegateSigs idx)) (cAbsR : forall (DelegateReps : Fin.t DelegateIDs -> Type) (DelegateConsImpls : forall idx (cidx : ConstructorIndex (DelegateSigs idx)), constructorType (DelegateReps idx) (ConstructorDom _ cidx)) (DelegateMethImpls : forall idx (midx : MethodIndex (DelegateSigs idx)), methodType (DelegateReps idx) (fst (MethodDomCod _ midx)) (snd (MethodDomCod _ midx))) (DelegateImpls := fun idx => {| Rep := DelegateReps idx; Constructors := DelegateConsImpls idx; Methods := DelegateMethImpls idx |}) (ValidImpls : forall idx : Fin.t DelegateIDs, refineADT (DelegateSpecs idx) (DelegateImpls idx)), RepT -> rep DelegateReps -> Prop) (constructorsRefinesSpec : forall (DelegateReps : Fin.t DelegateIDs -> Type) (DelegateConsImpls : forall idx (cidx : ConstructorIndex (DelegateSigs idx)), constructorType (DelegateReps idx) (ConstructorDom _ cidx)) (DelegateMethImpls : forall idx (midx : MethodIndex (DelegateSigs idx)), methodType (DelegateReps idx) (fst (MethodDomCod _ midx)) (snd (MethodDomCod _ midx))) (DelegateImpls := fun idx => {| Rep := DelegateReps idx; Constructors := DelegateConsImpls idx; Methods := DelegateMethImpls idx |}) (ValidImpls : forall idx : Fin.t DelegateIDs, refineADT (DelegateSpecs idx) (DelegateImpls idx)), Iterate_Dep_Type_BoundedIndex (fun idx => @refineConstructor (RepT) (rep DelegateReps) (cAbsR _ _ _ ValidImpls) (consDom (Vector.nth consSigs idx)) (getConsDef consDefs idx) (ith (refinedConstructors DelegateReps DelegateConsImpls DelegateMethImpls) idx))) (methodsRefinesSpec : forall (DelegateReps : Fin.t DelegateIDs -> Type) (DelegateConsImpls : forall idx (cidx : ConstructorIndex (DelegateSigs idx)), constructorType (DelegateReps idx) (ConstructorDom _ cidx)) (DelegateMethImpls : forall idx (midx : MethodIndex (DelegateSigs idx)), methodType (DelegateReps idx) (fst (MethodDomCod _ midx)) (snd (MethodDomCod _ midx))) (DelegateImpls := fun idx => {| Rep := DelegateReps idx; Constructors := DelegateConsImpls idx; Methods := DelegateMethImpls idx |}) (ValidImpls : forall idx : Fin.t DelegateIDs, refineADT (DelegateSpecs idx) (DelegateImpls idx)), Iterate_Dep_Type_BoundedIndex (fun idx => @refineMethod (RepT) (rep DelegateReps) (cAbsR _ _ _ ValidImpls) (methDom (Vector.nth methSigs idx)) (methCod (Vector.nth methSigs idx)) (getMethDef methDefs idx) (ith (refinedMethods DelegateReps DelegateConsImpls DelegateMethImpls) idx))) : refinedUnderDelegates (BuildADT (Rep := RepT) consDefs methDefs) {| DelegateeSigs := DelegateSigs; DelegatedImplementation := fun DelegateReps DelegateConsImpls DelegateMethImpls => BuildADT (Rep := rep DelegateReps) (imap (@Build_consDef _) (refinedConstructors DelegateReps DelegateConsImpls DelegateMethImpls)) (imap (@Build_methDef _) (refinedMethods DelegateReps DelegateConsImpls DelegateMethImpls)); DelegateeSpecs := DelegateSpecs |}.
proof: Proof. unfold refinedUnderDelegates; simpl; intros. eapply (@refinesADT _ (BuildADT (Rep := RepT) consDefs methDefs) (BuildADT (Rep := rep (fun idx => DelegateReps idx)) _ _) (cAbsR DelegateReps _ _ ValidImpls)). - intros. unfold Constructors; simpl. rewrite <- ith_imap; eauto. eapply (Lookup_Iterate_Dep_Type _ (constructorsRefinesSpec _ _ _ ValidImpls) idx). - intros. unfold Methods; simpl. rewrite <- ith_imap; eauto. eapply (Lookup_Iterate_Dep_Type _ (methodsRefinesSpec _ _ _ ValidImpls) idx). Defined.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory