From a1a467a65ff223dd02eb4856d8a9eef60515c4ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Jan 2014 13:48:28 -0800 Subject: [PATCH] refactor(builtin): move congruence theorems to kernel/if_then_else modules Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 1 - src/builtin/congr.lean | 108 ----------------------------- src/builtin/if_then_else.lean | 17 +++++ src/builtin/kernel.lean | 84 ++++++++++++++++++++++ src/builtin/obj/congr.olean | Bin 5986 -> 0 bytes src/builtin/obj/if_then_else.olean | Bin 573 -> 2143 bytes src/builtin/obj/kernel.olean | Bin 16088 -> 20327 bytes src/kernel/kernel_decls.cpp | 9 +++ src/kernel/kernel_decls.h | 27 ++++++++ 9 files changed, 137 insertions(+), 109 deletions(-) delete mode 100644 src/builtin/congr.lean delete mode 100644 src/builtin/obj/congr.olean diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index ff700ebe18..2670aca666 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -94,7 +94,6 @@ 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 deleted file mode 100644 index 5987cfc82d..0000000000 --- a/src/builtin/congr.lean +++ /dev/null @@ -1,108 +0,0 @@ --- 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/if_then_else.lean b/src/builtin/if_then_else.lean index 4f023c92bd..ad5f768531 100644 --- a/src/builtin/if_then_else.lean +++ b/src/builtin/if_then_else.lean @@ -8,4 +8,21 @@ axiom if_false {A : TypeU} (a b : A) : if false then a else b = b theorem if_a_a {A : TypeU} (c : Bool) (a : A) : if c then a else a = a := case (λ x, if x then a else a = a) (if_true a a) (if_false a a) c +-- 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) }) + set_opaque ite true \ No newline at end of file diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 3c3a6120be..94241390e7 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -365,6 +365,90 @@ theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = := boolext (λ H : (∃ x : A, P x), exists_unfold1 a H) (λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) +-- 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 +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 +-- (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) +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))) +-- (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 + set_opaque exists true set_opaque not true set_opaque or true diff --git a/src/builtin/obj/congr.olean b/src/builtin/obj/congr.olean deleted file mode 100644 index 14efc8c49299f6d3fc9c5dc5705c139f6f4fc94e..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 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 zgfMuq83lVOph#!rga9F4|C z0POL+)2xV!BujDgB^ekgF5=WkJeEll2UA3eOB@SPzdXQb;5^$m6k|9vMrga zTti{%O~@)nLVFUyAeS^6tqZCPho z52Oz#V}aHd1Tv$h5y+I=s|0dIPz|IT_WDMvrx!#Uq6O}HYBO|0jo5ZgZY<4g&~7-p zqFLHETOw&z=tB}X`&-W5<=S(T+5^7>(Sc~MFqml#O6nR_z{e1}8_rmF^8{LjPXPnk zJ_A&@=YTD0UjViVHvzW^UjptDZUMg87RmB39wsAPjoGLAHQ@#eqIzxlj@bv)^6h-$ zMXc&_vimkqkw@u72Y1`G--Ro~Gf1bza4@>A62oCCvyB*s5R7&NMCN!M!#wRWQ;J?g z46TUhKjtjPnSZkFPNuzyeNJ%d5IVx;`=rD5u>3oqS-FOBrJRBBA(VL~lE(x4&g0O7 zy*60gDU?h_;~KZTOXWNnFhgoBxU%NYuK>>>81%&Ei7$&VNsBy#cAnpF0`eiFoi@xT zCII8xpN+|EG+#eWj-l80%K5Eq%@xgw@7z!{4a#qin~*Z4PL4UtK8jeG46Z-$aN747 z=YaD&1Z2@iZUemE1EWO)eJqK}0+{=z<&)GP#-$eVTzZ!W5T8Y6BjUeUZPo$o2GCHaHdCS z#EmP0>?Bur3pD3C!J^HT7}jCYRO%GGUC}Vahf^yPY)9YRN6=QMRQqkPVwhqt0wHQn zHQ^eU+-{zw(z57gvm&MsOLIjLStKWM`-&{D&AlmO`XFLx8bU%BOdp_m1|%-2k&)n% zeBA*)UqUFvw0D8N0Rk;Ii)Z_bkVH3Y??if{cZG;k*8{%;OzC|ZE3;xc@qS=D{jx&mO65B?S zvLua2nzIr_k=y#Tg2QaigZ)|FW`{+I663fBSZgq(jj1u^yzO$nT?JvB8_KeUPX#aL z^C!|uQ|jW08?lG3w9rqsf%h}hHzMTrg7|8e^V4R@6fgwlKv>$r1+B@P3y?aP1`lRy z1`Y{|zQyA=jl!Nr9r0)6mWp-{_R3h7o`#V5E-8xOU^;LL=nt@i7d~)I#Ae?>5c>+` zH;`i>Ke6KB1FO!Rz~avj?wF8YW6^6al22}|Zm+)5yZS1=6L=!fV@ z`MSM9v>&2se}AJ`V?^Xqh`MsKLbPM*h8)=Y$u4e}8-Fx;e?EPF24IIzKv-(W^D;)~ zdi{*-h6ZMY=Jew(ftkU$h-VH)ec!R5Kb19iv~U0hfhO$>u)i$yX7yl4YZ5!wzQ*lj z(NU<)fi!M1aDE4Ye`X+md?p58L*|%}=r~VfLfv_hPkaevG78y$|8Fj#v`i{biA?b| zWs_#CmgMUlL2%uVLbPk!@%SgmQ6ce)<$|>c(Ylu{7Uw}05u)szKn;e09j}Ja2?%9I z0j#4n?t8F*$fr^5giO3Duc(~jBt#1u_Z{S$jFA=|NXNyMU}VNcbzAS626F=CnYnW@ za}3k_*xIfITklYMG2`k@VfE$!Z-MAq#8mEU@{v0f-V_{M{!LLa<}PD+$dCv^%1(j~ zfwZKy-yjb)+js6-@&XCbX+PYE^B!6BynT;m-!9NQb4P%^0p1xPU%PrA6pQ5uWFx*+ z3QUrWCiOENsKT=2B3(oJ4E*yqTYV{7*ueWu(`f;rp>$Sm0k;+b&g?XMX#}>*EqK&a zU+Z1jAd#Z&&SZxCINOrZb(r#TKVvX}V>F?62e>Z4!2s_O=%@U>0^?!LCo0Rt>#1G= z+<*o3S0~Q`R`V%EU@|GaKs7=SB^M9S*!u)}V>bqPe}J0;L^0*6Z(6NIBt!M3#Rp+< zt_>lFy)_F*$IHuB-AtzHX1Yb&_YsDUVUQRNgeba<{yYqh1|NS4JbWa;M+4j}(9KW{ zrIF}Al57#7>g)<=;2d{8y`>=3nv*sy+Eheatv^&NQ&eK1%73s<$hFDWP7)5$k-t^@ zG5O&=Zw$|d@8qm8Sfsl+T`RgHZRdw%r9QGt-CVd6+pKnR!5(LY#4j@@PYU$$dn&-E z1Jr94WuJxUTZGRE#BD{K#53D5X*!*T4(G<}g+y0?tMPjrupFXR!83cDzAk9|)Z~AP zk)sF$$9`mt;@8v2JRv)|wzSWs=$7k?ZS>-KSfF*pT@~^Iu8>JmNS7K+WhAA(FZ@t8 SRoixH$&QGGB(6F+xZyva281~P delta 12 TcmaDpkMTzBh8cE~)%_g+Drp6) diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index f4101dfb03..70b5aa39d1 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -100,4 +100,13 @@ MK_CONSTANT(not_exists_elim_fn, name("not_exists_elim")); MK_CONSTANT(exists_unfold1_fn, name("exists_unfold1")); MK_CONSTANT(exists_unfold2_fn, name("exists_unfold2")); MK_CONSTANT(exists_unfold_fn, name("exists_unfold")); +MK_CONSTANT(imp_congrr_fn, name("imp_congrr")); +MK_CONSTANT(imp_congrl_fn, name("imp_congrl")); +MK_CONSTANT(imp_congr_fn, name("imp_congr")); +MK_CONSTANT(or_congrr_fn, name("or_congrr")); +MK_CONSTANT(or_congrl_fn, name("or_congrl")); +MK_CONSTANT(or_congr_fn, name("or_congr")); +MK_CONSTANT(and_congrr_fn, name("and_congrr")); +MK_CONSTANT(and_congrl_fn, name("and_congrl")); +MK_CONSTANT(and_congr_fn, name("and_congr")); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 8e9768323f..69a031edb2 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -291,4 +291,31 @@ inline expr mk_exists_unfold2_th(expr const & e1, expr const & e2, expr const & expr mk_exists_unfold_fn(); bool is_exists_unfold_fn(expr const & e); inline expr mk_exists_unfold_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_exists_unfold_fn(), e1, e2, e3}); } +expr mk_imp_congrr_fn(); +bool is_imp_congrr_fn(expr const & e); +inline expr mk_imp_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_imp_congrl_fn(); +bool is_imp_congrl_fn(expr const & e); +inline expr mk_imp_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congrl_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_imp_congr_fn(); +bool is_imp_congr_fn(expr const & e); +inline expr mk_imp_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_imp_congr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_or_congrr_fn(); +bool is_or_congrr_fn(expr const & e); +inline expr mk_or_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_or_congrl_fn(); +bool is_or_congrl_fn(expr const & e); +inline expr mk_or_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congrl_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_or_congr_fn(); +bool is_or_congr_fn(expr const & e); +inline expr mk_or_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_congr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_and_congrr_fn(); +bool is_and_congrr_fn(expr const & e); +inline expr mk_and_congrr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrr_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_and_congrl_fn(); +bool is_and_congrl_fn(expr const & e); +inline expr mk_and_congrl_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congrl_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_and_congr_fn(); +bool is_and_congr_fn(expr const & e); +inline expr mk_and_congr_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_and_congr_fn(), e1, e2, e3, e4, e5, e6}); } }