Coq：一元到二进制的转换答案

【问题标题】：Coq: unary to binary convertionCoq：一元到二进制的转换
【发布时间】：2020-08-12 20:18:28
【问题描述】：

任务：编写一个将自然数转换为二进制数的函数。

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。

【问题讨论】：

从不同的角度看待问题有一个更简单的解决方案。在这里，您尝试将bin 构造函数Z、A、B 转换为nat 上的操作。翻转过来：你能把nat构造函数Z、S翻译成对bin的操作吗？
@Li-yaoXia The SF book already heavily hints at that solution 要求你写incr : bin -> bin，给nat_to_bin := nat_rec _ Z (fun _ => incr). 我假设OP知道那个解决方案并且故意不这样做。

标签： coq logical-foundations

【解决方案1】：

证明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.

【讨论】：