■

δ-reduction

δ-reduction は変数をその定義で置き換える。

まず何か定義して、

Coq < Definition hoge := fun x:nat => 2+x.
hoge is defined

cbvを実行してみる。

Coq < Eval cbv delta [hoge] in (hoge 3).
     = (fun x : nat => 2 + x) 3
     : nat

この場合は「hoge」だけを展開する。

さらに「plus」も展開してみる。

Coq < Eval cbv delta [hoge plus] in (hoge 3).
     = (fun x : nat =>
        (fix plus (n m : nat) {struct n} : nat :=
           match n with
           | 0 => m
           | S p => S (p + m)
           end) 2 x) 3
     : nat

全部の定義を展開したい場合は[]はいらない。

β-reduction

β-reduction は

(fun x:T, t) a

を

t{a/x}

に変換する。ここで{a/x}はtの中に含まれるxをaに置き換える操作。

Coq < Eval cbv delta [hoge] beta in (hoge 3).
     = 2 + 3
     : nat

さらにplusも展開すると

Coq < Eval cbv delta beta in (hoge 3).
     = (fix plus (n m : nat) {struct n} : nat :=
          match n with
          | 0 => m
          | S p => S (p + m)
          end) 2 3
     : nat

ι-reduction

ι-reduction は再帰的な定義を展開する。fixpointもできるだけ計算してくれる。

まず、ちっとも計算できない場合。

Coq < Eval cbv delta beta iota in plus.
     = fix plus (n m : nat) {struct n} : nat :=
         match n with
         | 0 => m
         | S p => S (p + m)
         end
     : nat -> nat -> nat

これは n が分からないので、これ以上進まない。ひとつ引数を与えると

Coq < Eval cbv delta beta iota in (plus 2).
     = fun m : nat => S (S m)
     : nat -> nat

と、完全に計算してくれる。

ζ-reduction

let で定義した変数を定義で置き換える。δと似てるがなぜか違う名前がついている。

cbv, lazy

cbv と lazy は指定した reduction ルールをできるだけ適用する tactic。
ふたつの違いは call-by-value か call-by-need のどっちを使うかどうか。

red

red はゴールの頭の変数だけを展開する。

hnf

red をひたすら適用するんだと思う。

simpl

δを一回だけ使い、βιする？

unfold qualid

指定した変数を展開する。

fold term

unfold の逆。

pattern term

βの逆。たとえば、ゴール

Q x y z

に

lt_wf_ind :
  forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.

この定理を「n := y」として適用したいとする。ということは「P := fun n => Q x n z」ということになる。
そこで、pattern y とすると

(fun n => Q x n z) y

となって apply しやすくなる。ただこの場合は pattern しなくても、apply が正しくパターンマッチに成功するので、もっと複雑な場合で失敗したらこの方法を思い出すとよい。