Library set

set

set というのはゴール内の部分項を指定した変数に束縛した上で 部分項をその変数に置換する tactic です。 証明項の形からは、let 式を構築します。 set の変種として、pose があり、これは純粋に let 式を構築するだけの tactic です。 まず、pose からみていきましょう。

前提: foo := 3 + 4 : nat pose により、前提に foo := 3 + 4 が追加されています。

証明項: (let foo := 3 + 4 in ?Goal) 証明項では、let 式により、foo が定義されています。 次に、set では行われる変数への置換が起きないことを確認してみましょう。

前提: bar := 1 + 1 : nat ゴール: 1 + 1 = 2 pose により、前提に bar が追加されましたが、 ゴールは変化していません。

証明項: (let foo := 3 + 4 in let bar := 1 + 1 in ?Goal) 証明項では let 式により、bar が定義されています。

次は、set では変数による置換も行われることを確認してみましょう。

前提: baz := 1 + 1 : nat ゴール: baz = 2 set により、baz が前提に追加され、ゴール内の 1 + 1 が baz に置換されていることがわかります。

証明項: (let baz := 1 + 1 in ?Goal) 証明項では、let 式により、baz が定義されています。 ゴールの型はここには表示されていないので、ゴール内で置換がおきたかどうかは この証明項の表示からはわかりません。