[Rodin-b-sharp-user] Induction in proof From: George Zaff - 2013-01-18 19:11 Attachments: Message as HTML ```Hi all, Im new to Rodin/event-b and have been exploring the interactive proof system. I found myself stuck while trying to apply induction. In the following, I define a set of natural numbers, mappings to/from this set into the builtin set of natural numbers and show that it defines the same set. However, when attempting to show that the mappings are isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their proofs require the induction hypothesis. CONTEXT Nat › SETS Nat › CONSTANTS zero › suc › toNat › fromNat › S › AXIOMS axm1: zero ∈ Nat not theorem › axm2: suc ∈ Nat → Nat not theorem › axm3: toNat ∈ ℕ → Nat not theorem › axm4: toNat(0) = zero not theorem › axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › axm6: toNat(1) = suc(zero) theorem › axm7: fromNat ∈ Nat → ℕ not theorem › axm8: fromNat(zero) = 0 not theorem › axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not theorem › axm10: fromNat(suc(zero)) = 1 theorem › axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s not theorem › axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not theorem › axm14: S ⊆ ℕ theorem › axm15: 0 ∈ S theorem › axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › axm17: ℕ ⊆ S theorem › axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) not theorem › axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › END A second small query I have is whether there is support for a type of all sets? E.g. it is possible to write something of the form: ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a = a' ⇒ f(a) = f(a') Thanks, George ```
 Re: [Rodin-b-sharp-user] Induction in proof From: Hoang, Thai Son - 2013-01-19 00:38 ```Dear George, Here is the wiki page for an example of performing a proof by induction http://wiki.event-b.org/index.php/Induction_proof In your case, for proving axm18, you can instantiate s in axm11 with {a | a∈ℕ∧fromNat(toNat(a))=a}. Cheers, Son On 18 Jan 2013, at 20:11, George Zaff > wrote: Hi all, Im new to Rodin/event-b and have been exploring the interactive proof system. I found myself stuck while trying to apply induction. In the following, I define a set of natural numbers, mappings to/from this set into the builtin set of natural numbers and show that it defines the same set. However, when attempting to show that the mappings are isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their proofs require the induction hypothesis. CONTEXT Nat › SETS Nat › CONSTANTS zero › suc › toNat › fromNat › S › AXIOMS axm1: zero ∈ Nat not theorem › axm2: suc ∈ Nat → Nat not theorem › axm3: toNat ∈ ℕ → Nat not theorem › axm4: toNat(0) = zero not theorem › axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › axm6: toNat(1) = suc(zero) theorem › axm7: fromNat ∈ Nat → ℕ not theorem › axm8: fromNat(zero) = 0 not theorem › axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not theorem › axm10: fromNat(suc(zero)) = 1 theorem › axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s not theorem › axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not theorem › axm14: S ⊆ ℕ theorem › axm15: 0 ∈ S theorem › axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › axm17: ℕ ⊆ S theorem › axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) not theorem › axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › END A second small query I have is whether there is support for a type of all sets? E.g. it is possible to write something of the form: ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a = a' ⇒ f(a) = f(a') Thanks, George ------------------------------------------------------------------------------ Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and much more. Get web development skills now with LearnDevNow - 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE \$99.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122812_______________________________________________ Rodin-b-sharp-user mailing list Rodin-b-sharp-user@... https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user ```
 Re: [Rodin-b-sharp-user] Induction in proof From: George Zaff - 2013-01-19 16:42 Attachments: Message as HTML ```Thanks that is very helpful. I have another question relating to induction: Out of interest, I was wondering whether it is possible to prove the axiom of induction on natural numbers using Rodin? Ive looked at the proof on the Wikipedia article: https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction However, I have been unable to carry out the proof in Rodin. Thanks, George On Sat, Jan 19, 2013 at 12:38 AM, Hoang, Thai Son wrote: > Dear George, > Here is the wiki page for an example of performing a proof by induction > http://wiki.event-b.org/index.php/Induction_proof > In your case, for proving axm18, you can instantiate s in axm11 with {a | > a∈ℕ∧fromNat(toNat(a))=a}. > Cheers, > Son > On 18 Jan 2013, at 20:11, George Zaff ggzaff@...>> > wrote: > > Hi all, > > Im new to Rodin/event-b and have been exploring the interactive proof > system. I found myself stuck while trying to apply induction. > > In the following, I define a set of natural numbers, mappings to/from this > set into the builtin set of natural numbers and show that it defines the > same set. However, when attempting to show that the mappings are > isomorphic, axm18 and amx20 below, I am not sure how to proceed. Their > proofs require the induction hypothesis. > > CONTEXT > Nat › > SETS > Nat › > CONSTANTS > zero › > suc › > toNat › > fromNat › > S › > AXIOMS > axm1: zero ∈ Nat not theorem › > axm2: suc ∈ Nat → Nat not theorem › > axm3: toNat ∈ ℕ → Nat not theorem › > axm4: toNat(0) = zero not theorem › > axm5: ∀ n · n ∈ ℕ ⇒ toNat(n + 1) = suc(toNat(n)) not theorem › > axm6: toNat(1) = suc(zero) theorem › > axm7: fromNat ∈ Nat → ℕ not theorem › > axm8: fromNat(zero) = 0 not theorem › > axm9: ∀ n · n ∈ Nat ⇒ fromNat(suc(n)) = fromNat(n) + 1 not > theorem › > axm10: fromNat(suc(zero)) = 1 theorem › > axm11: ∀ s · s ⊆ ℕ ∧ 0 ∈ s ∧ (∀ n · n ∈ s ⇒ n + 1 ∈ s) ⇒ ℕ ⊆ s > not theorem › > axm12: ∀ n · n ∈ ℕ ⇒ n = 0 ∨ (∃ m · m ∈ ℕ ∧ n = m + 1) theorem › > axm13: S = { n ∣ n ∈ ℕ ∧ (∃ x · x ∈ Nat ∧ n = fromNat(x)) } not > theorem › > axm14: S ⊆ ℕ theorem › > axm15: 0 ∈ S theorem › > axm16: ∀ s · s ∈ S ⇒ s + 1 ∈ S theorem › > axm17: ℕ ⊆ S theorem › > axm18: ∀ n · n ∈ ℕ ⇒ fromNat(toNat(n)) = n theorem › > axm19: ∀ x · x ∈ Nat ⇒ x = zero ∨ (∃ y · y ∈ Nat ∧ x = suc(y)) > not theorem › > axm20: ∀ x · x ∈ Nat ⇒ toNat(fromNat(x)) = x theorem › > END > > > A second small query I have is whether there is support for a type of all > sets? E.g. it is possible to write something of the form: > ∀ A , B , f , a , a' · A ∈ SET ∧ B ∈ SET ∧ f ∈ A → B ∧ a ∈ A ∧ a' ∈ A ∧ a > = a' ⇒ f(a) = f(a') > > Thanks, > George > > ------------------------------------------------------------------------------ > Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web > API and > much more. Get web development skills now with LearnDevNow - > 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. > SALE \$99.99 this month only -- learn more at: > > http://p.sf.net/sfu/learnmore_122812_______________________________________________ > Rodin-b-sharp-user mailing list > Rodin-b-sharp-user@... > https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user > > ```
 Re: [Rodin-b-sharp-user] Induction in proof From: Hoang, Thai Son - 2013-01-21 09:53 Attachments: Induction0.zip ```Dear George, Attached is a development where I mimic the proof of induction. If you have any problem with the proving interface of Rodin, the following page from the Rodin Handbook will be quite useful. http://handbook.event-b.org/current/html/proving_perspective.html Cheers, Son On 19 Jan 2013, at 17:42, George Zaff > wrote: Thanks that is very helpful. I have another question relating to induction: Out of interest, I was wondering whether it is possible to prove the axiom of induction on natural numbers using Rodin? Ive looked at the proof on the Wikipedia article: https://en.wikipedia.org/wiki/Mathematical_induction#Proof_of_mathematical_induction However, I have been unable to carry out the proof in Rodin. ```