proposition: Lemma refineADT_Build_ADT_Rep Sig oldRep newRep (AbsR : oldRep -> newRep -> Prop) : (@respectful_heteroT (forall idx, constructorType oldRep (ConstructorDom Sig idx)) (forall idx, constructorType newRep (ConstructorDom Sig idx)) (fun oldConstrs => (forall idx, methodType oldRep (fst (MethodDomCod Sig idx)) (snd (MethodDomCod Sig idx))) -> ADT Sig) (fun newConstrs => (forall idx, methodType newRep (fst (MethodDomCod Sig idx)) (snd (MethodDomCod Sig idx))) -> ADT Sig) (fun oldConstrs newConstrs => forall mutIdx, @refineConstructor oldRep newRep AbsR _ (oldConstrs mutIdx) (newConstrs mutIdx)) (fun x y => @respectful_heteroT (forall idx, methodType oldRep _ _) (forall idx, methodType newRep _ _) (fun _ => ADT Sig) (fun _ => ADT Sig) (fun obs obs' => forall obsIdx : MethodIndex Sig, @refineMethod oldRep newRep AbsR (fst (MethodDomCod Sig obsIdx)) (snd (MethodDomCod Sig obsIdx)) (obs obsIdx) (obs' obsIdx)) (fun obs obs' => refineADT))) (@Build_ADT Sig oldRep) (@Build_ADT Sig newRep).
proof: Proof. unfold Proper, respectful_heteroT; intros. let A := match goal with |- refineADT ?A ?B => constr:(A) end in let B := match goal with |- refineADT ?A ?B => constr:(B) end in eapply (@refinesADT Sig A B AbsR); unfold id, pointwise_relation in *; simpl in *; intros; eauto. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core