Использование обратного значения инъективной функции - PullRequest
Новая
       26

Использование обратного значения инъективной функции

2 голосов
/ 29 марта 2020

Я пытаюсь доказать эту лемму: 

lemma 
  assumes "x = inv f y" and "inj f" and "x ≠ undefined"
  shows "y ∈ range f"
  using assms try

Но Нитпик говорит мне, что это утверждение неверно: 

Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"... 
Nitpick found a counterexample for card 'b = 3
and card 'a = 2:

  Free variables:
    f = (λx. _)(a1 := b1, a2 := b2)
    x = a2
    y = b3

Контрпример Нитпика предполагает, что y = b3 не в диапазон f. Но в таком случае, как может существовать x = inv f b3, который не является неопределенным?

Ответы [ 2 ]

3 голосов
/ 29 марта 2020

peq уже дал хороший ответ. Однако я хотел бы сделать несколько дополнительных замечаний, которые могут оказаться полезными для вас (т. Е. Это не ответ, а дополнение к ответу peq).

Как правило, мне известны два встроенных удобства в Изабель / HOL для имитации (технически, f::'a=>'b всегда будет целой функцией с доменом UNIV::'a set) функций с ограниченным доменом / доменом:

  • Инструменты в теории Map, которые являются доступно из теории Main. Эти инструменты могут дополнить предложение peq для работы с конструктором типов option.
  • Инструменты в HOL-Library.FuncSet. Эти инструменты были разработаны вокруг идеи использования undefined для «ограничения» области / диапазона функции.

Следуя второму предложению использовать, например, HOL-Library.FuncSet, вы можете «ограничить» inv диапазоном функции. В этом случае сформулированная вами теорема может быть доказана под ограниченным обратным: 

theory Scratch
  imports 
    Main
    "HOL-Library.FuncSet"
begin

abbreviation inv' where "inv' f ≡ restrict (inv f) (range f)"

lemma 
  assumes "x = inv' f y" and "inj f" and "x ≠ undefined"
  shows "y ∈ range f"
  using assms unfolding restrict_def by meson

end

Заметьте, однако, что приведенная выше теорема все еще не очень полезна, так как она неявным образом исключает возможность того, что undefined = inv' f y когда y находится в диапазоне f.

Попробовав оба набора инструментов, о которых я упоминал выше, мое личное мнение (не то, чтобы вы предполагали, что он имеет какой-либо вес) состоит в том, что зачастую самым простым и наиболее естественным решением является не используйте их и просто предоставьте дополнительные допущения, которые указывают, что набор (или конкретные значения), на которые должна воздействовать функция или ее обратное, находятся в (желаемой) области / диапазоне функции.

3 голосов
/ 29 марта 2020

Значение undefined является произвольным неизвестным значением. Вы не можете использовать его, проверьте, что результат функции не определен. Все функции в Изабель являются общими.

Если y не находится в диапазоне f, тогда inv f y может принимать любое значение.

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

...