Induction Proofs in B - Revision history

Michael Leuschel: /* Rodin Archive */

2024-01-08T12:22:56Z

Rodin Archive

← Older revision		Revision as of 12:22, 8 January 2024
Line 229:		Line 229:

	The Rodin archive [https://www3.hhu.de/stups/models/rodin_archives/InductionTests.zip InductionTests.zip] including all models above is available.		The Rodin archive [https://www3.hhu.de/stups/models/rodin_archives/InductionTests.zip InductionTests.zip] including all models above is available.

			See also the page [https://wiki.event-b.org/index.php/Induction_proof https://wiki.event-b.org/index.php/Induction_proof].

Michael Leuschel: /* Induction and B */

2020-09-10T07:45:11Z

Induction and B

← Older revision		Revision as of 07:45, 10 September 2020
Line 11:		Line 11:
	The answer is, maybe surprisingly, yes.		The answer is, maybe surprisingly, yes.
	The reason is that B is not just rooted in predicate logic, but has access to arithmetic and set theory.		The reason is that B is not just rooted in predicate logic, but has access to arithmetic and set theory.
	As such, induction comes "bundled" with the arithmetic operators and data types, more precisely with the well-founded nature of the natural ~~number~~ and the concept of the minimum of a set.		As such, induction comes "bundled" with the arithmetic operators and data types, more precisely with the well-founded nature of the natural numbers and the concept of the minimum of a set.

Michael Leuschel: /* The full model with the inductive proof */

2020-04-23T08:27:13Z

The full model with the inductive proof

← Older revision		Revision as of 08:27, 23 April 2020
Line 132:		Line 132:
	[[File:Rodin_Induction_ScreenshotFinal.png\|200px\|center]]		[[File:Rodin_Induction_ScreenshotFinal.png\|200px\|center]]

	This example can also be conducted within Atelier-B. In fact, Dominique Cansell showed me the "trick" at the time ~~within AtelierB (~~within the B4Free version).		This example can also be conducted within Atelier-B. In fact, Dominique Cansell showed me the "trick" at the time within the B4Free version of Atelier-B.


	== Additional Discussions ==		== Additional Discussions ==

Michael Leuschel: /* A generic induction proof */

2020-04-23T08:26:17Z

A generic induction proof

← Older revision		Revision as of 08:26, 23 April 2020
Line 92:		Line 92:


	The proof above is very similar to, e.g., the proof of Theorem 1.7.1 on page 17 of the book "The Joy of Sets" by Keith Devlin or the proof [https://proofwiki.org/wiki/Principle_of_Mathematical_Induction/Well-Ordered_Set in https://proofwiki.org] for well-ordered sets: there a proof by contradiction is conducted, using the fact that		The proof above is very similar to, e.g., the proof of Theorem 1.7.1 on page 17 of the book "The Joy of Sets" by Keith Devlin or the proof [https://proofwiki.org/wiki/Principle_of_Mathematical_Induction/Well-Ordered_Set in https://proofwiki.org] for well-ordered sets: there a proof by contradiction is conducted, using the fact that the complement NAT1 \ P is non-empty and choosing the minimal element of the complement to arrive at a contradiction.
	the complement NAT1 \ P is non-empty and choosing the minimal element of the complement to arrive at a contradiction.

	== The full model with the inductive proof ==		== The full model with the inductive proof ==

Michael Leuschel: /* A generic induction proof */

2020-04-23T08:25:23Z

A generic induction proof

← Older revision		Revision as of 08:25, 23 April 2020
Line 66:		Line 66:

	Here P is the property we wish to hold for all natural numbers ≥ 1.		Here P is the property we wish to hold for all natural numbers ≥ 1.
	We stipulate the base of the induction proof as an axiom here:		We stipulate the base of the induction proof as an axiom here: we assume we have prove that 1 is an element of P in the axiom <tt>@base</tt>
	we assume we have prove that 1 is an element of P in the axiom <tt>@base</tt>
	We also assume that we have proven the induction step in the axiom <tt>@induct</tt>,		We also assume that we have proven the induction step in the axiom <tt>@induct</tt>,
	namely that i-1 in P implies that i is in the property P.		namely that i-1 in P implies that i is in the property P.

Michael Leuschel: /* Induction and Pure Predicate Logic */

2020-04-23T08:15:05Z

Induction and Pure Predicate Logic

← Older revision		Revision as of 08:15, 23 April 2020
Line 228:		Line 228:

	But as shown above, in B we have directly access to the set of natural numbers and to the min operator; hence we can conduct valid induction this way.		But as shown above, in B we have directly access to the set of natural numbers and to the min operator; hence we can conduct valid induction this way.

			== Rodin Archive ==

			The Rodin archive [https://www3.hhu.de/stups/models/rodin_archives/InductionTests.zip InductionTests.zip] including all models above is available.

Michael Leuschel: /* Induction and B */

2020-04-23T07:58:40Z

Induction and B

← Older revision		Revision as of 07:58, 23 April 2020
Line 3:		Line 3:
	The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction.		The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction.
	Note that the B proof rules for invariant preservation are an induction proof in disguise, i.e, the induction is provided by the POG (Proof Obligation Generator) and not the prover itself.		Note that the B proof rules for invariant preservation are an induction proof in disguise, i.e, the induction is provided by the POG (Proof Obligation Generator) and not the prover itself.
	They require coding your problem and induction steps as B operations ([[Induction_Proofs_in_B#Encoding_the_Problem_as_a_B_Operation\|see the ~~end of this page for one way to do this~~]]).		They require coding your problem and induction steps as B operations ([[Induction_Proofs_in_B#Encoding_the_Problem_as_a_B_Operation\|see the discussions below]]).
	Here, I am interested in proving properties in B directly using induction without the help of an external POG.		Here, I am interested in proving properties in B directly using induction without the help of an external POG.

	It is well known that predicate logic is too weak to axiomatize exactly the natural numbers or concepts such as the [https://en.wikipedia.org/wiki/Transitive_closure transitive closure]: <em>The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (FO) </em> ([https://en.wikipedia.org/wiki/Transitive_closure#In_logic_and_computational_complexity Source: Wikipedia]).		It is well known that predicate logic is too weak to axiomatize exactly the natural numbers or concepts such as the [https://en.wikipedia.org/wiki/Transitive_closure transitive closure]: <em>The transitive closure of a binary relation cannot, in general, be expressed in first-order logic (FO) </em> ([https://en.wikipedia.org/wiki/Transitive_closure#In_logic_and_computational_complexity Source: Wikipedia]). [[Induction_Proofs_in_B#Induction_and_Pure_Predicate_Logic\|See also the discussions below]].

	So, can we perform induction proofs within the B language, without resorting to provers such as Isabelle?		So, can we perform induction proofs within the B language, without resorting to provers such as Isabelle?

Michael Leuschel: /* Induction and B */

2020-04-23T07:57:43Z

Induction and B

← Older revision		Revision as of 07:57, 23 April 2020
Line 3:		Line 3:
	The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction.		The classical B and Event-B method are both rooted in classical predicate logic and do not have an explicit inference rule for induction.
	Note that the B proof rules for invariant preservation are an induction proof in disguise, i.e, the induction is provided by the POG (Proof Obligation Generator) and not the prover itself.		Note that the B proof rules for invariant preservation are an induction proof in disguise, i.e, the induction is provided by the POG (Proof Obligation Generator) and not the prover itself.
	They require coding your problem and induction steps as B operations (see the end of this page for one way to do this).		They require coding your problem and induction steps as B operations ([[Induction_Proofs_in_B#Encoding_the_Problem_as_a_B_Operation\|see the end of this page for one way to do this]]).
	Here, I am interested in proving properties in B directly using induction without the help of an external POG.		Here, I am interested in proving properties in B directly using induction without the help of an external POG.

Michael Leuschel: /* Induction and Pure Predicate Logic */

2020-04-23T07:56:49Z

Induction and Pure Predicate Logic

← Older revision		Revision as of 07:56, 23 April 2020
Line 176:		Line 176:
	The induction principle itself is here outside of the B provers: the provers are used to discharge the above proof obligations, not to prove that they entail that the invariant is true in all reachable states.		The induction principle itself is here outside of the B provers: the provers are used to discharge the above proof obligations, not to prove that they entail that the invariant is true in all reachable states.

	== Induction and Pure Predicate Logic ==		=== Induction and Pure Predicate Logic ===

	Let us try and encode natural numbers using predicate logic:		Let us try and encode natural numbers using predicate logic:

Michael Leuschel: /* Encoding the Problem as a B Operation */

2020-04-23T07:56:40Z

Encoding the Problem as a B Operation

← Older revision		Revision as of 07:56, 23 April 2020
Line 136:		Line 136:
	This example can also be conducted within Atelier-B. In fact, Dominique Cansell showed me the "trick" at the time within AtelierB (within the B4Free version).		This example can also be conducted within Atelier-B. In fact, Dominique Cansell showed me the "trick" at the time within AtelierB (within the B4Free version).

	== Encoding the Problem as a B Operation ==
			== Additional Discussions ==

			Below we provide two additional discussions, one about how to encode induction
			using B operations and the B proof obligations, and one about induction
			and pure predicate logic.

			=== Encoding the Problem as a B Operation ===

	Here is how we can encode our property about the consecutive sums using a B operation		Here is how we can encode our property about the consecutive sums using a B operation