Examen 2

chapter {* Examen de Lógica Matemática y Fundamentos (6 junio 2019) *}

text {*
  Nota: En las demostraciones se pueden  las reglas básicas de deducción
  natural de la lógica proposicional, de los cuantificadores y de la
  igualdad:  
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  · excluded_middle: (¬P ∨ P) 

  · allE:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allI:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ c = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y

  También se pueden usar las reglas notnotI y mt que demostramos a
  continuación. 
  *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. (2.5 puntos) Demostrar detalladamente que la siguiente
  fórmula es una tautología: 
     (p ⟶ q) ⟶((¬p ⟶ q) ⟶ q)

  Nota: No usar ninguno de los métodos automáticos: simp, simp_all, 
  auto, blast, force, fast, arith o metis
  ------------------------------------------------------------------ *}

(* La demostración declarativa es *)
lemma "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"  
proof
  assume "p ⟶ q"
  show "(¬p ⟶ q) ⟶ q"
  proof 
    assume "¬p ⟶ q"
    have "¬p ∨ p" by (rule excluded_middle)
    then show "q"
    proof (rule disjE)
      assume "¬p"
      with `¬p ⟶ q` show q by (rule mp)
    next
      assume "p"
      with `p ⟶ q` show q by (rule mp)
    qed
  qed 
qed

(* Una demostración aplicativa es *)
lemma "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"
  apply (rule impI)+
     (* ⟦p ⟶ q; ¬ p ⟶ q⟧ ⟹ q *)
  apply (cut_tac P=p in excluded_middle)
     (* ⟦p ⟶ q; ¬ p ⟶ q; ¬ p ∨ p⟧ ⟹ q *)
  apply (erule disjE)
     (* 1. ⟦p ⟶ q; ¬ p ⟶ q; ¬ p⟧ ⟹ q
        2. ⟦p ⟶ q; ¬ p ⟶ q; p⟧ ⟹ q *)
   apply (erule_tac P="¬p" in mp)
     (* 1. ⟦p ⟶ q; ¬ p⟧ ⟹ ¬ p
        2. ⟦p ⟶ q; ¬ p ⟶ q; p⟧ ⟹ q *)
   apply assumption
     (* ⟦p ⟶ q; ¬ p ⟶ q; p⟧ ⟹ q *)
  apply (erule mp)
     (* ⟦¬ p ⟶ q; p⟧ ⟹ p *)
  apply assumption
     (* *)
  done

(* Otra demostración aplicativa es *)
lemma "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"
  apply (rule impI)+
     (* ⟦p ⟶ q; ¬ p ⟶ q⟧ ⟹ q *)
  apply (rule ccontr)
     (* ⟦p ⟶ q; ¬ p ⟶ q; ¬ q⟧ ⟹ False *)
  apply (drule_tac G=q in mt)
     (* 1. ⟦¬ p ⟶ q; ¬ q⟧ ⟹ ¬ q
        2. ⟦¬ p ⟶ q; ¬ q; ¬ p⟧ ⟹ False *)
   apply assumption
     (* ⟦¬ p ⟶ q; ¬ q; ¬ p⟧ ⟹ False *)
  apply (erule notE)
     (* ⟦¬ p ⟶ q; ¬ p⟧ ⟹ q *)
  apply (erule mp)
     (* ¬ p ⟹ ¬ p *)
  apply assumption
     (* *)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 2. (2.5 puntos) Demostrar detalladamente que si R es una
  relación irreflexiva y transitiva, entonces R es antisimétrica. 
  { ∀x. ¬R(x,x), 
    ∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z)) } 
  ⊢  ∀x. ∀y. (R(x,y) ⟶ ¬R(y,x))

  Nota: No usar ninguno de los métodos automáticos: simp, simp_all, 
  auto, blast, force, fast, arith o metis
  ------------------------------------------------------------------ *}

(* La demostración declarativa es *)
lemma
  assumes "∀x. ¬R(x,x)"
          "∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))" 
  shows   "∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"
proof 
  fix a
  show "∀y. (R(a,y) ⟶ ¬R(y,a))"
  proof
   fix b
   show "R(a,b) ⟶ ¬R(b,a)"
   proof
     assume "R(a,b)"
     show "¬ R(b,a)"
     proof
       assume "R(b,a)"
       then have "R(b,a) ∧ R(a,b)" using `R(a,b)` by (rule conjI)
       have "∀y. ∀z.(R(b,y) ∧ R(y,z) ⟶ R(b,z))" 
         using assms(2) by (rule allE)
       then have "∀z.(R(b,a) ∧ R(a,z) ⟶ R(b,z))" by (rule allE)
       then have "R(b,a) ∧ R(a,b) ⟶ R(b,b)" by (rule allE)
       then have "R(b,b)" using `R(b,a) ∧ R(a,b)` by (rule mp)
       have "¬R(b,b)" using assms(1) by (rule allE)
       then show False using `R(b,b)` by (rule notE)
     qed
   qed
 qed
qed

(* La demostración aplicativa es *)
lemma 
  "⟦ ∀x. ¬R(x,x);
     ∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))⟧
   ⟹ ∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"   
  apply (rule allI)+
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ R (x, y) ⟶ ¬ R (y, x)*)
  apply (rule impI)
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y)⟧
               ⟹ ¬ R (y, x) *)
    apply (rule notI)
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y); 
                 R (y, x)⟧
               ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y); 
                 R (y, x); 
                 ¬ R (x, x)⟧
           ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 ∀y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ False *)
  apply (erule_tac x=y in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 ∀z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
               ⟹ False *)
  apply (erule notE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x);
                 R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
               ⟹ R (x, x) *)
  apply (drule mp)
      (* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y) ∧ R (y, x)
         2. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x) *)
    apply (rule conjI)
      (* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y)
         2. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (y, x)
         3. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x)*)
    apply assumption+
      (* *)
  done  

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3 (2.5 puntos) Consideremos el árbol binario definido por
     datatype 'a arbol = H  | N "'a" "'a arbol" "'a arbol"
  
  Por ejemplo, el árbol
          e
         / \
        /   \
       c     g
      / \   / \
             
  se representa por "N e (N c H H) (N g H H)".

  Definir las funciones 
     nNodos :: "'a arbol ⇒ nat"
     nHojas :: "'a arbol ⇒ nat" 
  tales que 
  + (nNodos a) es el número de nodos de a. Por ejemplo,
       nNodos (N e (N c H H) (N g H H)) = 3
  + (nHojas a) es el número de hojas de a. Por ejemplo,
       nHojas (N e (N c H H) (N g H H)) = 4

  Demostrar detalladamente que el número de hojas de un árbol es igual 
  al número de nodos más 1.

  Nota: Los únicos métodos que se pueden usar son induct, 
  (simp only: ...) o this.
  ------------------------------------------------------------------- *}

datatype 'a arbol = H  | N "'a" "'a arbol" "'a arbol"

fun nNodos :: "'a arbol ⇒ nat" where
  "nNodos H         = 0"
| "nNodos (N x i d) = 1 + (nNodos i) + (nNodos d)"

fun nHojas :: "'a arbol ⇒ nat" where
  "nHojas H         = 1"
| "nHojas (N x i d) = (nHojas i) + (nHojas d)"

(* Demostración declarativa *)
lemma "nHojas a = (nNodos a) + 1" (is "?P a")
proof (induct a)
  show "?P H" by (simp only: nHojas.simps(1) nNodos.simps(1)) 
next
  fix x i d
  assume HI1: "?P i"
  assume HI2: "?P d"
  show "?P (N x i d)" 
  proof -
    have "nHojas (N x i d) = (nHojas i) + (nHojas d)" 
      by (simp only: nHojas.simps(2))
    also have "... = (nNodos i + 1) + (nNodos d + 1)" 
      by (simp only: HI1 HI2)
    also have "... = (nNodos (N x i d)) + 1" 
      by (simp only: nNodos.simps(2))
    finally show "?P (N x i d)" by this
  qed
qed

(* Demostración aplicativa *)
lemma "nHojas a = (nNodos a) + 1"  
  apply (induct a)
     (* 1. nHojas H = nNodos H + 1
        2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                        nHojas a2 = nNodos a2 + 1⟧
                      ⟹ nHojas (N x1 a1 a2) = 
                          nNodos (N x1 a1 a2) + 1 *)
   apply (simp only: nHojas.simps(1)) 
     (* 1. 1 = nNodos H + 1
        2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                        nHojas a2 = nNodos a2 + 1⟧
                      ⟹ nHojas (N x1 a1 a2) = nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nNodos.simps(1))
     (* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                     nHojas a2 = nNodos a2 + 1⟧
                   ⟹ nHojas (N x1 a1 a2) = 
                       nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nHojas.simps(2))
     (* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
                     nHojas a2 = nNodos a2 + 1⟧
                   ⟹ nNodos a1 + 1 + (nNodos a2 + 1) = 
                       nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nNodos.simps(2))
     (* *)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 4. (2.5 puntos) Sea G un grupo. Domostrar detalladamente que 
  para todo par de elementos x e y de G, si x es el inverso de y, 
  entonces y es el inverso de x.

  Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
  fast, arith o metis 
  ------------------------------------------------------------------ *}

locale grupo =
  fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
    and neutro ("𝟭") 
    and inverso ("_^" [100] 100)
  assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
      and neutro_i:   "𝟭 ⋅ x = x"
      and neutro_d:   "x ⋅ 𝟭 = x"
      and inverso_i:  "x^ ⋅ x = 𝟭"

(* Notas sobre notación:
   * El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos). 
   * El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
   * El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)

context grupo
begin

(* Una demostración declarativa es *)
lemma "∀x. ∀y. x = y^ ⟶ y = x^" 
proof (rule allI)+
  fix a b
  show "a = b^ ⟶ b = a^"
  proof 
    assume "a = b^"
    then have "a^ ⋅ a = a^ ⋅ b^" by simp
    then have "𝟭 = a^ ⋅ b^" by (simp only: inverso_i)
    then have "𝟭 ⋅ b = (a^ ⋅ b^) ⋅ b" by simp
    then have "b = (a^ ⋅ b^) ⋅ b" by (simp only: neutro_i)
    then have "b = a^ ⋅ (b^ ⋅ b)" by (simp only: asociativa)
    then have "b = a^ ⋅ 𝟭" by (simp only: inverso_i)
    then show "b = a^ " by (simp only: neutro_d)
  qed
qed

(* Otra demostración declarativa es *)
lemma "∀x. ∀y. x = y^ ⟶ y = x^" 
proof (rule allI)+
  fix a b
  show "a = b^ ⟶ b = a^"
  proof 
    assume "a = b^"
    show "b = a^"
    proof -
      have "b = 𝟭 ⋅ b" by (simp only: neutro_i)
      also have "… = (a^ ⋅ a) ⋅ b" by (simp only: inverso_i)
      also have "… = a^ ⋅ (a ⋅ b)" by (simp only: asociativa)
      also have "… = a^ ⋅ (b^ ⋅ b)" using `a = b^`  by simp
      also have "… = a^ ⋅ 𝟭" by (simp only: inverso_i)
      also have "… = a^" by (simp only: neutro_d)
      finally show "b = a^" by this
    qed 
  qed
qed

end

end