I feel these example with increasing complexity are interesting:
ppt = 'abc HERE abc'
ept = 'abc TERM abc'
re_ppt = ppt.replace('HERE', '(.+)')
print()
print(f'{re_ppt=}')
out = re.search(pattern=re_ppt, string=ept)
print(out)
print(out.groups())
ppt = 'abc HERE abc HERE abc'
ept = 'abc TERM1 abc TERM2 abc'
re_ppt = ppt.replace('HERE', '(.+)')
print()
print(f'{re_ppt=}')
out = re.search(pattern=re_ppt, string=ept)
print(out)
print(out.groups())
print()
ppt = """(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal"""
print(f"{ppt=}")
ept = """(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) (eq_refl : 0 + 0 = 0)"""
print(f'{ept=}')
pattern_meta_var = r'\?(\w)+'
_ppt = re.sub(pattern=pattern_meta_var, repl='HERE', string=ppt)
print(f'{ppt=}')
_ppt = re.escape(_ppt)
print(f'{ppt=}')
re_ppt = _ppt.replace('HERE', '(.+)')
print(f'{re_ppt=}')
out = re.search(pattern=re_ppt, string=ept)
print(out)
print(out.groups())
print()
# sometimes the actual proof term missing won't have white spaces surrounding it but the ppt will have surrounding spaces where the hole
# would be. So in goal cames I removed the surrounding whitespaces. Then inserted a regex that accepts a hole with or
# without surrounding white spaces. That way in case the proof term in the hole does have surrounding white spaces then
# the regex hole catcher would match it anyway.
ppt = """\n (fun (n' : nat) (IH : n' + 0 = n') => ?Goal0) n)"""
ept = """\n (fun (n' : nat) (IH : n' + 0 = n') =>\n\teq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH : S n' + 0 = S n') n)"""
print(f"{ppt=}")
print(f'{ept=}')
pattern_meta_var = r'\s*\?(\w)+\s*'
_ppt = re.sub(pattern=pattern_meta_var, repl='HERE', string=ppt)
print(f'{_ppt=}')
_ppt = re.escape(_ppt)
print(f'{_ppt=}')
re_ppt = _ppt.replace('HERE', '\s*(.+)\s*')
print(f'{re_ppt=}')
out = re.search(pattern=re_ppt, string=ept)
print(out)
assert out is not None, f'expected two holes matched but go {out=}'
print(out.groups())
print()
ppt = """(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal
(fun (n' : nat) (IH : n' + 0 = n') => ?Goal0) n)"""
print(f"{ppt=}")
ept = """(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) (eq_refl : 0 + 0 = 0)
(fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH : S n' + 0 = S n') n)"""
print(f'{ept=}')
pattern_meta_var = r'\s*\?(\w)+\s*'
_ppt = re.sub(pattern=pattern_meta_var, repl='HERE', string=ppt)
print(f'{_ppt=}')
_ppt = re.escape(_ppt)
print(f'{_ppt=}')
re_ppt = _ppt.replace('HERE', '\s*(.+)\s*')
print(f'{re_ppt=}')
out = re.search(pattern=re_ppt, string=ept)
print(out)
print(out.groups())