From fbaf6e887ff6bb37dd52111e5dccbdb9b6fc0c86 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jan 2014 14:03:51 -0800
Subject: [PATCH] refactor(builtin/kernel): put the congruence theorems in a
 format that is easier for the simplifier to process

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/kernel.lean      |  10 +++++-----
 src/builtin/obj/kernel.olean | Bin 25218 -> 25296 bytes
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index 941989026c..2b324829ec 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -428,7 +428,7 @@ theorem imp_congrr {a b c d : Bool} (H_ac : ∀ (H_nb : ¬ b), a = c) (H_bd : 
 -- 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)
+theorem imp_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : (a → b) = (c → d)
 := or_elim (em a)
       (λ H_a : a,
           or_elim (em d)
@@ -462,8 +462,8 @@ theorem imp_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_c : c), b = d)
 -- 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
+theorem or_congrl {a b c d : Bool} (H_bd : ∀ (H_na : ¬ a), b = d) (H_ac : ∀ (H_nd : ¬ d), a = c) : a ∨ b ↔ c ∨ d
+:= imp_congrl H_bd (λ H_nd : ¬ d, congr2 not (H_ac H_nd))
 -- (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
@@ -471,8 +471,8 @@ theorem or_congr {a b c d : Bool} (H_ac : a = c) (H_bd : ∀ (H_nc : ¬ c), b =
 -- 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)))
+theorem and_congrl {a b c d : Bool} (H_bd : ∀ (H_a : a), b = d) (H_ac : ∀ (H_d : d), a = c) : a ∧ b ↔ c ∧ d
+:= congr2 not (imp_congrl (λ H_a : a, congr2 not (H_bd H_a)) (λ (H_nnd : ¬ ¬ d), H_ac (not_not_elim H_nnd)))
 -- (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
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 19d0ab9bdf9ce7af2714e7d5a7f4b609e8483cb4..df77b2434f850228b853334ade621e1529534f5d 100644
GIT binary patch
delta 1021
zcmZ9KUr1AN6vywG-fMp*a}CT5WYU~&nfM2^bc#eMYq~k-zq#w~yym|N4XL1BEXv9r
zg9D)!rSwOsmmreB$RK>_K@934$fw@4Kq8{ZsB?aI(VxLSoO{mioZt7H^SiJDYb)>&
zTXyyjNQ%jy&?RgxuzStIJ|<kL0f~RvZl;4FGm?y2eAePK_p-wjAjlfZ!7W(DFTqwA
z!KP3IQaBwt3SoR7auu)2bVW+%OnJ~lgdw(T8E@$?TNuMw+IkI6QC<Pn2)5>B$rbD$
z!Sl^FEDP+0bLa}!!#L{UvYb&49b_CQNMW1}2k?1YCaCx`>?8WxKEe!oBlq0t9t{D;
zg=)G{&es^X@pGiQ=CSBVl-4{M<To85kZ5KjTMyWBGR&eWV@R8rh`68>N7{pmN-_Bk
zF11&ah)?YY;5s@x)*XY2Nen=AZIs!?qmXAXw{y9WH1bF9Ukflwo7o*_yvA>x)#;&6
zu;T;zy7H~}*?dQkjCxNo*_EFyud_Vk#v~>?U4>zxH@($u7blntnco>=7g@N}6*3xl
zgO+Y?ps9NUtXL7vBL<?8y>_aS8siLU(@ii<5fnQ<ik3TUvgr&5q}qRXOyM8Vda$Ff
zXA<_{i=HYsFIKTJD*3F*PY~}*5fLj#Y?vQ&Sj%}O5)W03UCBXztbwXriJc^F$4a0P
zJ*t-&Q9Gas=T#5gw5HmL8|tzpL5Ye^s=0!az^#NGU-eeP5N5{xki=koALuw1cfv4U
zjh}!~%+MyF4=1&%x{D&0ap^ymB4U&-;&%f4jMEBvH;RT|wFWA4C^1f4Oq5u}pr(Hd
znIa+0a1-nLYOMU;q%4Y@=H?}34lnm<-UT-A77;Vg5}=L0=LyF1<MaHXOk=k0gj-mu
f-+(!MsTac{&K}Oi9sO486Fy=7v!^-S-yi)284u05

delta 1010
zcmZ9KOH5Ny5QgtuxVJu#woxmPKvf<sK?OCSP!S^mp@qIc3cbCh4=gG|3?@oKP(h>7
z?MMSch~OhpH^#@pn1~zJ7+;ACiED_78&|q;=3I!6Cg;0z{y8(9Idk4Fz}Nyj!IrXk
zQc~rn?tvbOfBR`E87w4vgdP`igOG8l#g(NgWXo<AB3Rt|9Tw5%^+5_#-XNU8m)>S@
zVTP~Jv8Zrb5w9ejbRJR!sfO{HmSSd{z*b)x1}Sbk<>>e2n3TP&r*PD>8Oz-pVFc^_
zwJ?mM{&LGnb{$~!5hNGB@w;)hWh<HkE<p4IzQH6`2Opq6v@ZXzE{rndryQBVn8VDr
zs$)hkr&xIIWL>T&NXkQ|==l*_cF~D(K`XRZ9<yp{?mx?4If=8uE$9eUs7PDoE-trK
zQ87E(cfoD+wtvY>s<Ls7+`A%DZr}@1Cb8l8e9`IzjQl3n*9O3Lgz*lY9aUM&;_9yo
z6;F5MTe(gsAV@~OS2)p;Un#AKdRHg<tC0QnBIZwq7=Ve77)6QpzvB9k*QozJ>LITG
zR%jWr@lt0FaiTN0%|;;uqGM^LnDWRI1l5MnRgq^=<RQ*2)%-hXa(lXJ!G<@wu7eq^
z;mYDY9A#mY^I5rxAaP@=@MN=P!M<>wbvLV$#<0^;H(@$lM_E3F&k@~P863s)S}F04
z)(-XfLvzwU6-0802P5-lzBx5YRdWV4f`?<dXxH~a5`%gZJ+>)*Cq(hJZigOR(g&dz
z1JNs><Hu;_p-~ab82hhE;W1K|@RI?4%c~V$CPUS*vAd4aT<aboX2#0Q<1DAw3K^$D
zJTQefW7XDP@<=?33;gIMbp}7gqNVrQoGT$_UL-((_xA|m9>jUxsA<&Vc9_QD_%zI5
XPQn4t@JPa8eZk(WKQo%ap+x6zxyZ$g