重写相关函数

我想为二进制自然数（位列表）定义前驱函数。我想限制我的函数输入到被修剪的数字（没有前导零）并且是正数（所以，我不必担心零的前任）。重写相关函数

这是运营商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。

我该如何证明这一点？

来源

2012-11-24 user1494846

另外，'dependent-types'应该是一个标签。 – user1494846

'dependent-type'（单数）是一个标签。 – sepp2k

我刚刚注意到这个目标是“微不足道的”。（-_-'）不过，我想知道如何通过手工解决它，以防我陷入类似但更复杂的情况。 – user1494846

这个目标确实微不足道，因为您可以返回任何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-25 17:27:01 Ptival

重写相关函数

回答

相关问题