证明coq函数终止的一些帮助 [英] Some help proving coq function terminates

问题描述

我知道这是一个常见问题:)我将继续阅读，但是我做了一些搜索，但我还没有完全理解如何衡量"问题.有效

I know this is a common issue :) I will keep reading up, but I've done some searching and thing I don't fully understand how "measure" works

我正在完成本杰明·皮尔斯(Benjamin Pierce)的有关依赖类型的认证编程的课堂练习.这是我的代码.

I'm working through Benjamin Pierce's class exercises for Certified Programming with Dependent Types. Here's my code.

Inductive type : Type :=
| Nat
| Bool
| Pair : type -> type -> type.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool
| TPair : forall in1 in2, tbinop in1 in2 (Pair in1 in2).

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Fixpoint typeDenote (t : type) : Type :=
  match t with
    | Nat => nat
    | Bool => bool
    | Pair l r => prod (typeDenote l) (typeDenote r)
  end.

Fixpoint typeDepth (t: type): nat :=
  match t with
  | Nat => 1
  | Bool => 1
  | Pair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
  end.

Program Fixpoint tbinopDepth arg1 arg2 res (b: tbinop arg1 arg2 res)
{measure (Nat.max (typeDepth arg1) (typeDepth arg2))}
  : nat :=
match b with
| TPlus => 1
| TTimes => 1
| TEq Nat => 1
| TEq Bool => 1
| TEq (Pair A B) => tbinopDepth (TPair A B)
| TLt => 1
| TPair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
end.
Next Obligation.
simpl.
rewrite Nat.max_idempotent.
omega.
Qed.

Eval compute in tbinopDepth (TEq (Pair Nat Nat)). (* 2 *)
Eval compute in tbinopDepth (TEq Nat). (* 1 *)

Program Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  {measure (tbinopDepth b)} : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
    (*| TPlus => plus*)
    | TPlus => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat
    | TTimes => mult
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TEq (Pair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => eqb (tbinopDenote (TEq A) x1 y1) (tbinopDenote (TEq B) x2 y2)
        end : typeDenote Bool
    | TLt => leb
    | TPair _ _ => fun a b => (a,b)
  end.

但是，当我尝试编译它时，出现类型错误.注意:如果有重组的方法可以避免证明这一点，那当然是理想的！我对此表示欢迎.就是说，我想了解我的措施出了什么问题.

However, when I try to compile this I get a type error. Note: if there are ways to restructure this to avoid having to prove this, of course that is ideal! And I welcome any suggestions in that vein. That said, I'd like to understand where I'm going wrong with my measure.

我收到这样的错误:

The term "x1" has type
 "(fix typeDenote (t : type) : Type :=
     match t with
     | Nat => nat
     | Bool => bool
     | Pair l r => (typeDenote l * typeDenote r)%type
     end) A" while it is expected to have type
 "tbinopDepth (TEq A) < tbinopDepth b".

这就是为什么我认为很清楚我不太了解度量与代码如何交互的原因，因为我认为度量将产生证明义务，而不改变我定义的函数的类型.

Which is why I think it's clear I'm not quite understanding how the measure interacts with the code, as I thought the measure would generate a proof obligation, not change the type of the function I'm defining.

我应该补充一点，之所以包含两个评估值，是因为如果我能达到证明目标，则"tbinopDepth(TEq A)<tbinopDepth b" 是真的，因为我们知道b是 TEq(Pair AB)，所以 tbinopDepth(TEq A)和 tbinopDepth(TEqB)小于那个.但这不会进行类型检查...

I should add that the reason I included the two Evals is because if I can get to a proof goal, "tbinopDepth (TEq A) < tbinopDepth b" is true, since we know b is TEq (Pair A B) so it's probable that tbinopDepth (TEq A) and tbinopDepth (TEq B) are smaller than that. But it won't typecheck...

推荐答案

您可以通过分别定义相等运算符来解决此问题:

You can solve this issue by defining the equality operator separately:

Require Import Coq.Arith.Arith.
Set Implicit Arguments.

Inductive type : Type :=
| Nat
| Bool
| Pair : type -> type -> type.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool
| TPair : forall in1 in2, tbinop in1 in2 (Pair in1 in2).

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Fixpoint typeDenote (t : type) : Type :=
  match t with
    | Nat => nat
    | Bool => bool
    | Pair l r => prod (typeDenote l) (typeDenote r)
  end.

Fixpoint typeDepth (t: type): nat :=
  match t with
  | Nat => 1
  | Bool => 1
  | Pair A B => 1 + Nat.max (typeDepth A) (typeDepth B)
  end.

Fixpoint eqb arg : typeDenote arg -> typeDenote arg -> bool :=
  match arg return typeDenote arg -> typeDenote arg -> bool with
  | Nat => Nat.eqb
  | Bool => Bool.eqb
  | Pair A B => fun '(x1, y1) '(x2, y2) => andb (eqb _ x1 x2) (eqb _ y1 y2)
  end.

Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res) {struct arg1}
    : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b in tbinop arg1 arg2 res return typeDenote arg1 -> typeDenote arg2 -> typeDenote res with
  | TPlus => Nat.add
  | TTimes => Nat.mul
  | TEq arg => eqb arg
  | TLt => leb
  | TPair _ _ => fun a b => (a,b)
  end.

这篇关于证明coq函数终止的一些帮助的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！