Гипотеза универсальной количественной оценки в Coq

Я хочу изменить гипотезу 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

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

Я думаю, они оба могут решить одну и ту же задачу, но мне нужна гипотеза в более поздней форме. Или, точнее, дальнейшее разделение 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

universal quantifiers coq
person Khan    schedule 22.03.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Для этого вам нужно иметь в своем контексте термин 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 был специализирован и не может быть специализирован снова.

Вы не можете «получить» k и e из H, хотя это не имеет особого смысла для универсальной количественной оценки, так как это формальные параметры термина H (функция не передает свои аргументы, а запрашивает их в качестве входных данных).

Вы, должно быть, ошиблись с экзистенциальной квантификацией, где вы можете destruct выдвинуть гипотезу, чтобы получить свидетельство и доказательство того, что свидетельство удовлетворяет свойству.

person Ptival    schedule 23.03.2013
comment
Спасибо за ваш ответ. На самом деле у меня нет k и e в контексте. Я попробовал цель формы forall (k : RecType) (e : String.string), MapsTo k e (filter (is_vis_cookie l) mL) <-> MapsTo k e (filter (is_vis_cookie l) mR) с intros k e. (**теперь k и e находятся в контексте *), затем apply H, но затем k и e повторно объединяются... чего я не хочу... - person Khan; 26.03.2013
comment
То, что вы делаете, очень сбивает с толку и показывает, что вы действительно не понимаете, что происходит. Не могли бы вы, например, представить форму вашей фактической цели? - person Ptival; 26.03.2013
comment
Я не эксперт, мои вопросы могут раздражать. простите за это. Цель: StringMap.MapsTo zk zv (get_site_cookies (http_s_url p d ru) ckmL) <-> StringMap.MapsTo zk zv (get_site_cookies (http_s_url p d ru) ckmR), где zk и zv — строки ключ-значение, RecType — запись из пяти элементов (ключ — один из них), а get_site_cookies — свертка, где f работает только с 3 элементами RecType. MapsTo в H в сообщении выше — CookieMap.MapsTo... Может быть трудно понять типы/карты, однако я могу предоставить подробные типы/функции, если вам нужно. - person Khan; 02.04.2013
comment
Это нормально быть новичком. Просто попробуйте дать подробности, чтобы помочь людям помочь вам! Таким образом, кажется, что если вам нужно применить вашу гипотезу H, вы хотите использовать ее на zk и zv, используя что-то вроде specialize (H zk zv).. Однако это дает вам доказательство MapsTo zk zv (filter (is_vis_cookie l) mL) <-> MapsTo zk zv (filter (is_vis_cookie l) mR). Это все еще далеко от вашей цели (если mL и ckmL не совпадают, это может быть даже бесполезно). Поскольку get_site_cookies — это складка, вам, вероятно, понадобится доказательство по индукции. - person Ptival; 02.04.2013