Используете rewrite для моего собственного равенства?

У меня есть следующее определение равенства:

data Equal : x -> y -> Type where
    Reflexive : Equal a a

Когда я хочу использовать синтаксис rewrite, мне нужно что-то типа (a = b), поэтому я создал:

makeEquitable : Equal x y -> x = y
makeEquitable Reflexive = Refl

Теперь я могу делать makeEquitable (_ : Equal a b), которые затем могу использовать для rewrite вещей. Я хотел бы упростить это, и я изучил replace, который я действительно не понимаю replace : (x = y) -> P x -> P y. Я полагаю, что эта P вещь является встроенным свойством Идриса - как мне сделать такую ​​функцию для моего собственного определения Equality - можно ли также «встроить» что-то особенное, чтобы rewrite волшебным образом работало для Equal a b?


idris
person ScarletAmaranth    schedule 24.03.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Если вы установите :set showimplicits в ответе, вы увидите неявные аргументы для :t replace:

replace : {a : Type} -> {x : a} -> {y : a} -> {P : a -> Type} ->
          ((=) {A = a} {B = a} x y) -> P x -> P y

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

replaceEqual : {P : a -> Type} -> Equal x y -> P x -> P y
replaceEqual Reflexive prf = prf

Но насколько мне известно, вы не сможете легко сделать свой собственный rewrite. Однако вы можете использовать правило синтаксиса, чтобы усовершенствовать свой подход:

syntax eqrewrite [a] "in" [b] = rewrite makeEquitable a in b;

plus_commutes_Z' : Equal m (plus m 0)
plus_commutes_Z' {m = Z} = Reflexive
plus_commutes_Z' {m = (S k)} =
  let rec = plus_commutes_Z' {m=k}
  in eqrewrite rec in Reflexive
person xash    schedule 24.03.2016