如何解决Coq:一元到二进制转换
任务:编写一个将自然数转换为二进制数的函数。
Inductive bin : Type :=
| Z
| A (n : bin)
| B (n : bin).
(* Division by 2. Returns (quotient,remainder) *)
Fixpoint div2_aux (n accum : nat) : (nat * nat) :=
match n with
| O => (accum,O)
| S O => (accum,S O)
| S (S n') => div2_aux n' (S accum)
end.
Fixpoint nat_to_bin (n: nat) : bin :=
let (q,r) := (div2_aux n 0) in
match q,r with
| O,O => Z
| O,1 => B Z
| _,O => A (nat_to_bin q)
| _,_ => B (nat_to_bin q)
end.
第二个函数给出错误,因为它在结构上不是递归的:
Recursive call to nat_to_bin has principal argument equal to
"q" instead of a subterm of "n".
我应该做些什么来证明它总是终止,因为q总是小于n。
解决方法
证明q
(几乎总是)小于n
:
(* This condition is sufficient,but a "better" one is n <> 0
That makes the actual function slightly more complicated,though *)
Theorem div2_aux_lt {n} (prf : fst (div2_aux n 0) <> 0) : fst (div2_aux n 0) < n.
(* The proof is somewhat involved...
I did it by proving
forall n k,n <> 0 ->
fst (div2_aux n k) < n + k /\ fst (div2_aux (S n) k) < S n + k
by induction on n first *)
然后在lt
上进行有根据的归纳:
Require Import Arith.Wf_nat.
Definition nat_to_bin (n : nat) : bin :=
lt_wf_rec (* Recurse down a chain of lts instead of structurally *)
n (fun _ => bin) (* Starting from n and building a bin *)
(fun n rec => (* At each step,we have (n : nat) and (rec : forall m,m < n -> bin) *)
match div2_aux n 0 as qr return (fst qr <> 0 -> fst qr < n) -> _ with (* Take div2_aux_lt as an argument; within the match the (div2_aux_lt n 0) in its type is rewritten in terms of the matched variables *)
| (O,r) => fun _ => if r then Z else B Z (* Commoning up cases for brevity *)
| (S _ as q,r) => (* note: O is "true" and S _ is "false" *)
fun prf => (if r then A else B) (rec q (prf ltac:(discriminate)))
end div2_aux_lt).
我可能建议让div2_aux
返回nat * bool
。
或者,Program Fixpoint
也支持以下归纳法:
Require Import Program.
(* I don't like the automatic introing in program_simpl and
now/easy can solve some of our obligations. *)
#[local] Obligation Tactic := (now program_simpl) + cbv zeta.
(* {measure n} is short for {measure n lt},which can replace the
core language {struct arg} when in a Program Fixpoint
(n can be any expression and lt can be any well-founded relation
on the type of that expression) *)
#[program] Fixpoint nat_to_bin (n : nat) {measure n} : bin :=
match div2_aux n 0 with
| (O,O) => Z
| (O,_) => B Z
| (q,O) => A (nat_to_bin q)
| (q,_) => B (nat_to_bin q)
end.
Next Obligation.
intros n _ q [_ mem] prf%(f_equal fst).
simpl in *.
subst.
apply div2_aux_lt.
auto.
Defined.
Next Obligation.
intros n _ q r [mem _] prf%(f_equal fst).
specialize (mem r).
simpl in *.
subst.
apply div2_aux_lt.
auto.
Defined.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。