Search code examples
coqproofisabelle

Proof with false hypothesis in Isabelle/HOL Isar

I am trying to prove a lemma which in a certain part has a false hypothesis. In Coq I used to write "congruence" and it would get rid of the goal. However, I am not sure how to proceed in Isabelle Isar. I am trying to prove a lemma about my le function:

primrec le::"nat ⇒ nat ⇒ bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ⇒ False | Suc j ⇒ le k j)"

lemma def_le: "le a b = True ⟷ (∃k. a + k = b)"
proof
  assume H:"le a b = True"
  show "∃k. a + k = b"
  proof (induct a)
    case 0
    show "∃k. 0 + k = b"
    proof -
      have "0 + b = b" by simp
      thus ?thesis by (rule exI)
    qed

    case Suc
    fix n::nat
    assume HI:"∃k. n + k = b"
    show "∃k. (Suc n) + k = b"
    proof (induct b)
      case 0
      show "∃k. (Suc n) + k = 0"
      proof -
        have "le (Suc n) 0 = False" by simp
        oops

Note that my le function is "less or equal". At this point of the proof I find I have the hypothesis H which states that le a b = True, or in this case that le (Suc n) 0 = True which is false. How can I solve this lemma?

Another little question: I would like to write have "le (Suc n) 0 = False" by (simp only:le.simps) but this does not work. It seems I need to add some rule for reducing case expressions. What am I missing?

Thank you very much for your help.

Solution

  • The problem is not that it is hard to get rid of a False hypothesis in Isabelle. In fact, pretty much all of Isabelle's proof methods will instantly prove anything if there is False in the assumptions. No, the problem here is that at that point of the proof, you don't have the assumptions you need anymore, because you did not chain them into the induction. But first, allow me to make a few small remarks, and then give concrete suggestions to fix your proof.

    A Few Remarks

    1. It is somewhat unidiomatic to write le a b = True or le a b = False in Isabelle. Just write le a b or ¬le a b.
    2. Writing the definition in a convenient form is very important to get good automation. Your definition works, of course, but I suggest the following one, which may be more natural and will give you a convenient induction rule for free:

    Using the function package:

    fun le :: "nat ⇒ nat ⇒ bool" where
  "le 0 n             = True"
| "le (Suc k) 0       = False"
| "le (Suc k) (Suc n) = le k n"
    1. Existentials can sometimes hide important information, and they tend mess with automation, since the automation never quite knows how to instantiate them.

    If you prove the following lemma, the proof is fully automatic:

    lemma def_le': "le a b ⟷ a + (b - a) = b"
  by (induction a arbitrary: b) (simp_all split: nat.split)

    Using my function definition, it is:

    lemma def_le': "le a b ⟷ (a + (b - a) = b)"
  by (induction a b rule: le.induct) simp_all

    Your lemma then follows from that trivially:

    lemma def_le: "le a b ⟷ (∃k. a + k = b)"
  using def_le' by auto

    This is because the existential makes the search space explode. Giving the automation something concrete to follow helps a lot.

    The actual answer

    There are a number of problems. First of all, you will probably need to do induct a arbitrary: b, since the b will change during your induction (for le (Suc a) b, you will have to do a case analysis on b, and then in the case b = Suc b' you will go from le (Suc a) (Suc b') to le a b').

    Second, at the very top, you have assume "le a b = True", but you do not chain this fact into the induction. If you do induction in Isabelle, you have to chain all required assumptions containing the induction variables into the induction command, or they will not be available in the induction proof. The assumption in question talks about a and b, but if you do induction over a, you will have to reason about some arbitrary variable a' that has nothing to do with a. So do e.g:

    assume H:"le a b = True"
thus "∃k. a + k = b"

    (and the same for the second induction over b)

    Third, when you have several cases in Isar (e.g. during an induction or case analysis), you have to separate them with next if they have different assumptions. The next essentially throws away all the fixed variables and local assumptions. With the changes I mentioned before, you will need a next before the case Suc, or Isabelle will complain.

    Fourth, the case command in Isar can fix variables. In your Suc case, the induction variable a is fixed; with the change to arbitrary: b, an a and a b are fixed. You should give explicit names to these variables; otherwise, Isabelle will invent them and you will have to hope that the ones it comes up with are the same as those that you use. That is not good style. So write e.g. case (Suc a b). Note that you do not have to fix variables or assume things when using case. The case command takes care of that for you and stores the local assumptions in a theorem collection with the same name as the case, e.g. Suc here. They are categorised as Suc.prems, Suc.IH, Suc.hyps. Also, the proof obligation for the current case is stored in ?case (not ?thesis!).

    Conclusion

    With that (and a little bit of cleanup), your proof looks like this:

    lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
  assume "le a b"
  thus "∃k. a + k = b"
  proof (induct a arbitrary: b)
    case 0
    show "∃k. 0 + k = b" by simp
  next
    case (Suc a b)
    thus ?case
    proof (induct b)
      case 0
      thus ?case by simp
    next
      case (Suc b)
      thus ?case by simp
    qed
  qed
next

    It can be condensed to

    lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
  assume "le a b"
  thus "∃k. a + k = b"
  proof (induct a arbitrary: b)
    case (Suc a b)
    thus ?case by (induct b) simp_all
  qed simp
next

    But really, I would suggest that you simply prove a concrete result like le a b ⟷ a + (b - a) = b first and then prove the existential statement using that.