[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Using DownwardNatInduction from NaturalsInduction

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)
  <1>2. \A n \in 1 .. m : R(n) => R(n-1)
  <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.