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)ため、使用できません。cixH

x必要な仮説 (および)を追加するにはどうすればよいHxですか?

ご助力ありがとうございます。

4

1 に答える 1

1

コンテキストに に関する詳細情報が含まれていない限り、引数の 1 つに の型があるため、 からl0何かを推測することはできません。HIn x l0x

がコンテキストと目標で完全に制約されていない場合l0、事実上、適切なタイプの任意のリストになる可能性があるため、 type の何かを偽造する方法はなくIn x l0、したがって を使用することは不可能Hです。

どこかに矛盾があるか、この証明を攻撃する別の方法があるかもしれません。

于 2013-01-08T07:44:43.620 に答える