CODEWITHSUNDEEP
logichigher-order-functionsisabelle
RosterPantyhose
RosterPantyhose

Reputation: 13

How to prove exists goal in this Isabelle/HOL lemma?

I have the following Isabelle/HOL theorem I'd like to prove:

lemma involution:
  "∀P h. (∀x. ¬P x ⟶ P (h x)) ⟶ (∃x. P x ∧ P (h (h x)))"

but I have so far not found the correct inference rules to prove it. I believe it follows from directly from inference rule applications since metis can prove it trivially.

My proof script has only the following:

apply (rule allI; rename_tac P; rule allI; rename_tac h; rule impI)
apply (rule exI; rule conjI)

leaving me with the goal:

proof (prove)
goal (2 subgoals):
 - ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
           P (?x17 P h)
 - ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
           P (h (h (?x17 P h)))

after which I'm quite stumped as to how to proceed. I may need some invocation of the law of excluded middle, I tried both:

to no avail.

I am more familiar with Coq than Isabelle/HOL but even there I could not prove it (even with the additional assumption that the argument type for P is inhabited, and the classic axiom).

Any clues would be much appreciated.

Upvotes: 1

Views: 390

Answers (1)

Javier Díaz
Javier Díaz

Reputation: 1101

First of all, as you already mentioned, your lemma can be trivially proved by some of the Isabelle's built-in proof methods, e.g., blast in Isabelle2021-1. However, since I guess you are looking for a more pedagogical answer, I'll elaborate a bit on it.

Before tackling the proof of a non-trivial result, it's often useful to have a pen-and-paper proof sketch first. Here's the one I got off the top of my head (perhaps there's a simpler one, but for illustration purposes I think it will suffice):

My proof is by case distinction. Let a by an arbitrary but fixed value. Then, the following table shows all the cases to consider and an associated witness that satisfies the conclusion:

Case #  P a  P (h a)  P (h (h a))  P (h (h (h a)))  P (h (h (h (h a))))  Witness
----------------------------------------------------------------------------------
1       T    ?        T            ?                ?                    a
2       T    F -----> T            ?                ?                    a
3       T    T        F ---------> T                ?                    h a
4       F -> T        ?            T                ?                    h a
5       F -> T        F ---------> T                ?                    h a
6       F -> T        T            F -------------> T                    h (h a)

In the table above, T, F and ? stands for True, False and "don't care" respectively, and a dashed arrow represents an instantiation of the premise ∀x. ¬P x ⟶ P (h x) with a specific value of x. This concludes our proof sketch.

Regarding an Isabelle/HOL proof for your lemma, I think a few remarks are in order:

  • Since the outermost universal quantifiers are superfluous, I'll remove them from the lemma statement and use free variables instead.

  • *_tac tactics are considered obsolete nowadays, and Isabelle/Isar (i.e., structured) proofs are strongly preferred over apply-scripts (except for the experimental stages of a proof). Please refer to the Isabelle/Isar Reference Manual for further details.

Now, please find below a structured proof for your lemma, based on the proof sketch above. For pedagogical purposes, I tried to break down the proof to the most elementary steps and included inline comments in the code in order to aid the reader:

lemma involution:
  assumes "∀x. ¬P x ⟶ P (h x)" 
  shows "∃x. P x ∧ P (h (h x))"
proof -
  fix a (* an arbitrary but fixed value *)
  show ?thesis
  proof (cases "P a")
    case True
    then consider
        ("Case #1") "P (h (h a))"
      | ("Case #2") "¬P (h a)"
      | ("Case #3") "P (h a)" and "¬P (h (h a))"
      by blast
    then show ?thesis
    proof cases
      case "Case #1"
      from ‹P a› and ‹P (h (h a))› have "P a ∧ P (h (h a))"
        by (intro conjI)
      then show ?thesis
        by (intro exI) (* `exI` using `a` as witness *)
    next
      case "Case #2"
      have "¬P (h a)"
        by fact (* assumption of case #2 *)
      moreover have "¬P (h a) ⟶ P (h (h a))"
        by (rule assms [THEN spec]) (* instantiation of premise with `h a` *)
      ultimately have "P (h (h a))"
        by (rule rev_mp) (* modus ponens *)
      (* NOTE: The three steps above can be replaced by `then have "P (h (h a))" using assms by simp` *)
      from ‹P a› and ‹P (h (h a))› have "P a ∧ P (h (h a))"
        by (intro conjI)
      then show ?thesis
        by (intro exI) (* `exI` using `a` as witness *)
    next
      case "Case #3"
      then have "P (h (h (h a)))" (* use of shortcut explained above *)
        using assms by simp (* instantiation of premise with `h (h a)` *)
      from ‹P (h a)› and ‹P (h (h (h a)))› have "P (h a) ∧ P (h (h (h a)))"
        by (intro conjI)
      then show ?thesis
        by (intro exI) (* `exI` using `h a` as witness *)
    qed
  next
    case False (* i.e., `¬P a` *)
    then have "P (h a)"
      using assms by simp (* instantiation of premise with `a` *)
    then consider
        ("Case #4") "P (h (h (h a)))"
      | ("Case #5") "¬P (h (h a))"
      | ("Case #6") "P (h (h a))" and "¬P (h (h (h a)))"
      by blast
    then show ?thesis
      sorry (* proof omitted, similar to cases #1, #2, and #3 *)
  qed
qed

Upvotes: 2

Related Questions