0

仮説Hを以下のフォームから変更したい

mL : Map
mR : Map
H : forall (k : RecType) (e : String.string),
       MapsTo k e (filter (is_vis_cookie l) mL) <->
       MapsTo k e (filter (is_vis_cookie l) mR)
-------------------------------------------------------
Goal

に

mL : Map
mR : Map
k : RecType
e : String.string
H : MapsTo k e (filter (is_vis_cookie l) mL) <->
    MapsTo k e (filter (is_vis_cookie l) mR)
-------------------------------------------------------
Goal

どちらも同じ目標を解決できると思いますが、後者の形式の仮説が必要です。または、より具体的には、以下のように、さらに k をその要素に分離します。仮説Hをこれら2つの形式に変更するにはどうすればよいですか?

    mL : Map
    mR : Map
    ks : String.string
    kh : String.string
    e : String.string
    H : MapsTo {| elem1:= ks; elem2:= kh|} e (filter (is_vis_cookie l) mL) <->
        MapsTo {| elem1:= ks; elem2:= kh|} e (filter (is_vis_cookie l) mR)
    -------------------------------------------------------
    Goal
4

1 に答える 1

3

これを行うには、コンテキスト内に typeの用語とktypeの用語が必要です。これにより、これを取得できます。RecTypeeString.string

使用pose proof (H k e) as Hke:

mL : Map
mR : Map
k : RecType
e : String.string
H : forall (k : RecType) (e : String.string),
    MapsTo k e (filter (is_vis_cookie l) mL) <->
    MapsTo k e (filter (is_vis_cookie l) mR)
Hke : MapsTo k e (filter (is_vis_cookie l) mL) <->
      MapsTo k e (filter (is_vis_cookie l) mR)
-------------------------------------------------------
Goal

H がまだ利用可能であることに注意してください。

使用specialize (H k e).:

mL : Map
mR : Map
k : RecType
e : String.string
H : MapsTo k e (filter (is_vis_cookie l) mL) <->
    MapsTo k e (filter (is_vis_cookie l) mR)
-------------------------------------------------------
Goal

H は特化されており、再度特化することはできないことに注意してください。

「取得」することはできませんが、これらは用語の形式k的なパラメーターであるため、これは全称量化にはあまり意味がありません (関数は引数を持たず、入力として要求します)。eHH

destruct証人を得る仮説と、証人がプロパティを満たすという証明を得ることができる存在量化と誤解されているに違いありません。

于 2013-03-23T00:25:39.807 に答える