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 更改为这两种形式？

    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

为此，您需要在上下文中有一个ktypeRecType的 term 和一个etype的 term String.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 回答