More than 5 years have passed since last update.
概要
Coqでは Fix という不動点オペレータを使って再帰関数を定義することができる。より複雑な再帰関数を定義したくなった場合に便利なことがある。
factorialの例
再帰関数といえば factorial 。階乗を計算する関数を考えてみる。
定義
Fact_definition.v
Definitionfact(n:nat):nat.refine(Fix(lt_wf)(fun_=>nat)(funnF=>matchnaskreturnn=k->natwith|O=>fun_=>1|Sn'=>fun_=>n*Fn'_end(eq_refl_))n).rewritee.autowitharith.Defined.便利な補題
Fixpointで定義した場合に比べて、計算したいアルゴリズムと停止性のための処理がごちゃまぜになってしまっているため、以下のような補題があるとうれしい。
Fact_theory.v
Lemmafact_equation:foralln:nat,factn=matchnwith|0=>1|Sp=>(Sp)*factpend.Proof.introsn.unfoldfactat1.rewriteFix_eq.-destructn;reflexivity.-introsxfgF.destructx;[reflexivity|nowrewriteF].Qed.Lemmafact_ind:forallP:nat->nat->Prop,P01->(foralln:nat,Pn(factn)->P(Sn)(Sn*factn))->foralln:nat,Pn(factn).Proof.introsPIH_0IH_Sn.apply(lt_wf_indn(funn=>Pn(factn))).introsxH.destructx.-assumption.-rewritefact_equation.applyIH_S.applyH.nowautowitharith.Qed.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme