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

要做到这一点，您需要在您的上下文中具有类型为RecType的k和类型为String.string的e的术语。使用此命令，您可以获得以下内容:

---

使用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一个假设来获得证人，并证明证人满足属性。