Skip to content

Instantly share code, notes, and snippets.

@yoshihiro503
Last active September 28, 2017 11:54
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save yoshihiro503/04059f454421d99c2c12cd95dfda41b1 to your computer and use it in GitHub Desktop.
CoqでFixを使って再帰関数を定義してみる ref: http://qiita.com/yoshihiro503/items/d92e67029929e4335022
Definition fact (n: nat) : nat.
refine (Fix (lt_wf) (fun _ => nat)
(fun n F =>
match n as k return n=k -> nat with
| O => fun _ => 1
| S n' => fun _ => n * F n' _
end (eq_refl _)
) n).
rewrite e. auto with arith.
Defined.
Definition fact (n: nat) : nat.
refine (Fix (lt_wf) (fun _ => nat)
(fun n F =>
match n as k return n=k -> nat with
| O => fun _ => 1
| S n' => fun _ => n * F n' _
end (eq_refl _)
) n).
rewrite e. auto with arith.
Defined.
Lemma fact_equation : forall n : nat, fact n = match n with
| 0 => 1
| S p => (S p) * fact p
end.
Proof.
intros n. unfold fact at 1. rewrite Fix_eq.
- destruct n; reflexivity.
- intros x f g F.
destruct x; [reflexivity| now rewrite F].
Qed.
Lemma fact_ind :
forall P : nat -> nat -> Prop,
P 0 1 ->
(forall n : nat, P n (fact n) -> P (S n) (S n * fact n)) ->
forall n : nat, P n (fact n).
Proof.
intros P IH_0 IH_S n.
apply (lt_wf_ind n (fun n => P n (fact n))). intros x H.
destruct x.
- assumption.
- rewrite fact_equation. apply IH_S. apply H. now auto with arith.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment