Theory Pelletier

(*
  File: Pelletier.thy
  Author: Bohua Zhan

  Pelletier's problems. From the paper "Seventy-five problems for testing
  automatic theorem provers" by Francis Jeffry Pelletier.
*)

section ‹Pelletier's problems›

theory Pelletier
  imports Logic_Thms
begin

theorem p1: "(p ⟶ q) ⟷ (¬q ⟶ ¬p)" by auto2

theorem p2: "(¬¬p) ⟷ p" by auto2

theorem p3: "¬(p ⟶ q) ⟹ q ⟶ p" by auto2

theorem p4: "(¬p ⟶ q) ⟷ (¬q ⟶ p)" by auto2

theorem p5: "(p ∨ q) ⟶ (p ∨ r) ⟹ p ∨ (q ⟶ r)" by auto2

theorem p6: "p ∨ ¬p" by auto2

theorem p7: "p ∨ ¬¬¬p" by auto2

theorem p8: "((p ⟶ q) ⟶ p) ⟹ p" by auto2

theorem p9: "(p ∨ q) ∧ (¬p ∨ q) ∧ (p ∨ ¬q) ⟹ ¬(¬p ∨ ¬q)" by auto2

theorem p10: "q ⟶ r ⟹ r ⟶ p ∧ q ⟹ p ⟶ q ∨ r ⟹ p ⟷ q" by auto2

theorem p11: "p ⟷ p" by auto2

theorem p12: "((p ⟷ q) ⟷ r) ⟷ (p ⟷ (q ⟷ r))"
@proof
  @case "p"
  @case "q"
@qed

theorem p13: "p ∨ (q ∧ r) ⟷ (p ∨ q) ∧ (p ∨ r)" by auto2

theorem p14: "(p ⟷ q) ⟷ ((q ∨ ¬p) ∧ (¬q ∨ p))" by auto2

theorem p15: "(p ⟶ q) ⟷ (¬p ∨ q)" by auto2

theorem p16: "(p ⟶ q) ∨ (q ⟶ p)" by auto2

theorem p17: "(p ∧ (q ⟶ r) ⟶ s) ⟷ (¬p ∨ q ∨ s) ∧ (¬p ∨ ¬r ∨ s)" by auto2

theorem p18: "∃y::'a. ∀x. F(y) ⟶ F(x)"
@proof
  @case "∀x. F(x)" @with
    @obtain "y::'a" where "y = y" @have "∀x. F(y) ⟶ F(x)"
  @end
  @obtain y where "¬F(y)" @have "∀x. F(y) ⟶ F(x)"
@qed

theorem p19: "∃x::'a. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x))"
@proof
  @case "∃x. P(x) ⟶ Q(x)" @with
    @obtain x where "P(x) ⟶ Q(x)"
    @have "∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x))"
  @end
  @obtain "x::'a" where "x = x"
  @have "∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x))"
@qed

theorem p20: "∀x y. ∃z. ∀w. P(x) ∧ Q(y) ⟶ R(z) ∧ S(w) ⟹
  ∃x y. P(x) ∧ Q(y) ⟹ ∃z. R(z)"
@proof
  @obtain x y where "P(x)" "Q(y)"
  @obtain z where "∀w. P(x) ∧ Q(y) ⟶ R(z) ∧ S(w)"
@qed

theorem p21: "∃x. p ⟶ F(x) ⟹ ∃x. F(x) ⟶ p ⟹ ∃x. p ⟷ F(x)"
@proof
  @case "p" @with @obtain x where "F(x)" @have "p ⟷ F(x)" @end
  @case "¬p" @with @obtain x where "¬F(x)" @have "p ⟷ F(x)" @end
@qed

theorem p22: "∀x::'a. p ⟷ F(x) ⟹ p ⟷ (∀x. F(x))"
@proof
  @case "p" @obtain "x::'a" where "x = x"
@qed

theorem p23: "(∀x::'a. p ∨ F(x)) ⟷ (p ∨ (∀x. F(x)))" by auto2

theorem p29: "∃x. F(x) ⟹ ∃x. G(x) ⟹
  ((∀x. F(x) ⟶ H(x)) ∧ (∀x. G(x) ⟶ J(x))) ⟷
  (∀x y. F(x) ∧ G(y) ⟶ H(x) ∧ J(y))"
@proof
  @obtain a b where "F(a)" "G(b)"
  @case "∀x y. F(x) ∧ G(y) ⟶ H(x) ∧ J(y)" @with
    @have "∀x. F(x) ⟶ H(x)" @with @have "F(x) ∧ G(b)" @end
    @have "∀y. G(y) ⟶ J(y)" @with @have "F(a) ∧ G(y)" @end
  @end
@qed

theorem p30: "∀x. F(x) ∨ G(x) ⟶ ¬H(x) ⟹
  ∀x. (G(x) ⟶ ¬I(x)) ⟶ F(x) ∧ H(x) ⟹ ∀x. I(x)"
@proof
  @have "∀x. I(x)" @with @case "F(x)" @end
@qed

theorem p31: "¬(∃x. F(x) ∧ (G(x) ∨ H(x))) ⟹ ∃x. I(x) ∧ F(x) ⟹ ∀x. ¬H(x) ⟶ J(x) ⟹
  ∃x. I(x) ∧ J(x)" by auto2

theorem p32: "∀x. (F(x) ∧ (G(x) ∨ H(x))) ⟶ I(x) ⟹ ∀x. I(x) ∧ H(x) ⟶ J(x) ⟹
  ∀x. K(x) ⟶ H(x) ⟹ ∀x. F(x) ∧ K(x) ⟶ J(x)" by auto2

theorem p33: "(∀x. p(a) ∧ (p(x) ⟶ p(b)) ⟶ p(c)) ⟷
  (∀x. (¬p(a) ∨ p(x) ∨ p(c)) ∧ (¬p(a) ∨ ¬p(b) ∨ p(c)))" by auto2

theorem p35: "∃(x::'a) (y::'b). P(x,y) ⟶ (∀x y. P(x,y))" by auto2

theorem p39: "¬(∃x. ∀y. F(y,x) ⟷ ¬F(y,y))"
@proof
  @contradiction
  @obtain x where "∀y. F(y,x) ⟷ ¬F(y,y)"
  @case "F(x,x)"
@qed

(* Note there is a typo in the original text. *)
theorem p40: "∃y. ∀x. F(x,y) ⟷ F(x,x) ⟹ ¬(∀x. ∃y. ∀z. F(z,y) ⟷ ¬F(z,x))"
@proof
  @obtain A where "∀x. F(x,A) ⟷ F(x,x)"
  @have "¬(∃y. ∀z. F(z,y) ⟷ ¬F(z,A))" @with
    @have (@rule) "∀y. ¬(∀z. F(z,y) ⟷ ¬F(z,A))" @with
      @have "¬(F(y,y) ⟷ ¬F(y,A))" @with @case "F(y,y)" @end
    @end
  @end
@qed

theorem p42: "¬(∃y. ∀x. F(x,y) ⟷ ¬(∃z. F(x,z) ∧ F(z,x)))"
@proof
  @contradiction
  @obtain y where "∀x. F(x,y) ⟷ ¬(∃z. F(x,z) ∧ F(z,x))"
  @case "F(y,y)"
@qed

theorem p43: "∀x y. Q(x,y) ⟷ (∀z. F(z,x) ⟷ F(z,y)) ⟹
  ∀x y. Q(x,y) ⟷ Q(y,x)" by auto2

theorem p47:
  "(∀x. P1(x) ⟶ P0(x)) ∧ (∃x. P1(x)) ⟹
   (∀x. P2(x) ⟶ P0(x)) ∧ (∃x. P2(x)) ⟹
   (∀x. P3(x) ⟶ P0(x)) ∧ (∃x. P3(x)) ⟹
   (∀x. P4(x) ⟶ P0(x)) ∧ (∃x. P4(x)) ⟹
   (∀x. P5(x) ⟶ P0(x)) ∧ (∃x. P5(x)) ⟹
   (∃x. Q1(x)) ∧ (∀x. Q1(x) ⟶ Q0(x)) ⟹
   ∀x. P0(x) ⟶ ((∀y. Q0(y) ⟶ R(x,y)) ∨
                   (∀y. P0(y) ∧ S(y,x) ∧ (∃z. Q0(z) ∧ R(y,z)) ⟶ R(x,y))) ⟹
   ∀x y. P3(y) ∧ (P5(x) ∨ P4(x)) ⟶ S(x,y) ⟹
   ∀x y. P3(x) ∧ P2(y) ⟶ S(x,y) ⟹
   ∀x y. P2(x) ∧ P1(y) ⟶ S(x,y) ⟹
   ∀x y. P1(x) ∧ (P2(y) ∨ Q1(y)) ⟶ ¬R(x,y) ⟹
   ∀x y. P3(x) ∧ P4(y) ⟶ R(x,y) ⟹
   ∀x y. P3(x) ∧ P5(y) ⟶ ¬R(x,y) ⟹
   ∀x. P4(x) ∨ P5(x) ⟶ (∃y. Q0(y) ∧ R(x,y)) ⟹
   ∃x y. P0(x) ∧ P0(y) ∧ (∃z. Q1(z) ∧ R(y,z) ∧ R(x,y))"
@proof
  @obtain x1 x2 x3 x4 x5 where "P1(x1)" "P2(x2)" "P3(x3)" "P4(x4)" "P5(x5)"
  @have "S(x3,x2)" @have "S(x2,x1)" @have "R(x3,x4)" @have "¬R(x3,x5)"
@qed

theorem p48: "a = b ∨ c = d ⟹ a = c ∨ b = d ⟹ a = d ∨ b = c" by auto2

theorem p49: "∃x y. ∀(z::'a). z = x ∨ z = y ⟹ P(a) ∧ P(b) ⟹ (a::'a) ≠ b ⟹ ∀x. P(x)"
@proof
  @obtain x y where "∀(z::'a). z = x ∨ z = y"
  @have "x = a ∨ x = b"
  @have "∀c. P(c)" @with @have "c = a ∨ c = b" @end
@qed

theorem p50: "∀x. F(a,x) ∨ (∀y. F(x,y)) ⟹ ∃x. ∀y. F(x,y)"
@proof
  @case "∀y. F(a,y)"
  @obtain y where "¬F(a,y)"
  @have (@rule) "∀z. F(a,y) ∨ F(y,z)"
@qed

theorem p51: "∃z w. ∀x y. F(x,y) ⟷ x = z ∧ y = w ⟹
  ∃z. ∀x. (∃w. ∀y. F(x,y) ⟷ y = w) ⟷ x = z"
@proof
  @obtain z w where "∀x y. F(x,y) ⟷ x = z ∧ y = w"
  @have "∀x. (∃w. ∀y. F(x,y) ⟷ y = w) ⟷ x = z" @with
    @case "x = z" @with @have "∀y. F(x,y) ⟷ y = w" @end
  @end
@qed

theorem p52: "∃z w. ∀x y. F(x,y) ⟷ x = z ∧ y = w ⟹
  ∃w. ∀y. (∃z. ∀x. F(x,y) ⟷ x = z) ⟷ y = w"
@proof
  @obtain z w where "∀x y. F(x,y) ⟷ x = z ∧ y = w"
  @have"∀y. (∃z. ∀x. F(x,y) ⟷ x = z) ⟷ y = w" @with
    @case "y = w" @with @have "∀x. F(x,y) ⟷ x = z" @end
  @end
@qed

theorem p55:
  "∃x. L(x) ∧ K(x,a) ⟹
   L(a) ∧ L(b) ∧ L(c) ⟹
   ∀x. L(x) ⟶ x = a ∨ x = b ∨ x = c ⟹
   ∀y x. K(x,y) ⟶ H(x,y) ⟹
   ∀x y. K(x,y) ⟶ ¬R(x,y) ⟹
   ∀x. H(a,x) ⟶ ¬H(c,x) ⟹
   ∀x. x ≠ b ⟶ H(a,x) ⟹
   ∀x. ¬R(x,a) ⟶ H(b,x) ⟹
   ∀x. H(a,x) ⟶ H(b,x) ⟹  ―‹typo in text›
   ∀x. ∃y. ¬H(x,y) ⟹
   a ≠ b ⟹
   K(a,a)"
@proof
  @case "K(b,a)" @with @have "∀x. H(b,x)" @end
@qed

theorem p56: "(∀x. (∃y. F(y) ∧ x = f(y)) ⟶ F(x)) ⟷ (∀x. F(x) ⟶ F(f(x)))" by auto2

theorem p57: "F(f(a,b),f(b,c)) ⟹ F(f(b,c),f(a,c)) ⟹
  ∀x y z. F(x,y) ∧ F(y,z) ⟶ F(x,z) ⟹ F(f(a,b),f(a,c))" by auto2

theorem p58: "∀x y. f(x) = g(y) ⟹ ∀x y. f(f(x)) = f(g(y))"
@proof
  @have "∀x y. f(f(x)) = f(g(y))" @with
    @have "f(x) = g(y)"
  @end
@qed

theorem p59: "∀x::'a. F(x) ⟷ ¬F(f(x)) ⟹ ∃x. F(x) ∧ ¬F(f(x))"
@proof
  @obtain "x::'a" where "x = x" @case "F(x)"
@qed

theorem p60: "∀x. F(x,f(x)) ⟷ (∃y. (∀z. F(z,y) ⟶ F(z,f(x))) ∧ F(x,y))" by auto2

theorem p61: "∀x y z. f(x,f(y,z)) = f(f(x,y),z) ⟹ ∀x y z w. f(x,f(y,f(z,w))) = f(f(f(x,y),z),w)"
  by auto2

end