Конгруэнтность для гетерогенного равенства

Я пытаюсь использовать гетерогенное равенство для доказательства утверждений, включающих этот индексированный тип данных:

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

Я смог написать свои доказательства, используя Relation.Binary.HeterogenousEquality.≅-Reasoning, но только при условии следующего свойства конгруэнтности:

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               k ≅ k′ → f k ≅ f k′
Counter-cong f k≅k′ = {!!}

Однако я не могу сопоставить шаблон k≅k′ с refl без получения следующего сообщения об ошибке от средства проверки типов:

Refuse to solve heterogeneous constraint 
    k : Counter n =?= k′ : Counter n′

и если я попытаюсь выполнить анализ случая для k≅k′ (т. е. используя C-c C-c из внешнего интерфейса Emacs), чтобы убедиться, что все неявные аргументы правильно сопоставлены с учетом их ограничений, наложенных refl, я получаю

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the 
inferred indices 
    [{.Level.zero}, {Counter n}, k] 
with the expected indices 
    [{.Level.zero}, {Counter n′}, k′]

(если вам интересно, вот некоторые не относящиеся к делу сведения: Устранение subst для доказательства равенства)


equality gadt proof agda
person Cactus    schedule 16.02.2012    source источник
comment
В качестве обходного пути я в настоящее время использую параметризованный тип вместо индексированного и вместо этого использую доказательство: data Counter (n : ℕ) : Set where cut : (i j : ℕ) → (i+j+1=n : suc (i + j) ≡ n) → Counter n   -  person Cactus    schedule 17.02.2012

Ответы (1)


arrow_upward
5
arrow_downward

Что вы можете сделать, так это взять дополнительное доказательство того, что два индекса равны:

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               n ≅ n′ → k ≅ k′ → f k ≅ f k′
Counter-cong f refl refl = refl

Исходная проблема заключается в том, что знание Counter n ≅ Counter n′ не подразумевает n ≡ n′, потому что конструкторы типов не предполагаются инъективными (для этого есть флаг --injective-type-constructors, который фактически заставляет совпадение пройти, но известно, что он несовместим с исключенным средним), поэтому в то время как он может сделать вывод, что два типа равны, он не будет переписывать n в n′, и поэтому вы получите эту ошибку, когда позже проверите, являются ли k и k′ унифицируемыми.

Поскольку Counter n состоит ровно из n элементов, на самом деле можно доказать, что Counter является инъективным, используя что-то вроде принципа сортировки (и, возможно, разрешимое равенство для натуральных чисел), поэтому вы могли бы обойтись без аргумента n ≅ n′, хотя это было бы быть грязным.

Редактировать: AFAICT the Het. поведение равенства остается прежним.

person Saizan    schedule 18.02.2012