From a0a92f11b7b19fc25120dfaab8464343beb568ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Jan 2014 13:37:36 -0800 Subject: [PATCH] feat(builtin/congr): add congruence theorems for contextual simplification Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 1 + src/builtin/congr.lean | 108 ++++++++++++++++++++++++++++++++++++ src/builtin/obj/congr.olean | Bin 0 -> 5986 bytes 3 files changed, 109 insertions(+) create mode 100644 src/builtin/congr.lean create mode 100644 src/builtin/obj/congr.olean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index 2670aca66..ff700ebe1 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -94,6 +94,7 @@ add_theory("Int.lean" "${CMAKE_CURRENT_BINARY_DIR}/if_then_else.olean") add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean") add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean") add_theory("cast.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") +add_theory("congr.lean" "${CMAKE_CURRENT_BINARY_DIR}/Nat.olean") update_interface("kernel.olean" "kernel" "-n") update_interface("Nat.olean" "library/arith" "-n") diff --git a/src/builtin/congr.lean b/src/builtin/congr.lean new file mode 100644 index 000000000..5987cfc82 --- /dev/null +++ b/src/builtin/congr.lean @@ -0,0 +1,108 @@ +-- Congruence theorems for contextual simplification + +-- Simplify a → b, by first simplifying a to c using the fact that ¬ b is true, and then +-- b to d using the fact that c is true +theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) +:= or_elim (em b) + (λ H_b : b, + or_elim (em c) + (λ H_c : c, + calc (a → b) = (a → true) : { eqt_intro H_b } + ... = true : imp_truer a + ... = (c → true) : symm (imp_truer c) + ... = (c → b) : { symm (eqt_intro H_b) } + ... = (c → d) : { H_bd H_c }) + (λ H_nc : ¬ c, + calc (a → b) = (a → true) : { eqt_intro H_b } + ... = true : imp_truer a + ... = (false → d) : symm (imp_falsel d) + ... = (c → d) : { symm (eqf_intro H_nc) })) + (λ H_nb : ¬ b, + or_elim (em c) + (λ H_c : c, + calc (a → b) = (c → b) : { H_ac H_nb } + ... = (c → d) : { H_bd H_c }) + (λ H_nc : ¬ c, + calc (a → b) = (c → b) : { H_ac H_nb } + ... = (false → b) : { eqf_intro H_nc } + ... = true : imp_falsel b + ... = (false → d) : symm (imp_falsel d) + ... = (c → d) : { symm (eqf_intro H_nc) })) + + +-- Simplify a → b, by first simplifying b to d using the fact that a is true, and then +-- b to d using the fact that ¬ d is true. +-- This kind of congruence seems to be useful in very rare cases. +theorem imp_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a → b) = (c → d) +:= or_elim (em a) + (λ H_a : a, + or_elim (em d) + (λ H_d : d, + calc (a → b) = (a → d) : { H_bd H_a } + ... = (a → true) : { eqt_intro H_d } + ... = true : imp_truer a + ... = (c → true) : symm (imp_truer c) + ... = (c → d) : { symm (eqt_intro H_d) }) + (λ H_nd : ¬ d, + calc (a → b) = (c → b) : { H_ac H_nd } + ... = (c → d) : { H_bd H_a })) + (λ H_na : ¬ a, + or_elim (em d) + (λ H_d : d, + calc (a → b) = (false → b) : { eqf_intro H_na } + ... = true : imp_falsel b + ... = (c → true) : symm (imp_truer c) + ... = (c → d) : { symm (eqt_intro H_d) }) + (λ H_nd : ¬ d, + calc (a → b) = (false → b) : { eqf_intro H_na } + ... = true : imp_falsel b + ... = (false → d) : symm (imp_falsel d) + ... = (a → d) : { symm (eqf_intro H_na) } + ... = (c → d) : { H_ac H_nd })) + +-- (Common case) simplify a to c, and then b to d using the fact that c is true +theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a → b) = (c → d) +:= imp_congrr (λ H, H_ac) H_bd + +-- In the following theorems we are using the fact that a ∨ b is defined as ¬ a → b +set_opaque or false +theorem or_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d) +:= imp_congrr (λ H_nb : ¬ b, congr2 not (H_ac H_nb)) H_bd +theorem or_congrl {a b c d : Bool} (H_ac : ∀ (H_nd : ¬ d), a = c) (H_bd : ∀ (H_na : ¬ a), b = d) : (a ∨ b) = (c ∨ d) +:= imp_congrl (λ H_nd : ¬ d, congr2 not (H_ac H_nd)) H_bd +set_opaque or true +-- (Common case) simplify a to c, and then b to d using the fact that ¬ c is true +theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b = d) : (a ∨ b) = (c ∨ d) +:= or_congrr (λ H, H_ac) H_bd + +-- In the following theorems we are using the fact hat a ∧ b is defined as ¬ (a → ¬ b) +set_opaque and false +theorem and_congrr {a b c d : Bool} (H_ac : ∀ (H_b : b), a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d) +:= congr2 not (imp_congrr (λ (H_nnb : ¬ ¬ b), H_ac (not_not_elim H_nnb)) (λ H_c : c, congr2 not (H_bd H_c))) +theorem and_congrl {a b c d : Bool} (H_ac : ∀ (H_d : d), a = c) (H_bd : ∀ (H_a : a), b = d) : (a ∧ b) = (c ∧ d) +:= congr2 not (imp_congrl (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)) (λ H_a : a, congr2 not (H_bd H_a))) +set_opaque and true +-- (Common case) simplify a to c, and then b to d using the fact that c is true +theorem and_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d) : (a ∧ b) = (c ∧ d) +:= and_congrr (λ H, H_ac) H_bd + + +-- Perhaps, we should move the following theorem to the if_then_else module +import if_then_else + +-- Simplify the then branch using the fact that c is true, and the else branch that c is false +theorem if_congr {A : TypeU} {b c : Bool} {x y u v : A} (H_bc : b = c) (H_xu : ∀ (H_c : c), x = u) (H_yv : ∀ (H_nc : ¬ c), y = v) : + (if b then x else y) = (if c then u else v) +:= or_elim (em c) + (λ H_c : c, calc (if b then x else y) = (if c then x else y) : { H_bc } + ... = (if true then x else y) : { eqt_intro H_c } + ... = x : if_true _ _ + ... = u : H_xu H_c + ... = (if true then u else v) : symm (if_true _ _) + ... = (if c then u else v) : { symm (eqt_intro H_c) }) + (λ H_nc : ¬ c, calc (if b then x else y) = (if c then x else y) : { H_bc } + ... = (if false then x else y) : { eqf_intro H_nc } + ... = y : if_false _ _ + ... = v : H_yv H_nc + ... = (if false then u else v) : symm (if_false _ _) + ... = (if c then u else v) : { symm (eqf_intro H_nc) }) diff --git a/src/builtin/obj/congr.olean b/src/builtin/obj/congr.olean new file mode 100644 index 0000000000000000000000000000000000000000..14efc8c49299f6d3fc9c5dc5705c139f6f4fc94e GIT binary patch literal 5986 zcmcIoTW?fV6h8a3Go5L{#KZz)VCVqTHiF0{jR;->132X>2nwhfr|l_>%%x1Hg_=l8 z5tSzs-;BS4Cw(;0C-v1ge}#!YX>@(xI_K;&yF;-go@Cany>5Hm_T`*bJ*YNkYxTej zA5&}0wb~u;X3%a1buS#9t9HE34bPWhWxCb8-fnwozv}t^u~w_@2|lIjX@5FGW+J3q zsZNVTxze2ScKUv^)$u$dOuy*+!7Y^{p&z&p$*CDCs4XAlbPnF0h#O+$2mgh8O0ao=yXD?z>1z);NW1f<^f>&NIA<9z#ymF29(eCSOk_9 z0;P_)QXm%qcDS5KKOc(}#Hsm(sd*_{{N%_@`FE6(v5sayDRR7pD7-hje7_ycN}t5f zb|D3~I+a?p({3r1M#m(r=rK6oR(gI^99U|Exh8D~V1aen2Q1ne4EHLB z@6T52^I<7j`c+kj8OA&b?11AuiG?t+v=vrDo7JYR4DIZySVll5FK*uwNI55{NoQXA zT4teVlZ7U|#ISYIXxNEG1M6D>x)uiriB`vO1VGba!(i`rg#oG2sI}=ktFnhx7y@?; z;KW*`fB-YOM)rG^4|+_VE-6<8>=6K_qC&O}MN^op2t?licn{zhz$J!p3Mjkr46t`5 z8*}*Q({JSI+P>@DM9KV*d-sgTY1pz%VLGu0qDIT!TA6nvFu8YBQ_;RA<6c>&pE3Ydv__XMaFm; zfIG##|Dmu`u&#w=Dlzm}&oVF#hMc!!4mXnP7_vHFJ}F@<5bfD;+-z2QC7Gol`x|JV zags>q=;j5mFFMt<0etN!YOAu^VVgn!0l;~HF95!ZHWoDP>WyVR`$`e^`T_XZjrbY* zaD-H%uUhmqi@t7AZi$bOY`Hq(k!u|P3Ak<05a;kkj&z>Vlq*G1VF56z^K){&ZOI)3 z`=(q76SrRKK6%@O*g&{R5>Lb{ry^|QQRmo3-(wuQ2=q9BF3b}aJ!#Q5Ey{@W9?RAk zU~#{Nz+C`_zYGlF<1UV8SZ;TW>;Q+Mm{vcegu4s%4QTW#P8fETxDBE_t?PJ!&BerF z($uxi;_x*2fpedOoQA<}RP-%NWw$H!BB*+raB2Rk-N1decRI9d`k?mm^|U+8J_7iW@mv9_?q0R%HH-3uSAq9IO}6)d2E;8r>>!9}?*RJ_AP(YP8Q37I zO^Ft5Eyz>$wY=8YrB=jT{Q#cyHLU|rH1_WpCmQ=hj5RbZHZ!6vNp#u@ure7^15h(; z?4KwA@H2a415nO*m*b5XbH-(0#;yhmvAM|Z<7&XGDdhl$iTVn2dma^0d0i#9Ea zmoTII?k!OD{^i8=7dU?dXg+@f+B=`g>tbJ+Pe}g*z|=5_T78%>{m~Zuk&L>Vl}j$p z)KjgwKbet5%&r+>o)p#BSPCpzfscVE*Iam{pnOqt17k4pkwPooN6LZ-F`k-!S*gud zIyZu*G?l#7@m4;ot55q_9;+(`+fja-}*ii%VTjgFMI3Xw7l-rco6a_?<5(}ihI&NIHROoXnONMMrT8vr;t31M4C=KY zqx#4NTAzMvrSsM@Pv{a1sCnAk9f=!;sat0}lS&p=&jc;lOY{`nH5VMC=Q!s34ks2A4I1 z