Это правильный способ использовать HeterogeneEquality в Agda? - PullRequest
Новая
       9

Это правильный способ использовать HeterogeneEquality в Agda?

2 голосов
/ 27 февраля 2020

Код ниже отражает мой вопрос.

Мое намерение состоит в том, чтобы создать P из Vec N (suc n) из P из Vec N (n + 1). Мой опыт использования subst пропозиционального равенства говорит мне, что это должен быть способ сделать это. 

open import Relation.Binary.HeterogeneousEquality
postulate
  n : ℕ
  xs : Vec ℕ (n + 1)
  ys : Vec ℕ (suc n)
  eq : xs ≅ ys
data P : ∀ {n} → Vec ℕ n → Set where

lemma : P xs → P ys
lemma h = subst (λ i → P i) eq h

Очевидно, что лемма не проверяет тип, потому что (n + 1) и (su c n ) не одно и то же Nat.

Правильно ли я использую HeterogeneEquality? Если нет, то как правильно заменить Vec N (n+1) на Vec N (suc n)?

Ответы [ 2 ]

1 голос
/ 28 февраля 2020

Другое решение, основанное на переписывании. Обратите внимание, что вам нужно задать параметры постулата. 

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.HeterogeneousEquality

data P : ∀ {n} → Vec ℕ n → Set where

lemma :
  (n : ℕ)
  (xs : Vec ℕ (n + 1))
  (ys : Vec ℕ (suc n))
  (eq : xs ≅ ys)
   → P xs → P ys
lemma n xs ys eq h rewrite +-comm 1 n = subst (λ i → P i) eq h

Вы также можете избавиться от subst путем сопоставления зависимых паттернов: 

lemma n xs ys rewrite +-comm n 1 = \ { refl h -> h }
1 голос
/ 28 февраля 2020

Вот одно решение вашей проблемы: 

open import Data.Nat using (ℕ ; zero ; suc ; _+_)
open import Data.Product using (Σ-syntax ; _,_ ; proj₁ ; proj₂)
open import Data.Vec using (Vec)
open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_ ; refl)


n+1≡Sn : ∀ n → n + 1 ≡ suc n
n+1≡Sn zero = refl
n+1≡Sn (suc n) = ≡.cong suc (n+1≡Sn n)


isubst : ∀ {la lp lq} {A : Set la} {P : A → Set lp} (Q : ∀ a → P a → Set lq)
  → ∀ {a a′}
  → a ≡ a′
  → {p : P a} {p′ : P a′}
  → p ≅ p′
  → Q a p
  → Q a′ p′
isubst Q refl refl h = h


postulate
  n : ℕ
  xs : Vec ℕ (n + 1)
  ys : Vec ℕ (suc n)
  eq : xs ≅ ys
  P : ∀ n → Vec ℕ n → Set


lemma : P (n + 1) xs → P (suc n) ys
lemma h = isubst P (n+1≡Sn n) eq h

Хитрость (заключенная в isubst) заключается в том, что мы «объединяем» типы xs и ys перед тем, как устранить eq.

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

...