Last active
September 28, 2017 11:54
Star
You must be signed in to star a gist
CoqでFixを使って再帰関数を定義してみる ref: http://qiita.com/yoshihiro503/items/d92e67029929e4335022
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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