Theory Intuitionistic

theory Intuitionistic
imports IFOL
(*  Title:      FOL/ex/Intuitionistic.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge
*)

section ‹Intuitionistic First-Order Logic›

theory Intuitionistic
imports IFOL
begin

(*
Single-step ML commands:
by (IntPr.step_tac 1)
by (biresolve_tac safe_brls 1);
by (biresolve_tac haz_brls 1);
by (assume_tac 1);
by (IntPr.safe_tac 1);
by (IntPr.mp_tac 1);
by (IntPr.fast_tac @{context} 1);
*)


text‹Metatheorem (for \emph{propositional} formulae):
  $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable.
  Therefore $\neg P$ is classically provable iff it is intuitionistically
  provable.

Proof: Let $Q$ be the conjuction of the propositions $A\vee\neg A$, one for
each atom $A$ in $P$.  Now $\neg\neg Q$ is intuitionistically provable because
$\neg\neg(A\vee\neg A)$ is and because double-negation distributes over
conjunction.  If $P$ is provable classically, then clearly $Q\rightarrow P$ is
provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable
intuitionistically.  The latter is intuitionistically equivalent to $\neg\neg
Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is
intuitionistically provable.  Finally, if $P$ is a negation then $\neg\neg P$
is intuitionstically equivalent to $P$.  [Andy Pitts]›

lemma "¬ ¬ (P ∧ Q) ⟷ ¬ ¬ P ∧ ¬ ¬ Q"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "¬ ¬ ((¬ P ⟶ Q) ⟶ (¬ P ⟶ ¬ Q) ⟶ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text ‹Double-negation does NOT distribute over disjunction.›

lemma "¬ ¬ (P ⟶ Q) ⟷ (¬ ¬ P ⟶ ¬ ¬ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "¬ ¬ ¬ P ⟷ ¬ P"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "¬ ¬ ((P ⟶ Q ∨ R) ⟶ (P ⟶ Q) ∨ (P ⟶ R))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "(P ⟷ Q) ⟷ (Q ⟷ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "((P ⟶ (Q ∨ (Q ⟶ R))) ⟶ R) ⟶ R"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma
  "(((G ⟶ A) ⟶ J) ⟶ D ⟶ E) ⟶ (((H ⟶ B) ⟶ I) ⟶ C ⟶ J)
    ⟶ (A ⟶ H) ⟶ F ⟶ G ⟶ (((C ⟶ B) ⟶ I) ⟶ D) ⟶ (A ⟶ C)
    ⟶ (((F ⟶ A) ⟶ B) ⟶ I) ⟶ E"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


subsection ‹Lemmas for the propositional double-negation translation›

lemma "P ⟶ ¬ ¬ P"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "¬ ¬ (¬ ¬ P ⟶ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "¬ ¬ P ∧ ¬ ¬ (P ⟶ Q) ⟶ ¬ ¬ Q"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


text ‹The following are classically but not constructively valid.
  The attempt to prove them terminates quickly!›
lemma "((P ⟶ Q) ⟶ P) ⟶ P"
apply (tactic ‹IntPr.fast_tac @{context} 1›)?
apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
oops

lemma "(P ∧ Q ⟶ R) ⟶ (P ⟶ R) ∨ (Q ⟶ R)"
apply (tactic ‹IntPr.fast_tac @{context} 1›)?
apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
oops


subsection ‹de Bruijn formulae›

text ‹de Bruijn formula with three predicates›
lemma
  "((P ⟷ Q) ⟶ P ∧ Q ∧ R) ∧
    ((Q ⟷ R) ⟶ P ∧ Q ∧ R) ∧
    ((R ⟷ P) ⟶ P ∧ Q ∧ R) ⟶ P ∧ Q ∧ R"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


text ‹de Bruijn formula with five predicates›
lemma
  "((P ⟷ Q) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((Q ⟷ R) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((R ⟷ S) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((S ⟷ T) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ∧
    ((T ⟷ P) ⟶ P ∧ Q ∧ R ∧ S ∧ T) ⟶ P ∧ Q ∧ R ∧ S ∧ T"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


text ‹
  Problems from of Sahlin, Franzen and Haridi,
  An Intuitionistic Predicate Logic Theorem Prover.
  J. Logic and Comp. 2 (5), October 1992, 619-656.
›

text‹Problem 1.1›
lemma
  "(∀x. ∃y. ∀z. p(x) ∧ q(y) ∧ r(z)) ⟷
    (∀z. ∃y. ∀x. p(x) ∧ q(y) ∧ r(z))"
  by (tactic ‹IntPr.best_dup_tac @{context} 1›)  ‹SLOW›

text‹Problem 3.1›
lemma "¬ (∃x. ∀y. mem(y,x) ⟷ ¬ mem(x,x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹Problem 4.1: hopeless!›
lemma
  "(∀x. p(x) ⟶ p(h(x)) ∨ p(g(x))) ∧ (∃x. p(x)) ∧ (∀x. ¬ p(h(x)))
    ⟶ (∃x. p(g(g(g(g(g(x)))))))"
  oops


subsection ‹Intuitionistic FOL: propositional problems based on Pelletier.›

text‹‹¬¬›1›
lemma "¬ ¬ ((P ⟶ Q) ⟷ (¬ Q ⟶ ¬ P))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›2›
lemma "¬ ¬ (¬ ¬ P ⟷ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹3›
lemma "¬ (P ⟶ Q) ⟶ (Q ⟶ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›4›
lemma "¬ ¬ ((¬ P ⟶ Q) ⟷ (¬ Q ⟶ P))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›5›
lemma "¬ ¬ ((P ∨ Q ⟶ P ∨ R) ⟶ P ∨ (Q ⟶ R))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›6›
lemma "¬ ¬ (P ∨ ¬ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›7›
lemma "¬ ¬ (P ∨ ¬ ¬ ¬ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›8. Peirce's law›
lemma "¬ ¬ (((P ⟶ Q) ⟶ P) ⟶ P)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹9›
lemma "((P ∨ Q) ∧ (¬ P ∨ Q) ∧ (P ∨ ¬ Q)) ⟶ ¬ (¬ P ∨ ¬ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹10›
lemma "(Q ⟶ R) ⟶ (R ⟶ P ∧ Q) ⟶ (P ⟶ (Q ∨ R)) ⟶ (P ⟷ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


subsection‹11. Proved in each direction (incorrectly, says Pelletier!!)›

lemma "P ⟷ P"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›12. Dijkstra's law›
lemma "¬ ¬ (((P ⟷ Q) ⟷ R) ⟷ (P ⟷ (Q ⟷ R)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "((P ⟷ Q) ⟷ R) ⟶ ¬ ¬ (P ⟷ (Q ⟷ R))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹13. Distributive law›
lemma "P ∨ (Q ∧ R) ⟷ (P ∨ Q) ∧ (P ∨ R)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›14›
lemma "¬ ¬ ((P ⟷ Q) ⟷ ((Q ∨ ¬ P) ∧ (¬ Q ∨ P)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›15›
lemma "¬ ¬ ((P ⟶ Q) ⟷ (¬ P ∨ Q))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›16›
lemma "¬ ¬ ((P ⟶ Q) ∨ (Q ⟶ P))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›17›
lemma "¬ ¬ (((P ∧ (Q ⟶ R)) ⟶ S) ⟷ ((¬ P ∨ Q ∨ S) ∧ (¬ P ∨ ¬ R ∨ S)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text ‹Dijkstra's ``Golden Rule''›
lemma "(P ∧ Q) ⟷ P ⟷ Q ⟷ (P ∨ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


section ‹Examples with quantifiers›

subsection ‹The converse is classical in the following implications \dots›

lemma "(∃x. P(x) ⟶ Q) ⟶ (∀x. P(x)) ⟶ Q"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "((∀x. P(x)) ⟶ Q) ⟶ ¬ (∀x. P(x) ∧ ¬ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "((∀x. ¬ P(x)) ⟶ Q) ⟶ ¬ (∀x. ¬ (P(x) ∨ Q))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "(∀x. P(x)) ∨ Q ⟶ (∀x. P(x) ∨ Q)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

lemma "(∃x. P ⟶ Q(x)) ⟶ (P ⟶ (∃x. Q(x)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)


subsection ‹The following are not constructively valid!›
text ‹The attempt to prove them terminates quickly!›

lemma "((∀x. P(x)) ⟶ Q) ⟶ (∃x. P(x) ⟶ Q)"
  apply (tactic ‹IntPr.fast_tac @{context} 1›)?
  apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
  oops

lemma "(P ⟶ (∃x. Q(x))) ⟶ (∃x. P ⟶ Q(x))"
  apply (tactic ‹IntPr.fast_tac @{context} 1›)?
  apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
  oops

lemma "(∀x. P(x) ∨ Q) ⟶ ((∀x. P(x)) ∨ Q)"
  apply (tactic ‹IntPr.fast_tac @{context} 1›)?
  apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
  oops

lemma "(∀x. ¬ ¬ P(x)) ⟶ ¬ ¬ (∀x. P(x))"
  apply (tactic ‹IntPr.fast_tac @{context} 1›)?
  apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
  oops

text ‹Classically but not intuitionistically valid.  Proved by a bug in 1986!›
lemma "∃x. Q(x) ⟶ (∀x. Q(x))"
  apply (tactic ‹IntPr.fast_tac @{context} 1›)?
  apply (rule asm_rl) ‹Checks that subgoals remain: proof failed.›
  oops


subsection ‹Hard examples with quantifiers›

text ‹
  The ones that have not been proved are not known to be valid! Some will
  require quantifier duplication -- not currently available.
›

text‹‹¬¬›18›
lemma "¬ ¬ (∃y. ∀x. P(y) ⟶ P(x))"
  oops   ‹NOT PROVED›

text‹‹¬¬›19›
lemma "¬ ¬ (∃x. ∀y z. (P(y) ⟶ Q(z)) ⟶ (P(x) ⟶ Q(x)))"
  oops   ‹NOT PROVED›

text‹20›
lemma
  "(∀x y. ∃z. ∀w. (P(x) ∧ Q(y) ⟶ R(z) ∧ S(w)))
    ⟶ (∃x y. P(x) ∧ Q(y)) ⟶ (∃z. R(z))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹21›
lemma "(∃x. P ⟶ Q(x)) ∧ (∃x. Q(x) ⟶ P) ⟶ ¬ ¬ (∃x. P ⟷ Q(x))"
  oops  ‹NOT PROVED; needs quantifier duplication›

text‹22›
lemma "(∀x. P ⟷ Q(x)) ⟶ (P ⟷ (∀x. Q(x)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›23›
lemma "¬ ¬ ((∀x. P ∨ Q(x)) ⟷ (P ∨ (∀x. Q(x))))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹24›
lemma
  "¬ (∃x. S(x) ∧ Q(x)) ∧ (∀x. P(x) ⟶ Q(x) ∨ R(x)) ∧
    (¬ (∃x. P(x)) ⟶ (∃x. Q(x))) ∧ (∀x. Q(x) ∨ R(x) ⟶ S(x))
    ⟶ ¬ ¬ (∃x. P(x) ∧ R(x))"
text ‹
  Not clear why ‹fast_tac›, ‹best_tac›, ‹ASTAR› and
  ‹ITER_DEEPEN› all take forever.
›
  apply (tactic ‹IntPr.safe_tac @{context}›)
  apply (erule impE)
  apply (tactic ‹IntPr.fast_tac @{context} 1›)
  apply (tactic ‹IntPr.fast_tac @{context} 1›)
  done

text‹25›
lemma
  "(∃x. P(x)) ∧
      (∀x. L(x) ⟶ ¬ (M(x) ∧ R(x))) ∧
      (∀x. P(x) ⟶ (M(x) ∧ L(x))) ∧
      ((∀x. P(x) ⟶ Q(x)) ∨ (∃x. P(x) ∧ R(x)))
    ⟶ (∃x. Q(x) ∧ P(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›26›
lemma
  "(¬ ¬ (∃x. p(x)) ⟷ ¬ ¬ (∃x. q(x))) ∧
    (∀x. ∀y. p(x) ∧ q(y) ⟶ (r(x) ⟷ s(y)))
  ⟶ ((∀x. p(x) ⟶ r(x)) ⟷ (∀x. q(x) ⟶ s(x)))"
  oops  ‹NOT PROVED›

text‹27›
lemma
  "(∃x. P(x) ∧ ¬ Q(x)) ∧
    (∀x. P(x) ⟶ R(x)) ∧
    (∀x. M(x) ∧ L(x) ⟶ P(x)) ∧
    ((∃x. R(x) ∧ ¬ Q(x)) ⟶ (∀x. L(x) ⟶ ¬ R(x)))
  ⟶ (∀x. M(x) ⟶ ¬ L(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›28. AMENDED›
lemma
  "(∀x. P(x) ⟶ (∀x. Q(x))) ∧
      (¬ ¬ (∀x. Q(x) ∨ R(x)) ⟶ (∃x. Q(x) ∧ S(x))) ∧
      (¬ ¬ (∃x. S(x)) ⟶ (∀x. L(x) ⟶ M(x)))
    ⟶ (∀x. P(x) ∧ L(x) ⟶ M(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹29. Essentially the same as Principia Mathematica *11.71›
lemma
  "(∃x. P(x)) ∧ (∃y. Q(y))
    ⟶ ((∀x. P(x) ⟶ R(x)) ∧ (∀y. Q(y) ⟶ S(y)) ⟷
      (∀x y. P(x) ∧ Q(y) ⟶ R(x) ∧ S(y)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›30›
lemma
  "(∀x. (P(x) ∨ Q(x)) ⟶ ¬ R(x)) ∧
      (∀x. (Q(x) ⟶ ¬ S(x)) ⟶ P(x) ∧ R(x))
    ⟶ (∀x. ¬ ¬ S(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹31›
lemma
  "¬ (∃x. P(x) ∧ (Q(x) ∨ R(x))) ∧
      (∃x. L(x) ∧ P(x)) ∧
      (∀x. ¬ R(x) ⟶ M(x))
  ⟶ (∃x. L(x) ∧ M(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹32›
lemma
  "(∀x. P(x) ∧ (Q(x) ∨ R(x)) ⟶ S(x)) ∧
    (∀x. S(x) ∧ R(x) ⟶ L(x)) ∧
    (∀x. M(x) ⟶ R(x))
  ⟶ (∀x. P(x) ∧ M(x) ⟶ L(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹‹¬¬›33›
lemma
  "(∀x. ¬ ¬ (P(a) ∧ (P(x) ⟶ P(b)) ⟶ P(c))) ⟷
    (∀x. ¬ ¬ ((¬ P(a) ∨ P(x) ∨ P(c)) ∧ (¬ P(a) ∨ ¬ P(b) ∨ P(c))))"
  apply (tactic ‹IntPr.best_tac @{context} 1›)
  done


text‹36›
lemma
  "(∀x. ∃y. J(x,y)) ∧
    (∀x. ∃y. G(x,y)) ∧
    (∀x y. J(x,y) ∨ G(x,y) ⟶ (∀z. J(y,z) ∨ G(y,z) ⟶ H(x,z)))
  ⟶ (∀x. ∃y. H(x,y))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹37›
lemma
  "(∀z. ∃w. ∀x. ∃y.
      ¬ ¬ (P(x,z) ⟶ P(y,w)) ∧ P(y,z) ∧ (P(y,w) ⟶ (∃u. Q(u,w)))) ∧
        (∀x z. ¬ P(x,z) ⟶ (∃y. Q(y,z))) ∧
        (¬ ¬ (∃x y. Q(x,y)) ⟶ (∀x. R(x,x)))
    ⟶ ¬ ¬ (∀x. ∃y. R(x,y))"
  oops  ‹NOT PROVED›

text‹39›
lemma "¬ (∃x. ∀y. F(y,x) ⟷ ¬ F(y,y))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹40. AMENDED›
lemma
  "(∃y. ∀x. F(x,y) ⟷ F(x,x)) ⟶
    ¬ (∀x. ∃y. ∀z. F(z,y) ⟷ ¬ F(z,x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹44›
lemma
  "(∀x. f(x) ⟶
    (∃y. g(y) ∧ h(x,y) ∧ (∃y. g(y) ∧ ¬ h(x,y)))) ∧
    (∃x. j(x) ∧ (∀y. g(y) ⟶ h(x,y)))
    ⟶ (∃x. j(x) ∧ ¬ f(x))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹48›
lemma "(a = b ∨ c = d) ∧ (a = c ∨ b = d) ⟶ a = d ∨ b = c"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹51›
lemma
  "(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃z. ∀x. ∃w. (∀y. P(x,y) ⟷ y = w) ⟷ x = z)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹52›
text ‹Almost the same as 51.›
lemma
  "(∃z w. ∀x y. P(x,y) ⟷ (x = z ∧ y = w)) ⟶
    (∃w. ∀y. ∃z. (∀x. P(x,y) ⟷ x = z) ⟷ y = w)"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹56›
lemma "(∀x. (∃y. P(y) ∧ x = f(y)) ⟶ P(x)) ⟷ (∀x. P(x) ⟶ P(f(x)))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹57›
lemma
  "P(f(a,b), f(b,c)) ∧ P(f(b,c), f(a,c)) ∧
    (∀x y z. P(x,y) ∧ P(y,z) ⟶ P(x,z)) ⟶ P(f(a,b), f(a,c))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

text‹60›
lemma "∀x. P(x,f(x)) ⟷ (∃y. (∀z. P(z,y) ⟶ P(z,f(x))) ∧ P(x,y))"
  by (tactic ‹IntPr.fast_tac @{context} 1›)

end