1

注意：此代码与Some help proving coq function terminates中的代码相似（但不相同） 。在该代码处理相等问题的地方，它试图将这种小语言中的加法扩展为包括对。

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

Inductive numeric: type -> Set :=
| NNat: numeric Nat
| MPair: forall a1 a2, numeric a1 -> numeric a2 -> numeric (Pair a1 a2).

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : forall t, numeric t -> tbinop t t t
| TTimes : forall t, numeric t -> tbinop t t t
| 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) : Set :=
  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 MNat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat
    | TPlus (MPair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (x1 + y1, x2 + y2)
        end : typeDenote (Pair A B)
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TEq (Pair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        false (* obviously extremely wrong, doing this to unlock pending https://stackoverflow.com/questions/62912587/some-help-proving-coq-function-terminates *)
        (*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.

当我尝试编译它时，我得到了错误

Found type "typeDenote Nat" where "typeDenote wildcard'" was expected.

我的猜测是我需要某种方式连接typeDenote Nat到TPlus MNat. 我没有任何线索。我将继续搜索有关 Coq 依赖模式匹配的信息。将不胜感激有关如何实现此类事情的任何指示，因为受其他归纳类型约束的归纳类型在证明中似乎很常见！

编辑：我应该补充一点，我天真的想法是比赛应该是这样的：

| TPlus Nat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat

但后来它说：Found a constructor of inductive type type while a constructor of numeric is expected.。所以我猜它会自动缩小范围并进行替换，但我不知道如何将它连接回 Nat 以使其进行类型检查。

Edit2：所以，阅读文档，玩耍，我已经到了这个：

Program Fixpoint tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  {measure (tbinopDepth b)} : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b in tbinop arg1 arg2 res return (typeDenote arg1 -> typeDenote arg2 -> typeDenote res) with
    | @TPlus Nat MNat => fun (a:typeDenote Nat) (b:typeDenote Nat) => plus a b : typeDenote Nat
    | @TPlus (Pair A B) (MPair A' B') => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (tbinopDenote (@TPlus A A') x1 y1, tbinopDenote (@TPlus B B') x2 y2)
        end : typeDenote (Pair A B)
    | @TPlus _ _ => !
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TEq (Pair A B) => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        false (* obviously extremely wrong, doing this to unlock pending https://stackoverflow.com/questions/62912587/some-help-proving-coq-function-terminates *)
        (*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.

编译，我得到以下错误：

The term "x1" has type
 "(fix typeDenote (t : type) : Set :=
     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
    (TPlus (eq_rect t0 (fun H : type => numeric H) A' A ?e@{b0:=b; b:=b0})) <
  tbinopDepth b".

这是另一个问题的递归错误，而不是打字错误。

也就是说......这是实现这一目标的正确方法吗？我知道 Coq 提供了很多方法让我们自责：D

另一个问题：

| @TPlus (Pair A B) (MPair A' B') => fun (a:typeDenote (Pair A B)) (b:typeDenote (Pair A B)) =>
        match a, b with
        | (x1, x2), (y1, y2) => (tbinopDenote (@TPlus A A') x1 y1, tbinopDenote (@TPlus B B') x2 y2)
        end : typeDenote (Pair A B)

如果这确实是正确的方法，有没有办法证明 A=A' 和 B=B'？有必要吗？

4

1 回答 1

1

这与您提到的问题中的技巧相同：只需单独定义数字运算：

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

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

Inductive numeric: type -> Set :=
| NNat: numeric Nat
| MPair: forall a1 a2, numeric a1 -> numeric a2 -> numeric (Pair a1 a2).

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : forall t, numeric t -> tbinop t t t
| 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 add t (n : numeric t) : typeDenote t -> typeDenote t -> typeDenote t :=
  match n in (numeric t0) return (typeDenote t0 -> typeDenote t0 -> typeDenote t0) with
  | NNat => Nat.add
  | @MPair a1 a2 n0 n1 => fun '(x1, y1) '(x2, y2) => (add n0 x1 x2, add n1 y1 y2)
  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 n => add n
  | TTimes => Nat.mul
  | TEq arg => eqb arg
  | TLt => leb
  | TPair _ _ => fun a b => (a,b)
  end.
于 2020-07-15T13:15:52.767 回答