CODEWITHSUNDEEP
coquniversalquantifiers
Khan
Khan

Reputation: 303

Universal qauntification hypothesis in Coq

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

to

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

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

Upvotes: 0

Views: 247

Answers (1)

Ptival
Ptival

Reputation: 9437

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:

Using 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

Notice that you still have H available.

Using 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

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

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.

Upvotes: 3

Related Questions