Блог

cong и injective позволяют применять и не применять функции к равенствам:

 cong : (f : a -gt; b) -gt; x = y -gt; f x = f y  injective : Injective f =gt; f x = f y -gt; x = y  

Оба они не работают для индексированных векторов разной длины по очевидным причинам.

Как я могу доказать, что два равных вектора имеют одинаковую длину? Т. Е.

 sameLen : {xs : Vect n a} -gt; {ys : Vect m b} -gt; xs = ys -gt; n = m  

Я не могу просто сделать

 sameLen pf = cong length pf  

потому length что у on xs есть тип Vect n a -gt; Nat и length у on ys есть тип Vect m b -gt; Nat . (На самом деле, я даже не уверен, как доказать одно и то же для двух обычных List s, из-за разных аргументов типа, не говоря уже о добавленных индексах).

Идя другим путем, как бы я доказал что-то вроде

 data Rose a = V a | T (Vect n (Rose a)) Injective T where  injective Refl = Refl unwrap : {xs : Vect n (Rose a)} -gt; {ys : Vect m (Rose b)} -gt; T xs = T ys -gt; xs = ys  

Опять же, я не могу просто сделать

 unwrap pf = injective pf  

из-за различных типов T (один с m и один с n). И даже если бы у меня было доказательство m=n , как я мог бы использовать его, чтобы убедить Идриса в том, что два применения T одного и того же?

Получил ответ от Idris Discord — если вы соответствуете шаблону Refl , то он объединяется a и b автоматически:

 sameLen : {xs : List a} -gt; {ys : List b} -gt; xs = ys -gt; length xs = length ys sameLen Refl = Refl  sameLen' : {xs : Vect n a} -gt; {ys : Vect m b} -gt; xs = ys -gt; n = m sameLen' Refl = Refl