小编Kes*_*ong的帖子

我正在尝试compile_correct从依赖类型的认证编程的第一章做一个修改过的证明.在我的版本中,我试图利用progDenote折叠的事实,并在证明主要引理的证据中使用较弱的归纳假设compile_correct.

与本书相同的代码是:

Require Import Bool Arith List.
Set Implicit Arguments.

Inductive binop : Set := Plus | Times.

Inductive exp : Set :=
  | Const : nat -> exp
  | Binop : binop -> exp -> exp -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (e : exp) : nat :=
  match …