`with fx` соответствует` false`, но не может создать `fx == false` - PullRequest
Новая
       6

`with fx` соответствует` false`, но не может создать `fx == false`

0 голосов
/ 05 ноября 2019

Кусок кода здесь: 

-- transitivity
trans : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl

union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
                           (ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' m n x with ismember m x | ismember n x | ismember (set-union (set-pair m n)) x
union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
                       (ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' m n x with ismember m x | ismember n x | ismember (set-union (set-pair m n)) x
...                  | false | false | false = trans {x = ismember (set-union (set-pair m n)) x} {y = false}
                                                     refl -- line #102
                                                     (union-match m n x)
-- more code available on request, although I can't see why that would matter

выдает ошибку: 

code.agda:102,54-58
(ismember (set-union (set-pair m n)) x) != false of type Bool
when checking that the expression refl has type
ismember (set-union (set-pair m n)) x == false

У меня есть with утверждение, которое точно устанавливает тот факт, что ismember (set-union (set-pair m n)) xfalse. Почему он не может установить, что это false?

Хорошо, я даже могу видеть некоторые известные проблемы https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#ill-typed-with-abstractions, но все же не знаю, как сопоставить паттерн тогда.

1 Ответ

3 голосов
/ 06 ноября 2019

Похоже, вам нужно помнить тот факт, что следующее выражение 

ismember (set-union (set-pair m n)) x

действительно равно 

false

Это очень распространенная проблема, возникающая из«с» строительные работы. По умолчанию у вас нет доступа к элементу доказательства, который связывает элемент, с которым сопоставляется шаблон, с результатом сопоставления с шаблоном, то есть в вашем примере это элемент типа: 

ismember (set-union (set-pair m n)) x == false

Чтобы получить элемент этого типа, вам нужно использовать идиому «осмотра», который определен наряду с пропозициональным равенством в стандартной библиотеке. Более конкретно, это означает, что вам нужно будет добавить новый элемент в сопоставление с образцом следующим образом: 

... | ismember (set-union (set-pair m n)) x | inspect (ismember (set-union (set-pair m n)) x

Это приведет к тому, что вы получите доступ как к «ложному», так и к требуемому элементу доказательства. Для получения дополнительной информации об идиоме осмотра см .:

  • Вики-страница на with-abtraction: https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html
  • Файл PropositionalEquality.agda в стандартной библиотеке, который предоставляетидиома, а также краткое описание того, как его использовать
  • Файл README / Inspect.agda в стандартной библиотеке, а также полный пример того, как и когда использовать инспекцию идиома
...