1

我正在尝试为二进制自然数（位列表）定义前置函数。我想将我的函数的输入限制为修剪过的数字（没有前导零）并且是正数（所以，我不必担心零的前身）。

这是运算符的定义pred：

Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat2 => Fill One (pred nat2 H1 H2)
  | Fill One nat2 => Fill Zer nat2
  end.

我的第一个义务如下：

nat1: Nat
H1: is_trim nat1 = True
H2: is_pos nat1 H1 = True
H3: Empt = nat1
______________________________________(1/1)
Nat

但是，我不知道如何解决它。

矛盾显然在H2。但是，因为它取决于H1，所以我不能只rewrite nat1使用Empt，然后(is_pos Empt H1)使用False。

我应该如何证明这一点？

4

1 回答 1

2

这个目标确实是微不足道的，因为您可以为 Empt 情况返回任何自然数，并且请放心，没有人可以达到该数字，因为他们首先必须传入适当的H2 : is_pos nat1 H1.

我相信解决此类问题的下一个“正确”方法是使用依赖模式匹配，如下所示：

Program Fixpoint pred (nat1: Nat) (H1: is_trim nat1 = True) (H2: is_pos nat1 H1 = True): Nat :=
  match nat1 as nat1' return is_pos nat1' H1 -> Nat with
  | Empt => fun isposEmpt =>
      (* hopefully, is_pos Empt H1 immediately reduces to False, and you can do this: *)
      False_rec Nat isposEmpt
  | Fill Zer nat2 => fun _ => Fill One (pred nat2 H1 H2)
  | Fill One nat2 => fun _ => Fill Zer nat2
  end H2.

也就是说，您需要证明 nat1 是肯定的作为匹配的参数，并且您在 Empt 情况下得出结论，证明是假的，因此您也可以返回假的。

希望这可行并且有意义。下次请提供必要的定义，以帮助人们使用您的示例。

于 2012-11-25T17:27:01.890 回答