Using DownwardNatInduction from NaturalsInduction

[Ugur Y. Yavuz]

The NaturalsInduction module contains useful theorems about inductive reasoning on naturals, including the following:

THEOREM DownwardNatInduction ==
  ASSUME NEW P(_), NEW m \in Nat, P(m),
         \A n \in 1 .. m : P(n) => P(n-1)

  PROVE  P(0)

It isn't hard to observe that one could easily go in the other direction, and it would be a corollary of DownwardNatInduction. However, I'm having a hard time proving it in TLAPS.

THEOREM UpwardNatInduction ==
    ASSUME NEW P(_), NEW m \in Nat, P(0),
           \A n \in 1 .. m : P(n-1) => P(n)
    PROVE  P(m)
  <1> DEFINE R(i) == P(m-i)
  <1>1. R(m)
    OBVIOUS
  <1>2. \A n \in 1 .. m : R(n) => R(n-1)
    OBVIOUS
  <1>3. R(0)
    BY <1>1, <1>2, DownwardNatInduction
  <1> QED
    BY <1>3

I expected that <1>3 would easily be proven by Isabelle given the original theorem, plus <1>1 and <1>2, but I was unable to make that step go through. I tried invoking Isabelle with "blast" and "force", and higher timeouts, also to no avail. What could be the reason for this failure?

On a side note, I can circumvent this problem by imitating the proof of DownwardNatInduction in NaturalsInduction_proofs, which uses NatInduction – but I would like to be able to leverage DownwardNatInduction directly to prove the claim.

[Stephan Merz]

Hi Ugur,

Isabelle uses the definition of R, simplifies the resulting arithmetic expressions, and the proof then no longer matches the rule you wish to apply. So you need to hide the definition of R before applying rule DownwardNatInduction. The following works:

THEOREM UpwardNatInduction ==

    ASSUME NEW P(_), NEW m \in Nat, P(0),

           \A n \in 1 .. m : P(n-1) => P(n)

    PROVE  P(m)

  <1> DEFINE R(i) == P(m-i)

  <1>1. R(m)

    OBVIOUS

  <1>2. \A n \in 1 .. m : R(n) => R(n-1)

    OBVIOUS

  <1>3. R(0)

    <2>. HIDE DEF R

    <2>. QED  BY <1>1, <1>2, DownwardNatInduction

  <1> QED

    BY <1>3

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e946a3f1-5422-4ee1-b598-a98e57c2275an%40googlegroups.com.