[tlaplus] Using DownwardNatInduction from NaturalsInduction

["Ugur Y. Yavuz" <uguryagmuryavuz@xxxxxxxxx>]

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.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e946a3f1-5422-4ee1-b598-a98e57c2275an%40googlegroups.com.