Email Gateway (Aug 18 2022 at 18:36): Email Gateway (Aug 18 2022 at 18:36):From: John Wickerson <jpw48@cam.ac.uk>
Hello,
I'm trying to justify the following induction principle over pairs of naturals. The principle is that if you can show Phi(0,n) for all n, and Phi(m,0) for all m, and if you also show that Phi(m,n+1) and Phi(m+1,n) imply Phi(m+1,n+1) for all m and n, then you can deduce Phi(m,n) for all m and n.
My proof plan is to show that this is an instance of wf induction, but I'm really struggling! (I previously tried to justify it using ordinary mathematical induction, but got stuck on that too.) I would very much appreciate any suggestions people may have for how I can complete this proof.
lemma pair_induction:
fixes \<Phi> :: "nat \<times> nat \<Rightarrow> bool"
assumes "\<And>n2. \<Phi>(0, n2)"
assumes "\<And>n1. \<Phi>(n1, 0)"
assumes "\<And>n1 n2. \<lbrakk>\<Phi>(Suc n1, n2); \<Phi>(n1, Suc n2)\<rbrakk> \<Longrightarrow> \<Phi>(Suc n1, Suc n2)"
shows "\<And>n1 n2. \<Phi>(n1,n2)"
proof -
fix n1 n2
let ?r = "{((m1,m2),(n1,n2)) | m1 m2 n1 n2.
(Suc m1 = n1 \<and> Suc m2 = n2) \<or> (m1 = n1 \<and> Suc m2 = n2)
\<or> (Suc m1 = n1 \<and> m2 = n2)}"
have "wf ?r"
and "\<And>p. (\<And>q. (q, p) \<in> ?r \<Longrightarrow> \<Phi> q) \<Longrightarrow> \<Phi> p" sorry
from wf_induct_rule[OF this]
show "\<Phi>(n1,n2)" sorry
qed
Many thanks!
john
Email Gateway (Aug 18 2022 at 18:37):From: John Wickerson <jpw48@cam.ac.uk>
ps. In the interests of full disclosure, I should point out that I'm really trying to prove the analogous induction principle over the following list-like datatype:
datatype chain =
cNil "assertion"
| cCons "assertion" "command" "chain"
but I thought I would start with naturals first!
Email Gateway (Aug 18 2022 at 18:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Well-founded induction is rather brain-bending, and no amount of experience eliminates that problem. But it isn't difficult to prove using other means:
lemma pair_induction_lemma:
fixes \<Phi> :: "nat \<times> nat \<Rightarrow> bool"
assumes z1: "\<And>n2. \<Phi>(0, n2)"
assumes z2:"\<And>n1. \<Phi>(n1, 0)"
assumes sc: "\<And>n1 n2. \<lbrakk>\<Phi>(Suc n1, n2); \<Phi>(n1, Suc n2)\<rbrakk> \<Longrightarrow> \<Phi>(Suc n1, Suc n2)"
shows "\<And>n1 n2. n1+n2 < k \<Longrightarrow> \<Phi>(n1,n2)"
proof (induct k)
case 0 thus ?case by auto
next
case (Suc k')
note case1 = this
show ?case
proof (cases n1)
case 0 thus ?thesis using z1 by auto
next
case (Suc m1)
note case2 = this
show ?thesis
proof (cases n2)
case 0 thus ?thesis using z2 by auto
next
case (Suc m2)
thus ?thesis using case1 case2
by (auto simp add: sc)
qed
qed
qed
This is only a lemma, now just put k = Suc(n1+n2). For your generalised version, it may suffice for you to introduce an appropriate length function.
Larry Paulson
Email Gateway (Aug 18 2022 at 18:37):From: John Wickerson <jpw48@cam.ac.uk>
Thank you very much Christian. This works perfectly for my case, as follows:
lemma pair_induction:
assumes "\<And>p1 G2. \<Phi> (cNil p1) G2"
assumes "\<And>p2 G1. \<Phi> G1 (cNil p2)"
assumes "\<And>p1 p2 c1 c2 G1 G2. \<lbrakk>\<Phi> G1 (cCons p2 c2 G2); \<Phi> (cCons p1 c1 G1) G2\<rbrakk>
\<Longrightarrow> \<Phi> (cCons p1 c1 G1) (cCons p2 c2 G2)"
shows "\<Phi> G1 G2"
using assms
apply(induction_schema)
apply(pat_completeness)
apply(lexicographic_order)
done
Last updated: Apr 19 2024 at 16:20 UTC