4

等価とローカル定義の違いがよくわかりません。たとえば、set戦術に関するドキュメントを読む場合:

用語を ident として覚える

これは set ( ident := term ) in * として動作し 、ローカル定義の代わりに論理 (ライプニッツの) 等価性を使用します

それはそう、

  1. set (ca := c + a) in *.たとえばca := c + a : Z、コンテキストで生成されますが、

  2. remember (c + a ) as ca.コンテキストで生成さHeqca : ca = c + aれます。

ケース 2. の場合、生成された仮説を のようrewrite Heqca.に使用できますが、ケース 1. の場合、 を使用できませんrewrite ca。

ケース 1. の目的は何ですか? また、実際の使用に関してケース 2. とどのように違いますか?

また、2 つの違いが基本的なものである場合、ドキュメント (8.5p1) で のrememberバリアントとして説明されているのはなぜですか?set

4

2 に答える 2

2

set a := b + b in H次のように書き換えると考えることができますH。

(fun a => H[b+b/a]) (b+b)

また

let a := b + b in
H[b+b/a]

つまり、一致しb+bたすべてのパターンを新しい変数に置き換えa、パターンの値にインスタンス化します。この点で、Hと 書き直された仮説は「変換」によって等しいままです。

確かに、remember はある意味で set の変形ですが、その意味は大きく異なります。この場合、remember は新しい等価性の証明を導入しeq_refl: b + b = b + b、左側の部分を抽象化します。これは、パターンマッチングなどで十分な自由度を持つのに便利です...これは、よりアトミックな戦術の観点から覚えています:

Lemma U b c : b + b = c + c.
Proof.
assert (b + b = b + b). reflexivity.
revert H.
generalize (b+b) at 1 3.
intros n H.
于 2016-06-25T08:46:55.477 に答える
2

@ejgallegoの回答に加えて。

はい、rewrite(ローカル) 定義はできませんが、できunfoldます:

set (ca := c + a) in *.    
unfold ca.

実際の使用における違いについては、まったく異なります。たとえば、@eponier によるこの回答を参照してください。remember誘導が思い通りに機能するように、戦術に依存します。しかし、それを置き換えるrememberとset失敗します:

Inductive good : nat -> Prop :=
  | g1 : good 1
  | g3 : forall n, good n -> good (n * 3)
  | g5 : forall n, good n -> good (n + 5).

Require Import Omega.

作品のバリアントremember：

Goal ~ good 0.
  remember 0 as n.
  intro contra. induction contra; try omega.
  apply IHcontra; omega.
Qed.

バリアント withはそうではありません (動作する自由変数setを導入しなかったため):

Goal ~ good 0.
  set (n := 0). intro contra.
  induction contra; try omega.
  Fail apply IHcontra; omega.
Abort.
于 2016-06-25T09:01:24.377 に答える