simpl Tactic

http://d.hatena.ne.jp/propella/20090215/p1

Coq < Parameter a b :nat.
a is assumed
b is assumed

Coq < Print plus.
plus = 
fix plus (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (plus p m)
  end
     : nat -> nat -> nat

Argument scopes are [nat_scope nat_scope]


Coq < Eval simpl in S a + (S b).
     = S (a + S b)
     : nat

Coq < Eval simpl in S a + (S a + (S b)).
     = S (a + S (a + S b))
     : nat

外側から簡約され、内側も再帰的に簡約される。

Coq < Definition hoge (a : nat) : nat := 1 + a.
hoge is defined

Coq < Eval simpl in hoge 1.
     = hoge 1
     : nat

Coq < Eval compute in hoge 1.
     = 2
     : nat

computeと違い、関数の中までは展開してくれない。

よく分からんが、Fixpoint + パターンマッチな関数なら、simplでも関数展開してくれる。ようだ。そうでなければ、plusで上記のような挙動になるはずがない。

Coq < Fixpoint mymatch (n : nat) : nat :=                             
Coq < match n with
Coq < | O => S O
Coq < | S n' => S (mymatch n')
Coq < end.

Coq < Eval simpl in mymatch (S a).
     = S (mymatch a)
     : nat

しかし、simpl. で何が行なわれるか、今迄考えたこともなかった。
だからテキトーにレバガチャして、技が出たらラッキーなストII初心者状態だったわけだ。どうりで分かってる感がなかったわけだ。これで少しは進歩出来たかもしれない。