如何用sed/awk替换Coq代码中Proof块为对应Lemma名称？

我需要处理包含大量Coq代码片段的文件，这些片段遵循以下模式：

Lemma <LEMMANAME> :
<LEMMASTATEMENT>
Proof.
<PROOF>
Qed.

希望替换为：

Lemma <LEMMANAME> :
<LEMMASTATEMENT>
Proof.
exact <LEMMANAME>
Qed.

相关规则：

• <LEMMANAME>是无空格的合法Coq标识符，冒号后直接换行
• <LEMMASTATEMENT>可有多行，不含以Proof.开头的行
• Proof.后直接换行
• <PROOF>可有多行，不含以Qed.开头的行
• Qed.后直接换行

现有的sed脚本只能把Proof块替换为固定内容，无法复用<LEMMANAME>：

sed -i '/Proof./,/Qed./c\Proof.\nexact LEMMANAMEHERE\nQed.' file

需要能插入对应<LEMMANAME>的sed或awk解决方案，要求支持文件内联修改，而非生成副本。

方案一：使用sed实现 #

以下是兼容GNU sed的内联修改命令，可捕获并复用Lemma名称：

sed -i -E '/^Lemma ([^ ]+) :$/{h;n;:a;/^Proof.$/{x;s/Lemma ([^ ]+) :/\1/;G;s/(.*)\n(.*)/Proof.\nexact \1\nQed./;b};n;ba}' file

命令逻辑 #

1. 匹配以Lemma开头的定义行，捕获无空格的标识符并存入保持空间
2. 逐行读取后续内容，直到匹配到Proof.行
3. 取出之前捕获的Lemma名称，替换Proof块内容为exact <LEMMANAME>
4. 继续处理文件剩余内容

如果是BSD sed（如macOS系统），需调整-i参数和换行符写法：

sed -i '' -E '/^Lemma ([^ ]+) :$/{h;n;:a;/^Proof.$/{x;s/Lemma ([^ ]+) :/\1/;G;s/(.*)\n(.*)/Proof.\
exact \1\
Qed./;b};n;ba}' file

方案二：使用awk实现 #

awk的逻辑更直观，通过记录Lemma名称来替换Proof块：

awk -i inplace '/^Lemma ([^ ]+) :$/ {lemma=$2; print; next} /^Proof.$/ {print; print "exact " lemma; while (getline > 0) {if ($0 == "Qed.") {print; break}}} 1' file

命令逻辑 #

1. 匹配Lemma定义行时，记录第二个字段（即Lemma名称）并打印当前行
2. 匹配到Proof.行时，依次打印Proof.、exact <LEMMANAME>，然后循环读取内容直到遇到Qed.并打印
3. 其他行（如Lemma陈述部分）直接打印

注：如果你的awk不支持-i inplace参数，可通过临时文件实现内联修改：

awk '/^Lemma ([^ ]+) :$/ {lemma=$2; print; next} /^Proof.$/ {print; print "exact " lemma; while (getline > 0) {if ($0 == "Qed.") {print; break}}} 1' file > tmp && mv tmp file

内容的提问来源于stack exchange，提问作者R. Bosman