Coq中的通用量化假设

问题描述

我想从下面的表格中更改假设H

I want to change the hypothesis H from the form below

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

I think, they can both solve the same goal, but I need the hypothesis in the later form. Or more specifically, further separating k into its elements, like below. How can I change the hypotheses H to these two forms?

    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

推荐答案

为此，您需要在上下文中包含类型为RecType的术语k和类型为String.string的术语e >.这样，您可以获得:

To do this, you need to have in your context a term k of type RecType and a term of type e of type String.string. With this, you can obtain this:

使用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.

Notice that you still have H available.

使用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已被专门化，并且无法再次被专门化.

Notice that H has been specialized, and cannot be specialized again.

但是您不能从H中获取" k和e，这对于通用量化没有多大意义，因为这些是术语H的形式参数(一个函数不带有其参数) ，而是要求他们作为输入).

You cannot "obtain" k and e from H though, this does not make much sense for universal quantification, as these are formal parameters of the term H (a function does not carry its arguments, rather it asks for them as input).

您一定会误认为存在量化，您可以在其中量化假设以获得证人和证人满足财产的证明.

You must be mistaken with existential quantification, where you can destruct an hypothesis to obtain the witness and the proof that the witness satisfies the property.

这篇关于Coq中的通用量化假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！