Как улучшить эту функцию Agda со стандартными библиотеками? - PullRequest
Новая
       9

Как улучшить эту функцию Agda со стандартными библиотеками?

0 голосов
/ 06 сентября 2018

Приведенная ниже функция deq возвращает экземпляр Dec для Name, который либо содержит строку, либо префикс Name одним из двух конструкторов. 

data Name : Set where
  Str : String -> Name
  Cp0 : Name -> Name
  Cp1 : Name -> Name

deq : (a : Name) -> (b : Name) -> Dec (a ≡ b)
deq (Str a) (Str b) with iseq a b
deq (Str a) (Str b) | yes p = yes (cong Str p)
deq (Str a) (Str b) | no ¬p = no f
  where f : (Str a ≡ Str b) -> ⊥
        f refl = ¬p refl
deq (Str a) (Cp0 b) = no (λ ())
deq (Str a) (Cp1 b) = no (λ ())
deq (Cp0 a) (Str b) = no (λ ())
deq (Cp0 a) (Cp0 b) with deq a b
deq (Cp0 a) (Cp0 b) | yes p = yes (cong Cp0 p)
deq (Cp0 a) (Cp0 b) | no ¬p = no f
  where f : (Cp0 a ≡ Cp0 b) -> ⊥
        f refl = ¬p refl
deq (Cp0 a) (Cp1 b) = no (λ ())
deq (Cp1 a) (Str b) = no (λ ())
deq (Cp1 a) (Cp0 b) = no (λ ())
deq (Cp1 a) (Cp1 b) with deq a b
deq (Cp1 a) (Cp1 b) | yes p = yes (cong Cp1 p)
deq (Cp1 a) (Cp1 b) | no ¬p = no f
  where f : (Cp1 a ≡ Cp1 b) -> ⊥
        f refl = ¬p refl

Но здесь несколько пунктов неудобны, потому что им нужен where. Если бы у стандартной библиотеки был cong эквивалент, который позволил нам превратить a ≡ b -> ⊥ в F a ≡ F b -> ⊥ для конструктора F, тогда мы могли бы сделать это определение короче. Кроме того, если бы мы могли сделать сопоставление с шаблоном, встроенное с лямбдами, мы могли бы также улучшить его, но для этого нам нужно было бы аннотировать ввод лямбда-типа с типом. Есть ли способ улучшить это определение?

...