Coq：合計から中括弧を削除します。

Question

a + (b + (c + d))のような合計があり、これを補題を適用するためにa + b + c + dに変換したいとします。

Nat.add_assocでこれを手動で行うのは非常に面倒です。もっとスマートな方法がありますか？私が使用する

Answer 1

「簡単ですが、素敵ではない」の方法は、あなたがそれはもう適用できなくなるまで、いくつかの戦術を繰り返している、repeat、戦術を使用することができますreplace (a + (b + (c + d)))) with (a + b + c + d) by now omega

Answer 2

です：

repeat rewrite Nat.add_assoc. 

以上の簡潔なバージョン：

rewrite !Nat.add_assoc. 

repeatの亜種とまったく同じです。

このアプローチの欠点は、目標のどこにでも書き換えられることです。そのため、数式の一部を選択して、書き換えを実行することができます。