2

我有一个证据，在我的假设中我有：

...
l0 : list
         (list (ATrs.rule (Sig a)) * boolean * option (list positiveInteger) *
          option cpf.dpProof)
H: forall
         x : list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) *
             option cpf.dpProof,
       In x l0 ->
       (let (p, o) := x in
        let (p0, _) := p in
        let (dps, b) := p0 in
        if b
        then
         match o with
         | Some pi => bool_of_result (dpProof n R dps pi)
         | None => false
         end
        else co_scc (dpg_unif_N 100 R D) dps) = true
 ci : list (ATrs.rule (Sig a))
 Hin : In ci l1
===========================
....

我被困在打破假设的技术上H。如果我有论据x:list (ATrs.rule (Sig a)) * bool * option (list positiveInteger) * option cpf.dpProof和假设，Hx: In x l0那么我可以使用策略：ded (H x Hx)获取(let (p, ...).H

所以在这种情况下我不能使用ded (H ci Hin)，因为ci类型与xin不同H。

我想知道如何添加我想要的假设（x和Hx）？

非常感谢您的帮助。

4

1 回答 1

1

好吧，除非您的上下文包含有关 的更多信息，否则您l0将永远无法从 中推断出任何内容H，因为其中一个参数的类型In x l0为 some x。

如果l0在您的上下文和目标中完全不受限制，它实际上可以是任何适当类型的任意列表，因此您无法伪造 type 的东西In x l0，因此无法使用H.

也许你在某个地方有矛盾，或者用另一种方式来攻击这个证明。

于 2013-01-08T07:44:43.620 回答