¿Cómo puedo utilizar la función “cong” e “injective” con vectores indexados en Idris?

15 Jul, 2023 Programación 0

cong y injective te permiten aplicar y deshacer funciones en igualdades:

cong : (f : a -> b) -> x = y -> f x = f y

injective : Injective f => f x = f y -> x = y

Ambas fallan para vectores indexados de diferentes longitudes, por razones obvias.

¿Cómo puedo demostrar que dos vectores iguales tienen la misma longitud? Es decir,

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

No puedo simplemente hacer

sameLen pf = cong length pf

porque length en xs tiene tipo Vect n a -> Nat y length en ys tiene tipo Vect m b -> Nat. (De hecho, ni siquiera estoy seguro de cómo probar lo mismo para dos List regulares, debido a los argumentos de tipo diferentes, mucho menos con los índices adicionales).

Yendo en la dirección opuesta, ¿cómo podría probar algo como

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

Nuevamente, no puedo simplemente hacer

unwrap pf = injective pf

debido a los tipos diferentes de T (uno con m y otro con n). Y incluso si tuviera una prueba de m = n, ¿cómo podría usarla para convencer a Idris de que las dos aplicaciones de T son iguales?

davy.ai

July 15, 2023 at 9:56 am

Para demostrar que dos vectores iguales tienen la misma longitud, podemos usar una combinación de cong y rewrite. Primero definimos una función lenEq: {n: Nat} -> {m: Nat} -> Vect n a -> Vect m b -> (n = m) -> Type que toma dos vectores y una prueba de que tienen la misma longitud, y devuelve un tipo. Este tipo estará habitado si y solo si los vectores tienen la misma longitud. Podemos definir lenEq de la siguiente manera:

lenEq: {n: Nat} -> {m: Nat} -> Vect n a -> Vect m b -> (n = m) -> Type
lenEq xs ys prf = if n == m then Vect n (xs = ys) else Void where
  n = length xs
  m = length ys

El bloque where calcula las longitudes de los vectores xs e ys y verifica si son iguales. Si lo son, entonces se devuelve Vect n (xs = ys), donde = es una igualdad a nivel de tipo. De lo contrario, se devuelve Void, lo que indica que los dos vectores tienen longitudes diferentes y no pueden ser iguales.

Ahora podemos definir sameLen en términos de lenEq:

sameLen: {xs: Vect n a} -> {ys: Vect m b} -> xs = ys -> n = m
sameLen pf = let prf = cong length pf in rewrite lenEq xs ys prf in Refl

Aquí aplicamos cong length a pf, lo que nos da una prueba de que las longitudes de xs e ys son iguales. Luego podemos usar rewrite para reemplazar el tipo n = length xs con m = length ys, utilizando lenEq xs ys (cong length pf) como la prueba de que estos tipos son iguales. Finalmente, se devuelve Refl como una prueba de que n y m son iguales.

Para demostrar unwrap, podemos usar el mismo enfoque. Primero definimos una función roseEq: {n: Nat} -> {m: Nat} -> Vect n (Rose a) -> Vect m (Rose b) -> (n = m) -> Type que toma dos vectores de Rose y una prueba de que tienen la misma longitud, y devuelve un tipo que indica si los vectores son iguales. Podemos definir roseEq de la siguiente manera:

roseEq: {n: Nat} -> {m: Nat} -> Vect n (Rose a) -> Vect m (Rose b) -> (n = m) -> Type
roseEq xs ys prf = if n == m then Vect n (xs = ys) else Void where
  n = length xs
  m = length ys

Ahora podemos definir unwrap en términos de roseEq:

unwrap: {xs: Vect n (Rose a)} -> {ys: Vect m (Rose b)} -> T xs = T ys -> xs = ys
unwrap pf = let prf = cong Vect.toList pf in
  let eqLen = sameLen prf in
  let xs' : Vect n (Rose a) = fromList xs eqLen in
  let ys' : Vect n (Rose b) = fromList ys eqLen in
  let eqVect: xs' = ys' = lenEq xs' ys' Refl in
  let eqRose = cong T eqVect in
  injective eqRose

Aquí primero usamos cong Vect.toList para obtener una prueba de que xs e ys tienen la misma longitud. Luego usamos sameLen para demostrar que las longitudes son iguales. Podemos usar fromList para convertir xs e ys en vectores de la misma longitud, y luego usar lenEq para demostrar que son iguales. Aplicamos cong T a esta prueba para obtener una prueba de que T xs' = T ys', y finalmente usamos injective para demostrar que xs' = ys'. Esto nos da una prueba de que xs e ys son iguales.

Answer

davy.ai

July 15, 2023 at 9:56 am
Para demostrar que dos vectores iguales tienen la misma longitud, podemos usar una combinación de cong y rewrite. Primero definimos una función lenEq: {n: Nat} -> {m: Nat} -> Vect n a -> Vect m b -> (n = m) -> Type que toma dos vectores y una prueba de que tienen la misma longitud, y devuelve un tipo. Este tipo estará habitado si y solo si los vectores tienen la misma longitud. Podemos definir lenEq de la siguiente manera:
```
lenEq: {n: Nat} -> {m: Nat} -> Vect n a -> Vect m b -> (n = m) -> Type
lenEq xs ys prf = if n == m then Vect n (xs = ys) else Void where
  n = length xs
  m = length ys
```
El bloque where calcula las longitudes de los vectores xs e ys y verifica si son iguales. Si lo son, entonces se devuelve Vect n (xs = ys), donde = es una igualdad a nivel de tipo. De lo contrario, se devuelve Void, lo que indica que los dos vectores tienen longitudes diferentes y no pueden ser iguales.

Ahora podemos definir sameLen en términos de lenEq:
```
sameLen: {xs: Vect n a} -> {ys: Vect m b} -> xs = ys -> n = m
sameLen pf = let prf = cong length pf in rewrite lenEq xs ys prf in Refl
```
Aquí aplicamos cong length a pf, lo que nos da una prueba de que las longitudes de xs e ys son iguales. Luego podemos usar rewrite para reemplazar el tipo n = length xs con m = length ys, utilizando lenEq xs ys (cong length pf) como la prueba de que estos tipos son iguales. Finalmente, se devuelve Refl como una prueba de que n y m son iguales.

Para demostrar unwrap, podemos usar el mismo enfoque. Primero definimos una función roseEq: {n: Nat} -> {m: Nat} -> Vect n (Rose a) -> Vect m (Rose b) -> (n = m) -> Type que toma dos vectores de Rose y una prueba de que tienen la misma longitud, y devuelve un tipo que indica si los vectores son iguales. Podemos definir roseEq de la siguiente manera:
```
roseEq: {n: Nat} -> {m: Nat} -> Vect n (Rose a) -> Vect m (Rose b) -> (n = m) -> Type
roseEq xs ys prf = if n == m then Vect n (xs = ys) else Void where
  n = length xs
  m = length ys
```
Ahora podemos definir unwrap en términos de roseEq:
```
unwrap: {xs: Vect n (Rose a)} -> {ys: Vect m (Rose b)} -> T xs = T ys -> xs = ys
unwrap pf = let prf = cong Vect.toList pf in
  let eqLen = sameLen prf in
  let xs' : Vect n (Rose a) = fromList xs eqLen in
  let ys' : Vect n (Rose b) = fromList ys eqLen in
  let eqVect: xs' = ys' = lenEq xs' ys' Refl in
  let eqRose = cong T eqVect in
  injective eqRose
```
Aquí primero usamos cong Vect.toList para obtener una prueba de que xs e ys tienen la misma longitud. Luego usamos sameLen para demostrar que las longitudes son iguales. Podemos usar fromList para convertir xs e ys en vectores de la misma longitud, y luego usar lenEq para demostrar que son iguales. Aplicamos cong T a esta prueba para obtener una prueba de que T xs' = T ys', y finalmente usamos injective para demostrar que xs' = ys'. Esto nos da una prueba de que xs e ys son iguales.

Comments are closed.

es.davy.ai

¿Tienes una pregunta?

¿Cómo puedo utilizar la función “cong” e “injective” con vectores indexados en Idris?

Answer

davy.ai