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

*From*: "Ugur Y. Yavuz" <uguryagmuryavuz@xxxxxxxxx>*Date*: Tue, 2 Jan 2024 08:59:55 -0800 (PST)

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

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

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.

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

<1>

<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>

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.

**Follow-Ups**:**Re: [tlaplus] Using DownwardNatInduction from NaturalsInduction***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: Where does assert go in Euclid Algorithm of Chapter 4.5** - Next by Date:
**Re: [tlaplus] Using DownwardNatInduction from NaturalsInduction** - Previous by thread:
**Re: [tlaplus] Trying to understand lifting in Isabelle/HOL TLA*** - Next by thread:
**Re: [tlaplus] Using DownwardNatInduction from NaturalsInduction** - Index(es):