From 495203bf962f9d37f85eca09665f63d934186896 Mon Sep 17 00:00:00 2001
From: Isaac <ihershenson@hmc.edu>
Date: Mon, 18 Apr 2022 16:08:57 -0700
Subject: [PATCH] qed on failed subproof

---
 __pycache__/logicObjects.cpython-39.pyc | Bin 8719 -> 9121 bytes
 __pycache__/proof.cpython-39.pyc        | Bin 20463 -> 21039 bytes
 contradiction_proof.py                  |   3 ++-
 logicObjects.py                         |  11 +++++++++++
 proof.py                                |  15 ++++++++++++++-
 5 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/__pycache__/logicObjects.cpython-39.pyc b/__pycache__/logicObjects.cpython-39.pyc
index 228e8e8c28c7cce11a4a5cea5adb71ce783752fb..7285b63b78d5c987cbac85559cad38de8906afaa 100644
GIT binary patch
delta 1538
zcmZ`(OKclu5Z-^+k9BNs?AVUoG_E(QRBAQYq)nO<(!}IZXlg=fpbAkf*NL}r()f{C
zhliCYh^h#Q1Bekw2(?lrxNzZdKyX2-go=<5QsIDPIE9DA2_eCy2*S)dwsU~BW_ETS
z-#;^+`Cpy7^@x`9dOIX~YQJR`U(r9*(k>j09LG)9F8=Q8!L*`<%H5mNs@N2(;;K9+
zft|b|ff;}A_E{25nZrd*J6o)*tr%t^n>E(6*(Jg1y+@(9jcAg{oFJALTY^BPDJc`#
zk~c+FY|7WfutZvsm-)TkL6VeLuFD4+T3c8mFKLzh!qS`+x6i`1m!R&+{ra!}?C$Pv
zaANw-ORwv31^P(_KePLZkwT@{f;VTH8^ua>rCc(rQ157e0ym+-+$;r&rHM=rF-h1&
zhwxZb^R?@Afl+~Mb~f(BgtJFPu;Ph^kCA_h$mA1Mq1x!Dz%eX4qj-mkdI~4qFN=Bn
z$_?TYj(cW9gXH)mM>rZ0ifV&F@*kIB2!Hfk6qj+tJ0nhFt}|fg#Fp@eHys!vDa&Ep
zSvp7|@3Qk@Jgv<*PLT>8<N$oZVH3;vu9kN<lx%53UB&*+M+3v8yh7B3vcWLMBIohD
z&W!gV4j3g?mn+M7*A*0Hyy(lhTl#%yRjm8A91RN(h<Fxjej_x(5SEr_#R7xV_=o?f
z*v4qr6JfTOh?*_4tBR_^2wv~naagf~SPUe^5Z(yH>?v}55pM?$i<Fh)P_Q7TTa~_v
z9|yN|7$B#6A|AIjW`O4orkG7LYnT5vu7=)n^F)G=*(7S+I>9BokBghQ*!|ZDE0iYz
z9%E+3cd}%a!mYP}>#DJ46pd2Vgmd^>_>_1LzYHG{<9OE_2{Zm1MEmRWzyziLj=P=J
znN|^>;xCbFNnWm+r(ZWWmI`{ckgMu2L#k#?b0q&~O`qWh2UZ;oGwMBk;x<n7{GGH8
zdYl2|x}10btZ6vOAlB&f)Yo03%SOp~t^#9suypXFGYnE!a%*ewza2Qo2p0DF7M6u-
ztr0irbG*`<-0Q>z`u>Dye<u{UU@gZ^?|P7dn#*dhK&ARTjJ4YGEpA8W{qyAV4MQ-t
zDu6aAmcpZlzG#ff1pav_79As7-M#mh%;t(lU0Exbbp;A0OyfZ8i1;4oV^1GkB0sP)
zUEm0!ChP*iejUoNov#3}F}uWU1mD-Asmm<#F$?aM(lZ8_1|I`CRxh&JwWpq52kVqp
zmo2=X(bIR|fWhAFo2Q-4G8uj%YG%XV@h(VXzVAeW?+f7V2i{w-HYCLo&lzxwftv(e
e641(e!}vp=9tdh~&8ewcPz`8@wH{6Nb^Hr4ghBBD

delta 1286
zcma)6T}V@L6z{*O-MM+Uxy?D(+I0hKD4H%mO3k^-FZ_(mudGeIG;50fx5^|Th$xCa
z=seYf74({5K@brXK?O$n;7fyEdI@^yrHJT5I_K}Ez6f17hjY*WcYf#Nf9}24czvH7
z&dSQ%gwOMjgF{C5yxgjTPT31rb<1GXIW2{F6hMikp^})C#tUKI;esB+S=ItehD)ps
z2D3Qpg2k+MTPcE?37xTm)*`-C;E|J+L0mq>x?w?XarhCyDe;QZlVwHK3&qA(OBq@R
zQBqm8ye!G$fw#t1Rt{!kE}Y9qV~3%_G~z9%@Cs5J@rK};smZt#Ap>i?P$K8UJBJ@4
z=E00A3f~0_W+xkg&*m`PHf3&D<|v%Vo=Js#&ECSIptq>DO5zYi8o@?tH(ao6XK|Rb
zblK^A7$qj5!fB>UT1n!SkYoLnA!18m*;;~wDz>@PYY}rA4%ob`7Mt&cSGEWXLMYG9
zu0UhXOy#tuNcqKlzBFz|BoC0PClw^M(I9TXpPXCzI)a!;1>mk-LEabkG6wM7{@WiQ
zH{Bv{Atl(1WQm?=4@8=Tq(;>-bvz#9P2h1<u{$u}C}1_v<<7Me|7Dc*jT(3z_Hkdo
zR^wjL%^XbSoo{SF^t7Q!iJcsdDDg-*uJA^5rMl}x`#-vS1VQI<{TkQ>bUBY<$@#ZL
z<ZUHRO+r(=gNvnE8xyTyLRWK49apC&_@1XXT@M?GD4`8UqZ`koX|=F6vcyUYQnAuB
zvM2D<Rg#=b2fjZ*Sw9yo?-0u!-#Tff8hu($>(QS+!6)Kpc(oYP8!)?j&E4pKP2t2V
zG2V@VR=DQ=wz55Sa8Yr)s_`tLPhL)YcuY-bqmfub%Of!!gqKPITZAu4pEHCwE~@N7
z>pe<}wkJtj1he_qZ2g2YkP>&_M^+`&dt8A*GAUiZesuhl%3~^}<44GSl-#<cd;cU4
zkyA`Zq$Ius%zCz!4y_)DQ-KqZ5j^;SlB$Z{ec8Mjet7)F^rzwUo8a_KbMf)e2gAi?
k)0jC8i&JZS1b5O7<6gz0llAguS(2@iMfS>hvSiBq2V>;~?EnA(

diff --git a/__pycache__/proof.cpython-39.pyc b/__pycache__/proof.cpython-39.pyc
index 0e857c7cc0903b81c6265c5711667f11ec3e73dc..c898826976047179757c88785b07a10596e0af05 100644
GIT binary patch
delta 565
zcmZuu%}T>S5S~fWQmrjg|EPFaZ}w2ZgDB!fDuPfGK|ENfk|wc@w25ZZONl6`2al4A
zUbF@8BEEvYhTsE;c=qCKTB`?Vnc1EBW@f*g{kX%2dra%8)F6<2y_YM`wX5_c79X!y
zF|}c;=TMq4aSL+V(;My-cMVx2_9RAooU}m7D`cv0EC;v><<Vm$klPTz0R~DII*4$T
z2tXm<mjXG8OIbLRs<;3W>|un-;c0Pfo6xq>0R&T~dzIG9AnVDx<9n{zG%Th&%x)ak
zZA15M*I^Z%TPCA}&Uv$OC}Ny)Or|r#b&PtGhquYeJYNwoUt)gEVs+cGxPX1#c5J5_
z1^?8Co#ezxfvSJgneX=cnO2`vYpzer?2@9k{}Lj8-Ah}Uzn!8WQ*$vdPb2ga!mJ20
z0P|#r=}6cRZKbrRSLq4ehm?{%U(hVYBl6rUgrA9#wUKB(7XKk9W>S~vpF|^wE119x
iPSI**H$B(gpZzC4mkXEGSG)<wwP{qtMNJDYw1aPj=%hCQ

delta 62
zcmZ3#gz^1+M!rN|UM>b8(0vn|#GW>huanVb;|v!@R>oikP2bHg86$m|G&Lrd2Hcw*
R5h%;(Gr26#fAaCb3;;jk6SDvS

diff --git a/contradiction_proof.py b/contradiction_proof.py
index a8e489e..dcac2a3 100644
--- a/contradiction_proof.py
+++ b/contradiction_proof.py
@@ -23,4 +23,5 @@
 p.switchSidesOfEqual(8)
 p.notElim(6,9)
 p.concludeSubproof(6)
-#p.impliesIntroduction([4,5],11)
\ No newline at end of file
+p.impliesIntroduction([4,5],11)
+p.qed(12)
diff --git a/logicObjects.py b/logicObjects.py
index 8ec70d7..4075cee 100644
--- a/logicObjects.py
+++ b/logicObjects.py
@@ -70,6 +70,17 @@ def elim(self, arg):
         if arg==self.assum:
             return self.conc
 
+    def __eq__(self, other):
+        return self.assum == other.assum and self.conc == other.conc
+
+    def __repr__(self):
+        assumptionstr = ""
+        for assumption in self.assum:
+            assumptionstr += str(assumption)
+            assumptionstr += ", "
+        assumptionstr = assumptionstr[:-2]
+        return  assumptionstr + " → " +  str(self.conc)
+
 class Not:
     def __init__(self, arg):
         self.arg = arg
diff --git a/proof.py b/proof.py
index 6041010..13e5698 100644
--- a/proof.py
+++ b/proof.py
@@ -615,4 +615,17 @@ def notElim(self, lineNum1, lineNum2):
             self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}']
             self.show()
         else:
-            print(f"The statement on line {lineNum1} isn't a Not")
\ No newline at end of file
+            print(f"The statement on line {lineNum1} isn't a Not")
+
+    def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it
+        '''
+        Introduce an implication based on assumptions and a conclusion
+        :param lineNumsAssums: the lines containing the assumptions
+        :param lineNumConc: the line to conclude
+        '''
+        assums = []
+        for line in lineNumsAssums:
+            assums.append(self.steps[line])
+        self.steps += [Implies(assums,self.steps[lineNumConc])]
+        self.justifications += [f"Introduced implies based on assumptions on lines {lineNumsAssums} to conclude line {lineNumConc}"]
+        self.show()
\ No newline at end of file