Buenas tengo unas dudas en cuanto a sintaxis y semantica para los temas del practico 4 y 5.
La primera es, referida al practico 4, ejercicio 1, parte 4, igualdad de lista:
Inductive eq_list (A:Set) : list A -> list A -> Prop :=
| eq_nil : eq_list A (nil A) (nil A)
| eq_cons : forall (m n: list A) (a b: A), eq_list A m n -> eq_list A (cons A a m) (cons A b n).
para este caso, tengo la duda porque yo lo pense como que los elementos que se agregan para las listas m y n pueden ser distintos y aun asi mantener el largo de la lista, pero tambien podria ser que el caso eq_cons sea: forall (m n : list A), ( a: A), eq_list A m n -> eq_list A (cons A a m) (cons A a n) .
En estos casos cual sería la solución correcta?
Luego para el practico 5 ejercicio 3, la definicion inductiva de MemL, nosotros lo pensamos de la siguiente forma:
Inductive MemL (a : A) : List -> Prop :=
| hereL : forall x : List, MemL a (consL a x)
| thereL : forall x : List, MemL a x -> forall b : A, MemL a (consL b x).
para el constructor thereL, es lo mismo poner el forall b: A antes del -> ? Es decir:
| thereL : forall (x : List) (b : A), MemL a x -> MemL a (consL b x).
Creo que esta forma facilita las demostraciones, pero no se si hay una sintaxis correcta para estos casos
Saludos!