无法推断环境中函数的类型

Question

我正在尝试在 Coq 中实现二元决策图。我想使用 2CNF 公式创建 BDD。

一、进口；

Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.EqNat.
Require Import Program.Wf.

为此，我有带有自然数的文字来表示顺序。

Inductive literal := 
  | L (val: nat).

使用它，我创建了子句。

Inductive two_clause := 
  Or (left: literal) (right: literal).

接下来，我有了BDD以及BDD上的一些函数。

Inductive bdd := 
  | Vertex (L: literal) (left_edge: bdd) (right_edge: bdd)
  | Leaf (val: Prop).

Definition get_bdd_var (b: bdd) : option literal :=
  match b with
    | Vertex l _ _  => Some l
    | _             => None
  end.

Definition get_high (b: bdd) : bdd := 
  match b with 
    | Vertex _ h _  => h
    | Leaf v        => Leaf v
  end.

Definition get_low (b: bdd) : bdd := 
  match b with 
    | Vertex _ _ l  => l
    | Leaf v        => Leaf v
  end.

最后，我使用递归 apply 函数创建 BDD（为了简单起见，我减少了案例数量，只为

and

案例制作了 apply 算法。

Definition construct (p: literal) (T U: option bdd) : option bdd := 
  match (T, U) with 
    | (Some T, Some U)  => Some (Vertex p T U)
    | _                 => None
  end.

Fixpoint bdd_size (b: bdd) : nat := 
  match b with 
    | Leaf _ => 0
    | Vertex _ l r => 1 + (bdd_size l) + (bdd_size r)
  end
.

Definition bdds_size (b1 b2: bdd) : nat := 
  bdd_size b1 + bdd_size b2.

Variable o_map : literal -> nat.

Fixpoint apply_and (T U : bdd) {bdds_size T U} : option bdd := 
  let tvaro := get_bdd_var T in
  let uvaro := get_bdd_var U in
  match (tvaro, uvaro) with
    | (Some tvar, Some uvar) =>  
      match (compare (o_map (tvar)) (o_map (uvar))) with 
        | Lt => construct
                  (tvar) 
                  (apply_and (get_high T: bdd) U)
                  (apply_and (get_low T: bdd) U)
        | _  => construct
                  (tvar)
                  (apply_and (get_high T:bdd) (get_high U:bdd))
                  (apply_and (get_low T:bdd) (get_low U:bdd))
      end 
    | _ => None
   end.

但是，Coq 并不相信 apply 函数会终止。因此，我添加了 T 和 U 尺寸减小的减小论点。 但是，我收到消息称 Coq 无法推断

bdds_size

的类型。

我需要更改什么才能使其正常工作？

Answer 1

我认为问题中代码的直接问题本质上是语法错误，导致错误解析。

Fixpoint apply_and (T U : bdd) {bdds_size T U}

被解析为

apply_and

定义的开始，它采用两个类型为

T

的显式参数

U

和

bdd

，然后是三个隐式参数

bdds_size

、

T

和

U 

未指定类型。因为这显然不是您想要的，所以此后的任何错误都变得毫无意义。

根据文档，固定点注释应该是以下三种形式之一：

<fixannot> ::= { struct <ident> }
             | { wf <one_term> <ident> }
             | { measure <one_term> <ident>? <one_term>? }

此外，

wf

和

measure

形式只能与

Program Fixpoint

一起使用，而不是裸露的

Fixpoint

。

struct

形式对我们来说看起来没什么用，因为它期望现有参数之一减少，而我们想要注意到表达式

bdds_size T U

减少。因此，我们将切换到

Program Fixpoint

，并使用

measure

形式。

Program Fixpoint apply_and (T U : bdd) {measure (bdds_size T U)} : option bdd := 
  let tvaro := get_bdd_var T in
  let uvaro := get_bdd_var U in
  match (tvaro, uvaro) with
    | (Some tvar, Some uvar) =>  
      match (compare (o_map (tvar)) (o_map (uvar))) with 
        | Lt => construct
                  (tvar) 
                  (apply_and (get_high T) U)
                  (apply_and (get_low T) U)
        | _  => construct
                  (tvar)
                  (apply_and (get_high T) (get_high U))
                  (apply_and (get_low T) (get_low U))
      end 
    | _ => None
   end.
(* 8 obligations remaining *)

之后，您需要使用

Program

机制，例如

Next Obligation.

，来处理每个生成的义务。

然而，正如 Pierre Jouvelot 在评论中指出的那样，这些义务无法证明，因为

bdd_size (get_high (Leaf v)) < bdd_size (Leaf v)

不正确。