Coq 中的通用量化假设

Question

我想从下面的表格中改变假设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

Answer 1

为此，您需要在上下文中有一个 k 类型的 RecType 和一个 e 类型的 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已经特化了，不能再特化了。

---

你不能从H“获得”k和e，但这对于通用量化没有多大意义，因为它们是术语H的形式参数（函数不携带它的参数，而是要求它们作为输入）。

你一定是对存在量化有误解，你可以destruct一个假设来获得证人以及证人满足属性的证明。