Relación 5

header {* 5ª relación de ejercicios *}

theory Relacion_5
imports Main 
begin

section {* Menor posición válida *}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función
     menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat"
  tal que (menorValida p xs) es el índice del primer elemento de una
  lista xs que satisface el predicado  p y es la longitud de xs si
  ningún elemento satisface el predicado p. Por ejemplo, 
     menorValida (λx. 4<x) [1::nat, 3, 5, 3, 1]     = 2
     menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1]     = 5
     menorValida (λx. 1<length x) [[], [1, 2], [3]] = 1
  --------------------------------------------------------------------- 
*}

primrec menorValida :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where
  "menorValida P [] = 0" 
  | "menorValida P (x#xs) = (if P x then 0 else ((menorValida P xs)+1))"


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar que menorValida devuelve la longitud de la
  lista syss ningún elemento satisface el predicado dado.
  --------------------------------------------------------------------- 
*}

lemma "menorValida (λx. 6<x) [1::nat, 3, 5, 3, 1] = 5"
by auto


text {* 
"Un comentario a la vista de esta propuesta: si lo que pide el enunciado 
es una demostración, considero que no basta con exhibir un ejemplo en el que  
el resultado se satisface."
*}



text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar si n es el valor de (menorValida P xs),
  entonces ninguno de los primeros n elementos de la lista xs verifica
  la propiedad P
  --------------------------------------------------------------------- 
*}

{* Una posible opcion inicial es poner un ejemplo en el que no se cumpla
e intentar sacar un contraejemplo
*}

lemma "menorValida (λx. 4<x) [1::nat, 2, 3, 4, 7] = 5"
by auto


text {* 
  --------------------------------------------------------------------- 
  Ejercicio 4. ¿Cómo se puede relacionar 
    "menorValida (λ x. P x ∨ Q x) xs" 
  con 
    "menorValida P xs" y "menorValida Q xs"? 
  ¿Se puede decir algo parecido con la conjunción de P y Q?  
  Prueba tus conjeturas.
  --------------------------------------------------------------------- 
*}

text {*
  La relación es la siguiente: La menor posición de los elementos que
  verifican la propiedad "P ∨ Q" es el mínimo de la menor posición de
  los elementos que verifican P y de la menor posición de los elementos
  que verifican Q.  
*}

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 5. Si P implica Q, ¿qué relación puede deducirse entre 
  "menorValida P xs" y "menorValida Q xs"?
  --------------------------------------------------------------------- 
*}

end