From cc4148a98d4ed91e4523c0ea378d7f0cd32457ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Feb 2014 22:05:57 -0800 Subject: [PATCH] feat(builtin/num): primitive recursion theorem Signed-off-by: Leonardo de Moura --- src/builtin/num.lean | 122 +++++++++++++++++++++++++++++++++++--- src/builtin/obj/num.olean | Bin 15973 -> 16323 bytes 2 files changed, 114 insertions(+), 8 deletions(-) diff --git a/src/builtin/num.lean b/src/builtin/num.lean index 7f689bdb1b..74b1263055 100644 --- a/src/builtin/num.lean +++ b/src/builtin/num.lean @@ -67,13 +67,15 @@ theorem succ_inj {a b : num} : succ a = succ b → a = b show a = b, from rep_inj rep_eq -theorem succ_nz (a : num) : succ a ≠ zero +theorem succ_nz (a : num) : ¬ (succ a = zero) := assume R : succ a = zero, have Heq1 : S (rep a) = Z, from abst_inj inhab (succ_pred a) zero_pred R, show false, from absurd Heq1 (S_ne_Z (rep a)) +add_rewrite num::succ_nz + theorem induction {P : num → Bool} (H1 : P zero) (H2 : ∀ n, P n → P (succ n)) : ∀ a, P a := take a, let Q := λ x, N x ∧ P (abst x inhab) @@ -134,6 +136,8 @@ theorem lt_nrefl (n : num) : ¬ (n < n) (assume N : n < n, lt_elim N (λ P Pred Pn nPn, absurd Pn nPn)) +add_rewrite num::lt_nrefl + theorem lt_succ {m n : num} : succ m < n → m < n := assume H : succ m < n, lt_elim H @@ -235,6 +239,8 @@ theorem zero_lt_succ_n {n : num} : zero < succ n (λ (n : num) (iH : zero < succ n), lt_to_lt_succ iH) +add_rewrite num::zero_lt_succ_n + theorem lt_succ_to_disj {m n : num} : m < succ n → m = n ∨ m < n := assume H : m < succ n, lt_elim H @@ -290,11 +296,11 @@ definition simp_rec_fun {A : (Type U)} (x : A) (f : A → A) (n : num) : num → definition simp_rec {A : (Type U)} (x : A) (f : A → A) (n : num) : A := simp_rec_fun x f (succ n) n -theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num) - : (∃ fn, simp_rec_rel fn x f n) - ↔ - (simp_rec_fun x f n zero = x ∧ - ∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m)) +theorem simp_rec_def {A : (Type U)} (x : A) (f : A → A) (n : num) + : (∃ fn, simp_rec_rel fn x f n) + ↔ + (simp_rec_fun x f n zero = x ∧ + ∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m)) := iff_intro (assume Hl : (∃ fn, simp_rec_rel fn x f n), obtain (fn : num → A) (Hfn : simp_rec_rel fn x f n), @@ -309,8 +315,8 @@ theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num) show (∃ fn, simp_rec_rel fn x f n), from exists_intro (simp_rec_fun x f n) H1) -theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n : num) - : ∃ fn, simp_rec_rel fn x f n +theorem simp_rec_ex {A : (Type U)} (x : A) (f : A → A) (n : num) + : ∃ fn, simp_rec_rel fn x f n := induction_on n (let fn : num → A := λ n, x in have fz : fn zero = x, @@ -372,9 +378,109 @@ theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n : num) show ∃ fn, simp_rec_rel fn x f (succ n), from exists_intro fn1 (and_intro f1z f1s)) +theorem simp_rec_lemma1 {A : (Type U)} (x : A) (f : A → A) (n : num) + : simp_rec_fun x f n zero = x ∧ + ∀ m, m < n → simp_rec_fun x f n (succ m) = f (simp_rec_fun x f n m) +:= (simp_rec_def x f n) ◂ (simp_rec_ex x f n) + +theorem simp_rec_lemma2 {A : (Type U)} (x : A) (f : A → A) (n m1 m2 : num) + : n < m1 → n < m2 → simp_rec_fun x f m1 n = simp_rec_fun x f m2 n +:= induction_on n + (assume H1 H2, + calc simp_rec_fun x f m1 zero = x : and_eliml (simp_rec_lemma1 x f m1) + ... = simp_rec_fun x f m2 zero : symm (and_eliml (simp_rec_lemma1 x f m2))) + (λ (n : num) (iH : n < m1 → n < m2 → simp_rec_fun x f m1 n = simp_rec_fun x f m2 n), + assume (Hs1 : succ n < m1) (Hs2 : succ n < m2), + have H1 : n < m1, + from lt_succ Hs1, + have H2 : n < m2, + from lt_succ Hs2, + have Heq1 : simp_rec_fun x f m1 (succ n) = f (simp_rec_fun x f m1 n), + from and_elimr (simp_rec_lemma1 x f m1) n H1, + have Heq2 : simp_rec_fun x f m1 n = simp_rec_fun x f m2 n, + from iH H1 H2, + have Heq3 : simp_rec_fun x f m2 (succ n) = f (simp_rec_fun x f m2 n), + from and_elimr (simp_rec_lemma1 x f m2) n H2, + calc simp_rec_fun x f m1 (succ n) = f (simp_rec_fun x f m1 n) : Heq1 + ... = f (simp_rec_fun x f m2 n) : congr2 f Heq2 + ... = simp_rec_fun x f m2 (succ n) : symm Heq3) + +theorem simp_rec_thm {A : (Type U)} (x : A) (f : A → A) + : simp_rec x f zero = x ∧ + ∀ m, simp_rec x f (succ m) = f (simp_rec x f m) +:= have Heqz : simp_rec_fun x f (succ zero) zero = x, + from and_eliml (simp_rec_lemma1 x f (succ zero)), + have Hz : simp_rec x f zero = x, + from calc simp_rec x f zero = simp_rec_fun x f (succ zero) zero : refl _ + ... = x : Heqz, + have Hs : ∀ m, simp_rec x f (succ m) = f (simp_rec x f m), + from take m, + have Hlt1 : m < succ (succ m), + from lt_to_lt_succ (n_lt_succ_n m), + have Hlt2 : m < succ m, + from n_lt_succ_n m, + have Heq1 : simp_rec_fun x f (succ (succ m)) (succ m) = f (simp_rec_fun x f (succ (succ m)) m), + from and_elimr (simp_rec_lemma1 x f (succ (succ m))) m Hlt1, + have Heq2 : simp_rec_fun x f (succ (succ m)) m = simp_rec_fun x f (succ m) m, + from simp_rec_lemma2 x f m (succ (succ m)) (succ m) Hlt1 Hlt2, + calc simp_rec x f (succ m) = simp_rec_fun x f (succ (succ m)) (succ m) : refl _ + ... = f (simp_rec_fun x f (succ (succ m)) m) : Heq1 + ... = f (simp_rec_fun x f (succ m) m) : { Heq2 } + ... = f (simp_rec x f m) : refl _, + show simp_rec x f zero = x ∧ ∀ m, simp_rec x f (succ m) = f (simp_rec x f m), + from and_intro Hz Hs + +definition pre (m : num) := if m = zero then zero else ε inhab (λ n, succ n = m) + +set_option simplifier::unfold true + +theorem pre_zero : pre zero = zero +:= by simp + +theorem pre_succ (m : num) : pre (succ m) = m +:= have Heq : (λ n, succ n = succ m) = (λ n, n = m), + from funext (λ n, iff_intro (assume Hl, succ_inj Hl) + (assume Hr, congr2 succ Hr)), + calc pre (succ m) = ε inhab (λ n, succ n = succ m) : by simp + ... = ε inhab (λ n, n = m) : { Heq } + ... = m : eps_singleton inhab m + +definition prim_rec_fun {A : (Type U)} (x : A) (f : A → num → A) +:= simp_rec (λ n : num, x) (λ fn n, f (fn (pre n)) n) + +definition prim_rec {A : (Type U)} (x : A) (f : A → num → A) (m : num) +:= prim_rec_fun x f m (pre m) + +theorem prim_rec_thm {A : (Type U)} (x : A) (f : A → num → A) + : prim_rec x f zero = x ∧ + ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m +:= let faux := λ fn n, f (fn (pre n)) n in + have Hz : prim_rec x f zero = x, + from have Heq1 : simp_rec (λ n, x) faux zero = (λ n : num, x), + from and_eliml (simp_rec_thm (λ n, x) faux), + calc prim_rec x f zero = prim_rec_fun x f zero (pre zero) : refl _ + ... = prim_rec_fun x f zero zero : { pre_zero } + ... = simp_rec (λ n, x) faux zero zero : refl _ + ... = x : congr1 zero Heq1, + have Hs : ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m, + from take m, + have Heq1 : pre (succ m) = m, + from pre_succ m, + have Heq2 : simp_rec (λ n, x) faux (succ m) = faux (simp_rec (λ n, x) faux m), + from and_elimr (simp_rec_thm (λ n, x) faux) m, + calc prim_rec x f (succ m) = prim_rec_fun x f (succ m) (pre (succ m)) : refl _ + ... = prim_rec_fun x f (succ m) m : congr2 (prim_rec_fun x f (succ m)) Heq1 + ... = simp_rec (λ n, x) faux (succ m) m : refl _ + ... = faux (simp_rec (λ n, x) faux m) m : congr1 m Heq2 + ... = f (prim_rec x f m) m : refl _, + show prim_rec x f zero = x ∧ ∀ m, prim_rec x f (succ m) = f (prim_rec x f m) m, + from and_intro Hz Hs + set_opaque simp_rec_rel true set_opaque simp_rec_fun true set_opaque simp_rec true +set_opaque prim_rec_fun true +set_opaque prim_rec true end definition num := num::num diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean index b266bd7fac099e46667c9a1ac7bf7722bfe34ea2..ff668ea828d940d75ee1856e4a693f9d2ce0bf1c 100644 GIT binary patch delta 2483 zcmai0U2IfE6uxt3+@*BWKMSP`lxk^h+3mIqEiKeiA)sg*pv#XYAWbP-yJ(@58nvk@ zK4?rDc;NV8qF`SQK0u67H2Bg4@qvWIm|!IGpazv9t)>(cA3Wcg>%Hwtu*sf&_nb3l zzVpr8x%2bL#OS%%RYeEWy^eA4cP!IC&^4Iuq5N3oLvR$(Pq8>XA6u%<(ld!l&8ZyQ zj+kzz>FQ#dsxtI?tXj2GGO>idj72Q!EDCdu+Jz!-3)~GD7PyCzUMuifc*m-=o9XTC z${ZdVJOYQKQ;)&60T)yO2D5d3AW}c{Nsis>aY)@zTh_u)DSQ zFoxv{+L#)qziVqE!*GmvGbIyM(Vgs2YN#(u znXdG!5GRiGlyq>2q1WPzfVRb#7tm5)44ttBY}63#sNcBwBs6g}e#3q>&@Wruwi2Pz|Av;+z50SBoc^yOALTL+ zPk;d`PabI>$IzSA82c&U6wEb|;=KQSg^~UkW?anu(yjtLvJD$}GG{)fZu^=a<%>uhee(=)8S&fzGaeWSJ!{ zg_A*fG^)qxm(}m8Z|IFRb?RF>zosnz8t;(7S6Cuc*PZkON4}@Lh7Q$9dmC1SCgA>& zjyDWHISF{1jl0PgL|bPCdu_u*_l^7d>PdQ{u{eE)v-F+pDs!>|-eV{zTA{R-He~p; zuZKq>OX@%9*7|59KPWmwHyYQDLRvk;#!8E&(tl-@`cuN-pfAHnlXhm|d;@V1lZYcd zFM>~YQ(Ms2j0kg+Bkn$=->Vn}zU;f5TXT{*WI}WJV#IYjjID$H;FWp6pe*H3&KtzY zlzw-IgLjvy@u*0$DdW!L!&<<2a1FB)-!%9GLtEUYF6>`@cg-?ARk7&mpRAL z-_e@p5vF>sxtaIzugxo>6YMsPGU_RTVRsu+O(Q+J?vurx4E0?&t{_JvUEihK>o$+( zVOkfi}x^*Tr-Ci)ppOxni|y|G#v<_ZHb`ZW#|yCG*E`^F{Ec z^97Z|#%$*|pgbgNm!iU!sG6a8i??$%V7sI4{g62>bA!o`ukQ=-sw#)(QX{`+5+i%9` zWNS?bCzv@w7h9tx;|!hI1#Hxtfc8uL7X9A3NoDA{#4_9iuxa&P@KEm~$zF9%1KNAQ z8Ajec-~)JZ)kz=i9{}bX1kBzl&HvO+nyOwDwm8Fhxq6S18%lGw4|F3}ZKJ0*Ec*xI CZ+vwC delta 2231 zcmah~OH74XbS}r1|;Dj2-YYOZPbvE zXv~SB3yp~`teRAs=%$-$G{&ezQxan|=?1k{r$Se_squd2j{gi}ql-B?|2f||_dDM` z|39BD|Gc!mTTP#J#2Puci@yA#Il@QAVIrhG-~|PmczC>=jX~zk=Qh z?AzB{A%sw!#)!;vxFNb-nN2(8nyv@3i#aV+vNH;VScUoB>x|F9QD-Qtrq(n(T2t>k z<8^wY;X!(~=A;R4*7V5Gk`J7GN4%=efL?7Vmg{u6p+sJ!YYnxT+;!KW1g2LXQdVPj_T>Z03D1oWPtGjN&mt$(I<+<4 z@3Du{NMnv%qbD0L$S*0QsaAeXolQj<-@XAsZZrSw2c&a%xRa3?l$1kalmWvsw$ zN2}r*A|GD_l5sMjU9`w}8cEF;ZDry!?&P3fOegJ_N3}^`wd`l1bP`2c3YWLQ-N9Hg z)peaQm#|JUDHc&D8%L+aM8q*#A>CP~oXPRwh55xW9*rU}5M2wGg$@3J%wK$axa`9! z;?BlL>1435ihK8-#SP7u#4NUf2=y&}(z+zKsH3gbEcLmz;zBI74scZuyI$vEKy`rD z+dj%gOx;3Y0~p2cz%6>_&_gnbK0Z{kj9K+DnAn?OSshCd1aG|+r0f6S?tFH|iws`o z?Je)NgBBucIk>9vj_c#RGL!rOgJ;XB~_?YFL*i~An(se^g|IjM|sQjF23z@0ys4A28H>6j)<$29S> z=)wPh)B528e+)Vl8w;KEK!QqVS*6q?saBNHIOUoDyCAk@j1$DOPJ-pnmEzaHez}4% zzWi^BUDaWj@r3h-O;BXUWMxvIdsbsKvEcHvO7xqUK8=0?yRSnoK|Pv4NbJ}Eu(8*` zwmD_~n#(+k=y0Cy?Wppchx-Ecbrj~UpDq979w-@;FZ=+g-0) Zj)ljCGqX623b6vS+C4LNd~zx*{sy=ESzG`B