Let $*$ be a commutative and associative binary operation on a set $S.$ Assume that for every $x$ and $y$ in $S,$ there exists $z$ in $S$ such that $x*z=y.$ (This $z$ may depend on $x$ and $y.$) Show that if $p,q,r$ are in $S$ and $p*r=q*r,$ then $p=q.$
</ol>
We have now proved the exists a unique Universal Identity, namely $e$ for the set $S$.Now for every pair $(x,e)$ we can find a $y$ (depending on $x$ and $e$) such that $x*y=e$ .Using this observation we can eliminate $c$ from the equation $a*c=b*c$.
In [1]:
import $cp.bin.`provingground-core-jvm-2312478e00.fat.jar`
Out[1]:
In [2]:
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[2]:
In [3]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
import FineDeducer.unif
import monix.execution.Scheduler.Implicits.global
import scala.concurrent._
import duration._
Out[3]:
In [4]:
val M = "M" ::Type
val a = "a" :: M
val b = "b" :: M
val c = "c" :: M
val d = "d" :: M
val x = "x" :: M
val y = "y" :: M
val z = "z" :: M
val e = "e" :: M
val p = "p" :: M
val q = "q" :: M
val r = "r" :: M
val s = "s" :: M
val t = "t" :: M
val e1 = "e1" :: M
val e2 = "e2" :: M
Out[4]:
In the section below we define the following operators:-
In [5]:
val eqM = "eqM" :: M ->: M ->: Type
val op = "op" :: M ->: M ->: M
val op_2 = "op_2" :: M ->: M ->: M ->: M
val inv = "inv" :: M ->: M ->: M
Out[5]:
One of the best festures of this notebook is that after this step every step of the proof can be executed independently.
In [24]:
val one_ :FiniteDistribution[Term] = unif(a,b)(x,e,op,eqM,inv)(
a ~>: b ~>: (eqM(op(a)(inv(a)(b)))(b))
)*0.5++(FiniteDistribution.unif(op:Term)*0.5)++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(inv:Term)*0.5)
val one_1 = one_.filter((t) => !Set(a, b).contains(t)).normalized()
val ts_0 = TermState(one_1,one_1.map(_.typ))
Out[24]:
In [25]:
val lp_0 = LocalProver(ts_0,cutoff = 5*math.pow(10,-6)).noIsles
Out[25]:
In [26]:
val lem_0 = lp_0.lemmas.runSyncUnsafe()
Out[26]:
In [6]:
val zero: FiniteDistribution[Term] = unif(a,b,c,d)(op(x)(e),x,inv(x)(y),op,eqM)(
eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c)),
eqM(op(x)(e))(x)
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term)*0.5) ++(FiniteDistribution.unif(op: Term)*0.25)
val zero1 = zero.filter((t) => !Set(a, b, c, d).contains(t)).normalized()
val ts_ = TermState(zero1,zero1.map(_.typ))
val ts_1 = TermState(zero1,zero1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(e))(x) ->: eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))))
Out[6]:
In [12]:
val lp_ = LocalProver(ts_,cutoff=5*math.pow(10,-6)).noIsles
val lp_1 = LocalProver(ts_1,cutoff=5*math.pow(10,-6)).noIsles
Out[12]:
We will see that when we do not put goals in the TermState then the prover generates the desired lemma with low wieghtage or does not generate the desired and some time even does not genrate any lemma(this is the case is when the cutoff is set very low is order to capture the desired lemma but before the program could finish the generation of lemmas the program timeouts).This is common when many terms and axioms are given to the prover.Including goals becomes a crucial part in these cases as they drastically change the wieghtage of terms and hence change the generation process too.Thus helping the prover in generation of desired lemma.
In [13]:
val lem_ = lp_.lemmas.runSyncUnsafe()
Out[13]:
In [14]:
val lem_1 = lp_1.lemmas.runSyncUnsafe()
Out[14]:
In [6]:
val negative1_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y),eqM,op)(
eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative1_1 = negative1_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_3 = TermState(negative1_1,negative1_1.map(_.typ))
val ts_4 = TermState(negative1_1,negative1_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y))))))
Out[6]:
In [ ]:
val lp_2 = LocalProver(ts_3,cutoff=5*math.pow(10,-6)).noIsles
val lp_3 = LocalProver(ts_4,cutoff=5*math.pow(10,-6)).noIsles
val lp_4 = LocalProver(ts_3,cutoff=math.pow(10,-6)).noIsles
In [13]:
val lem_2 = lp_2.lemmas.runSyncUnsafe()
Out[13]:
There were a large number of terms in the term state so the expexted lemmas had too low wieghtage to get generated.Thus no lemma was generated.So now we try to generate the desired lemma by,
In [12]:
val lem_3 = lp_3.lemmas.runSyncUnsafe()
Out[12]:
In [16]:
val lem_4 = lp_4.lemmas.runSyncUnsafe()
In [7]:
val negative2_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y),eqM,op)(
eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
eqM(op(a)(b))(op(b)(a))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.3)++(FiniteDistribution.unif(op:Term,eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)))*0.9)
val negative2_1 = negative2_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_5 = TermState(negative2_1,negative2_1.map(_.typ))
val ts_6 = TermState(negative2_1,negative2_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))))
Out[7]:
In [18]:
val tg = TermGenParams(unAppW=0.3)
val tg1 = TermGenParams(appW=0.3)
val tg2 = TermGenParams(unAppW=0.2,appW = 0.2)
val tg3 = TermGenParams(appW = 0.2)
val tg4 = TermGenParams(unAppW = 0.2)
val lp_5 = LocalProver(ts_6,cutoff=5*math.pow(10,-6)).noIsles
val lp_6 = LocalProver(ts_6,tg,cutoff=5*math.pow(10,-5)).noIsles
val lp_7 = LocalProver(ts_6,tg1,cutoff=5*math.pow(10,-6)).noIsles
val lp_8 = LocalProver(ts_6,tg2,cutoff=5*math.pow(10,-6)).noIsles
val lp_9 = LocalProver(ts_6,tg,cutoff=8*math.pow(10,-6)).noIsles
val lp_10 = LocalProver(ts_6,tg1,cutoff=8*math.pow(10,-6)).noIsles
val lp_11 = LocalProver(ts_6,tg2,cutoff=8*math.pow(10,-6)).noIsles
val lp_12 = LocalProver(ts_6,tg3,cutoff=math.pow(10,-5)).noIsles
val lp_13 = LocalProver(ts_6,tg3,cutoff=8*math.pow(10,-5)).noIsles
val lp_14 = LocalProver(ts_6,tg4,cutoff=5*math.pow(10,-5)).noIsles
val lp_15 = LocalProver(ts_6,tg4,cutoff=3*math.pow(10,-5)).noIsles
Out[18]:
In [19]:
val lem_5 = lp_5.lemmas.runSyncUnsafe()
Out[19]:
In [19]:
val lem_6 = lp_6.lemmas.runSyncUnsafe()
In [24]:
val lem_7 = lp_7.lemmas.runSyncUnsafe()
In [ ]:
val lem_8 = lp_8.lemmas.runSyncUnsafe()
In [27]:
val lem_9 = lp_9.lemmas.runSyncUnsafe()
In [26]:
val lem_10 = lp_10.lemmas.runSyncUnsafe()
In [ ]:
val lem_11 = lp_11.lemmas.runSyncUnsafe()
In [29]:
val lem_12 = lp_12.lemmas.runSyncUnsafe()
In [17]:
val lem_13 = lp_13.lemmas.runSyncUnsafe()
Out[17]:
In [11]:
val lem_14 = lp_14.lemmas.runSyncUnsafe()
Out[11]:
In [15]:
val lem_15=lp_15.lemmas.runSyncUnsafe()
Out[15]:
In the above cases we could clearly see that either the prover is only using the commutivity axiom to produce lemmas or it is not producing any.In the above case various combination of Term generation parameters as well as cutoff levels were tested in hope of obtaining the desired lemma.In the coming sections of the proof we will see that a similar situation ocuurs where prover has to use a axiom to generate some terms which will be used with some other axiom to generate the desired lemma.In some cases the prover would succesfully generate the lemmas because the number of terms in the Term State were fairly less.
In [20]:
val negative3_ : FiniteDistribution[Term] = unif(a,b,c)(x,inv(x)(y),e,eqM,op)(
eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
eqM(op(e)(inv(x)(y)))(op(inv(x)(y))(e))
)*0.5++(FiniteDistribution.unif(eqM:Term,op:Term)*0.5)
val negative3_1 = negative3_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_7 = TermState(negative3_1,negative3_1.map(_.typ))
val ts_8 = TermState(negative3_1,negative3_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e)))))
Out[20]:
In [30]:
val tg5 = TermGenParams(unAppW=0.3)
val tg6 = TermGenParams(appW=0.2)
val lp_16 = LocalProver(ts_8,cutoff=5*math.pow(10,-6)).noIsles
val lp_17 = LocalProver(ts_7,cutoff=5*math.pow(10,-6)).noIsles
val lp_18 = LocalProver(ts_7,tg5,cutoff=5*math.pow(10,-6)).noIsles
val lp_19 = LocalProver(ts_7,tg6,cutoff=9*math.pow(10,-5)).noIsles
Out[30]:
In [22]:
val lem_16 = lp_16.lemmas.runSyncUnsafe()
Out[22]:
In [24]:
val lem_17 = lp_17.lemmas.runSyncUnsafe()
Out[24]:
In [25]:
val lem_18 = lp_18.lemmas.runSyncUnsafe()
In [31]:
val lem_19 = lp_19.lemmas.runSyncUnsafe()
Out[31]:
In [6]:
val negative4_ : FiniteDistribution[Term] = unif(a,b,c)(x,inv(x)(y),e)(
eqM(op(op(a)(b))(c))(op(a)(op(b)(c)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative4_1 = negative4_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_9 = TermState(negative4_1,negative4_1.map(_.typ))
val ts_10 = TermState(negative4_1,negative4_1.map(_.typ),goals = FiniteDistribution.unif(a ~>: b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))))
val ts_11 = TermState(negative4_1,negative4_1.map(_.typ))
val ts_12 = TermState(negative4_1,negative4_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e)))))
Out[6]:
In [16]:
val tg7= TermGenParams(unAppW=0.3)
val lp_20=LocalProver(ts_10,tg7,cutoff=3*math.pow(10,-6),limit=10000.minutes).noIsles
val lp_21=LocalProver(ts_10,tg7,cutoff=5*math.pow(10,-6),limit=1000.minutes).noIsles
val lp_22=LocalProver(ts_12,cutoff=5*math.pow(10,-6),limit=1000.minutes).noIsles
val lp_23=LocalProver(ts_12,tg7,cutoff=5*math.pow(10,-6)).noIsles
val lp_24 = LocalProver(ts_10,cutoff=5*math.pow(10,-6)).noIsles
val lp_25 = LocalProver(ts_9,cutoff =1*math.pow(10,-6)).noIsles
Out[16]:
In [ ]:
val lem_20 = lp_20.lemmas.runSyncUnsafe()
In [9]:
val lem_22=lp_22.lemmas.runSyncUnsafe()
Out[9]:
In [14]:
val lem_21 = lp_21.lemmas.runSyncUnsafe()
In [21]:
val lem_25 = lp_25.lemmas.runSyncUnsafe()
In [33]:
val negative5_ : FiniteDistribution[Term] = unif(a,b,c)()(
eqM(op(op(x)(inv(x)(y)))(e))(op(x)(op(inv(x)(y))(e))),
eqM(a)(b) ->: eqM(b)(a)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.1)++(FiniteDistribution.unif(op:Term)*1)
val negative5_1 = negative5_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val negative6_ : FiniteDistribution[Term] = unif(a,b,c)()(
eqM(op(op(a)(b))(c))(op(a)(op(b)(c))),
eqM(a)(b) ->: eqM(b)(a)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.7)++(FiniteDistribution.unif(op:Term)*0.9)
val negative6_1 = negative6_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_13 = TermState(negative5_1,negative5_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e))))
val ts_14 = TermState(negative5_1,negative5_1.map(_.typ),goals = FiniteDistribution.unif(a ~>: b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))))
val ts_15 = TermState(negative5_1,negative5_1.map(_.typ))
Out[33]:
In [42]:
val tg8= TermGenParams(piW=0.3)
val tg9 = TermGenParams(unAppW=0.3,appW=0.2)
val lp_26 = LocalProver(ts_14,tg10,cutoff = 3*math.pow(10,-6))
val lp_27 = LocalProver(ts_13,cutoff = 5*math.pow(10,-6)).noIsles
val lp_28 = LocalProver(ts_15,tg9,cutoff = 2*math.pow(10,-6)).noIsles
Out[42]:
In [29]:
val lem_26 = lp_26.lemmas.runSyncUnsafe()
Out[29]:
In [12]:
val goals = a ~>: b ~>: c ~>: eqM(op(a)(op(b)(c)))(op(op(a)(b))(c))
Out[12]:
In [32]:
val lem_27 = lp_27.lemmas.runSyncUnsafe()
Out[32]:
In [43]:
val lem_28 = lp_28.lemmas.runSyncUnsafe()
Out[43]:
In [60]:
val negative7_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
eqM(op(x)(inv(x)(y)))(y),
eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.3)++(FiniteDistribution.unif(op:Term)*0.4)
val negative7_1 = negative7_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_17 = TermState(negative7_1,negative7_1.map(_.typ))
val ts_16 = TermState(negative7_1,negative7_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))))
Out[60]:
In [61]:
val lp_28 = LocalProver(ts_16,cutoff=2*math.pow(10,-6)).noIsles
Out[61]:
In [62]:
val lem_28 = lp_28.lemmas.runSyncUnsafe()
Out[62]:
Basically we will prove $$\{(x*e)*inv(x)(y) = x*(e*inv(x)(y)) \ \ \land$$ $$x*(e*inv(x)(y)) = x*(inv(x)(y)*e) \ \ \land$$ $$x*(inv(x)(y)*e) = (x*inv(x)(y))*e \ \ \land$$ $$(x*inv(x)(y))*e = y*e \} \implies $$ $$(x*e)*inv(x)(y) = y*e$$
In [26]:
val negative8_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(e)(inv(x)(y)))),
eqM(op(x)(op(e)(inv(x)(y))))(op(x)(op(inv(x)(y))(e))),
eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)),
eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative8_1 = negative8_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_18 = TermState(negative8_1,negative8_1.map(_.typ))
val ts_19 = TermState(negative8_1,negative8_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))))
val tg10 = TermGenParams(unAppW =0.2)
Out[26]:
In [27]:
val lp_29 = LocalProver(ts_19,tg10,cutoff=2*math.pow(10,-6)).noIsles
Out[27]:
In [18]:
val lem_29 = lp_29.lemmas.runSyncUnsafe()
Out[18]:
In [29]:
val lem_30 = lp_29.lemmas.runSyncUnsafe()
In [7]:
val negative9_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(op(op(x)(e))(inv(x)(y)))(op(x)(op(inv(x)(y))(e))),
eqM(op(x)(op(inv(x)(y))(e)))(op(op(x)(inv(x)(y)))(e)),
eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative9_1 = negative9_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_20 = TermState(negative9_1,negative9_1.map(_.typ))
val ts_21 = TermState(negative9_1,negative9_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e))))
val negative10_ : FiniteDistribution[Term] = unif(a,b,c)(x,e,inv(x)(y))(
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(op(op(x)(e))(inv(x)(y)))(op(op(x)(inv(x)(y)))(e)),
eqM(op(op(x)(inv(x)(y)))(e))(op(y)(e))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative10_1 = negative10_.filter((t) => !Set(a, b,c).contains(t)).normalized()
val ts_22 = TermState(negative10_1,negative10_1.map(_.typ))
val ts_23 = TermState(negative10_1,negative10_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e))))
Out[7]:
In [8]:
val lp_30 = LocalProver(ts_21,cutoff=2*math.pow(10,-6)).noIsles
val lp_31 = LocalProver(ts_23,cutoff=2*math.pow(10,-6)).noIsles
Out[8]:
In [9]:
val lem_30 = lp_30.lemmas.runSyncUnsafe()
val lem_31 = lp_31.lemmas.runSyncUnsafe()
Out[9]:
Basically we wil prove $$[ \{ (x*e)*inv(x)(y) = (y*e) \} \land \{x*inv(x)(y) = y\} \land \{(x*e)*inv(x)(y)) = ((x*inv(x)(y))\} ] \implies (y*e=y)$$ $$\Updownarrow$$ $$\{(a=b) \land (c=d) \land (a=c)\} \implies (b=d)$$ where $$ a= (x*e)*inv(x)(y) \\ b= (y*e) \\ c= x*inv(x)(y) \\ d= y \\ $$
In [6]:
val negative11_ : FiniteDistribution[Term] = unif(a,b,c,d)(x,e,inv(x)(y),y)(
eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
eqM(op(x)(inv(x)(y)))(y),
eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.8)
val negative11_1 = negative11_.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_24 = TermState(negative11_1,negative11_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))
val negative12_ : FiniteDistribution[Term] = unif(a,b,c,d)(op(op(x)(e))(inv(x)(y)),op(y)(e),op(x)(inv(x)(y)),y,eqM,op)(
eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
eqM(op(x)(inv(x)(y)))(y),
eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative12_1 = negative12_.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_25 = TermState(negative12_1,negative12_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))
val negative13 : FiniteDistribution[Term] = unif(a,b,c,d)(eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),eqM(op(x)(inv(x)(y)))(y),eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y))))(
eqM(a)(b) ->: eqM(c)(d) ->: eqM(a)(c) ->: eqM(b)(d),
eqM(op(op(x)(e))(inv(x)(y)))(op(y)(e)),
eqM(op(x)(inv(x)(y)))(y),
eqM(op(op(x)(e))(inv(x)(y)))(op(x)(inv(x)(y)))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative13_1 = negative13.filter((t) => !Set(a, b,c,d).contains(t)).normalized()
val ts_26 = TermState(negative13_1,negative13_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(y)(e))(y)))
Out[6]:
In [7]:
val tg11 = TermGenParams(unAppW=0.25)
val lp_32 = LocalProver(ts_24,cutoff=9*math.pow(10,-6)).noIsles
val lp_33 = LocalProver(ts_25,tg11,cutoff=9*math.pow(10,-6)).noIsles
val lp_34 = LocalProver(ts_26,cutoff=5*math.pow(10,-6)).noIsles
Out[7]:
In [24]:
val lem_32 = lp_32.lemmas.runSyncUnsafe()
Out[24]:
In [9]:
val lem_33 = lp_33.lemmas.runSyncUnsafe()
In [8]:
val lem_34 = lp_34.lemmas.runSyncUnsafe()
Out[8]:
We have proved that all identity elements are universal identities.Now we have to prove that the cardinality of set of all the universal identity is 1.This proof goes similar to Monoid proof.The link to the Monoid proof notebook is https://github.com/siddhartha-gadgil/ProvingGround/blob/master/notes/2019-09-18-monoid.ipynb .
In [18]:
val negative14_ : FiniteDistribution[Term] = unif(a)(e1,e2)(
eqM(op(a)(e1))(a),
eqM(op(e2)(a))(a),
eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.4)
val negative14_1 = negative14_.filter((t) => !Set(a).contains(t)).normalized()
val ts_27 = TermState(negative14_1,negative14_1.map(_.typ),goals = FiniteDistribution.unif(eqM(e1)(e2)))
Out[18]:
In [19]:
val lp_35 = LocalProver(ts_27,cutoff = 5*math.pow(10,-6)).noIsles
Out[19]:
In [20]:
val lem_35 = lp_35.lemmas.runSyncUnsafe()
Out[20]:
In [35]:
val negative15_ : FiniteDistribution[Term] = unif(a,b,c)(e1,e2,op)(
eqM(op(e2)(e1))(e1),
eqM(op(e2)(e1))(e2),
eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.5)++(FiniteDistribution.unif(op:Term)*0.4)
val negative15_1 = negative15_.filter((t) => !Set(a,b,c).contains(t)).normalized()
val ts_28 = TermState(negative15_1,negative15_1.map(_.typ))
val ts_29 = TermState(negative15_1,negative15_1.map(_.typ),goals = FiniteDistribution.unif(eqM(e1)(e2)))
Out[35]:
In [39]:
val lp_36 = LocalProver(ts_28,cutoff = 5*math.pow(10,-6)).noIsles
val lp_37 = LocalProver(ts_29,cutoff = 5*math.pow(10,-6)).noIsles
Out[39]:
In [37]:
val lem_36 = lp_36.lemmas.runSyncUnsafe()
Out[37]:
In [38]:
val lem_37 = lp_37.lemmas.runSyncUnsafe()
Out[38]:
Now we have successfully completed the prove for Part1.
In [42]:
val negative16_ : FiniteDistribution[Term] = unif(a,b,c)(op(p)(r),op(q)(r),inv(r)(e),op,eqM)(
eqM(a)(b) ->: eqM(op(a)(c))(op(b)(c)),
eqM(op(p)(r))(op(q)(r))
) * 0.5++(FiniteDistribution.unif(eqM: Term)*0.5)++(FiniteDistribution.unif(op: Term)*0.25)
val negative16_1 = negative16_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_30 = TermState(negative16_1,negative16_1.map(_.typ))
Out[42]:
In [43]:
val lp_38 = LocalProver(ts_30,cutoff = 5*math.pow(10,-6)).noIsles
Out[43]:
In [44]:
val lem_38 = lp_38.lemmas.runSyncUnsafe()
Out[44]:
In the above equation we haven't applied the bracketting on the first term, this is done to encompass the associative property of the operation *.
In [53]:
val negative17_ : FiniteDistribution[Term] = unif(a,b,c)(op(op(p)(r))(inv(r)(e)),op(p)(op(r)(inv(r)(e))),op_2(p)(r)(inv(r)(e)),eqM)(
eqM(op(op(a)(b))(c))(op(a)(op(b)(c))) ->: eqM(op(a)(op(b)(c)))(op_2(a)(b)(c)),
eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e))))
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative17_1 = negative17_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_31 = TermState(negative17_1,negative17_1.map(_.typ))
val ts_32= TermState(negative17_1,negative17_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e)))))
Out[53]:
In [54]:
val lp_39 = LocalProver(ts_32,cutoff = 5*math.pow(10,-6)).noIsles
Out[54]:
In [55]:
val lem_39= lp_39.lemmas.runSyncUnsafe()
Out[55]:
In [56]:
val negative18_ : FiniteDistribution[Term] = unif(a,b,c)(op(op(p)(r))(inv(r)(e)),op(p)(op(r)(inv(r)(e))),op_2(p)(r)(inv(r)(e)),eqM)(
eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(q)(inv(r)(e))),
eqM(op(op(p)(r))(inv(r)(e)))(op(p)(op(r)(inv(r)(e)))),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative18_1 = negative18_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_33 = TermState(negative18_1,negative18_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(q)(inv(r)(e)))))
Out[56]:
In [57]:
val lp_40 = LocalProver(ts_33,cutoff = 5*math.pow(10,-6)).noIsles
Out[57]:
In [58]:
val lem_40 = lp_40.lemmas.runSyncUnsafe()
Out[58]:
In [6]:
val negative19_ : FiniteDistribution[Term] = unif(a,b,c)(p,r,e,inv,op,eqM)(
eqM(a)(b) ->: eqM(op(c)(a))(op(c)(b)),
eqM(op(a)(inv(a)(e)))(e)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)
val negative19_1 = negative19_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_31 = TermState(negative19_1,negative19_1.map(_.typ))
val ts_32= TermState(negative19_1,negative19_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e))))
Out[6]:
In [15]:
val lp_41 = LocalProver(ts_32,cutoff = 5*math.pow(10,-6)).noIsles
Out[15]:
In [16]:
val lem_41 = lp_41.lemmas.runSyncUnsafe()
Out[16]:
In [9]:
val negative20_ :FiniteDistribution[Term] = unif(a,b,c)(eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)),eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))))(
eqM(op(p)(op(r)(inv(r)(e))))(op(p)(e)),
eqM(op(p)(op(r)(inv(r)(e))))(op_2(p)(r)(inv(r)(e))),
eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(op:Term)*0.6)
val negative20_1 = negative20_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_33 = TermState(negative20_1,negative20_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(inv(r)(e)))(op(p)(e))))
Out[9]:
In [10]:
val lp_42 = LocalProver(ts_33,cutoff = 5*math.pow(10,-6)).noIsles
Out[10]:
In [11]:
val lem_42 = lp_42.lemmas.runSyncUnsafe()
Out[11]:
In [15]:
val negative21_ :FiniteDistribution[Term] = unif(a,b,c)(p,eqM,op)(
eqM(op(a)(e))(a),
eqM(op_2(a)(r)(inv(r)(e))(op(a)(e)),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative21_1 = negative21_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_34 = TermState(negative21_1,negative21_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(s))(p)))
Out[15]:
In [16]:
val tg12 = TermGenParams(unAppW = 0.3)
val lp_43 = LocalProver(ts_34,tg12,cutoff = 5*math.pow(10,-6)).noIsles
Out[16]:
In [17]:
val lem_43 = lp_43.lemmas.runSyncUnsafe()
Out[17]:
In the following section below we are going to represent inv(r)(e) with variable s.Then we will see that after replacing the inv(r)(e) with s we were able to prove the theorem i.e we are defining $s$ such that $s \in M$ and $s=inv(r)(e)$.And by doing this we are able to get the desired lemma.
In the program below we have skipped a the following steps:- $$s=inv(r)(e) $$ $$\implies r*s = r*inv(r)(e)$$ $$\implies p*(r*s) = p*(r*inv(r)(e)) $$ $$\implies p*r*s = p*r*inv(r)(e) $$ But since we have done it several times previously we wont repeat it again.
In [6]:
val negative22_ :FiniteDistribution[Term] = unif(a,b,c)(p,eqM,op)(
eqM(op(a)(e))(a),
eqM(op_2(a)(r)(s))(op(a)(e)),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative22_1 = negative22_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_35 = TermState(negative22_1,negative22_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(p)(r)(s))(p)))
Out[6]:
In [19]:
val lp_44 = LocalProver(ts_35,tg12,cutoff = 5*math.pow(10,-6)).noIsles
Out[19]:
In [20]:
val lem_44 = lp_44.lemmas.runSyncUnsafe()
Out[20]:
In [24]:
val negative23_ :FiniteDistribution[Term] = unif(a,b,c)(eqM(op_2(p)(r)(s))(p),eqM(op_2(p)(r)(inv(r)(e)))(p))(
eqM(op_2(p)(r)(inv(r)(e)))(op_2(p)(r)(s)),
eqM(op_2(p)(r)(s))(p),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative23_1 = negative23_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_36 = TermState(negative23_1,negative23_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op_2(a)(r)(inv(r)(e)))(p)))
Out[24]:
In [25]:
val lp_45 = LocalProver(ts_36,cutoff = 5*math.pow(10,-6)).noIsles
Out[25]:
In [26]:
val lem_45 = lp_45.lemmas.runSyncUnsafe()
Out[26]:
Basically we will prove $$[ \{(p*r)*inv(r)(e) = p*r*inv(r)(e)\} \land$$ $$\{p*r*inv(r)(e) = p \}] \implies$$ $$(p*r)*inv(r)(e) = p$$
In [38]:
val negative24_ :FiniteDistribution[Term] = unif(a,b,c)(op_2(p)(r)(inv(r)(e)),op(op(p)(r))(inv(r)(e)))(
eqM(op(op(p)(r))(inv(r)(e)))(op_2(p)(r)(inv(r)(e))),
eqM(op_2(p)(r)(inv(r)(e)))(p),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(p:Term)*0.6)
val negative24_1 = negative24_.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts_37 = TermState(negative24_1,negative24_1.map(_.typ),goals = FiniteDistribution.unif(eqM(op(op(p)(r))(s))(p)))
Out[38]:
In [39]:
val tg13 = TermGenParams(unAppW = 0.2)
val lp_46 = LocalProver(ts_37,tg13,cutoff = 2*math.pow(10,-6)).noIsles
Out[39]:
In [40]:
val lem_46 = lp_46.lemmas.runSyncUnsafe()
Out[40]:
If we follow the same set of steps for q then we will get the same set of resuts as we got for p. For this step let, $$t=inv(r)(e)$$
I have skipped the following steps:- $$t = inv(r)(e)$$ $$\implies r*t = r*inv(r)(e) $$ $$\implies p*(r*t) = p*(r*inv(r)(e))$$ $$\implies p*r*t = p*r*inv(r)(e) $$ Also, $$t = inv(r)(e)$$ $$\implies r*t = r*inv(r)(e) $$ $$\implies q*(r*t) = q*(r*inv(r)(e))$$ $$\implies q*r*t = q*r*inv(r)(e) $$ and, $$p*r*inv(r)(e) = q*r*inv(r)(e)$$ $$\implies p*r*t=q*r*t $$
In [10]:
val negative26_ :FiniteDistribution[Term] = unif(a,b,c,d)(eqM(op_2(q)(r)(t))(q),eqM(op_2(p)(r)(t))(p),eqM(op_2(p)(r)(t))(op_2(q)(r)(t)))(
eqM(op_2(q)(r)(t))(q),
eqM(op_2(p)(r)(t))(p),
eqM(op_2(p)(r)(t))(op_2(q)(r)(t)),
eqM(a)(b) ->: eqM(a)(c) ->: eqM(b)(d) ->: eqM(c)(d)
)*0.5++(FiniteDistribution.unif(eqM:Term)*0.9)++(FiniteDistribution.unif(op_2:Term)*0.6)
val negative26_1 = negative26_.filter((t) => !Set(a, b, c,d).contains(t)).normalized()
val ts_38 = TermState(negative26_1,negative26_1.map(_.typ),goals = FiniteDistribution.unif(eqM(p)(q)))
Out[10]:
In [11]:
val lp_47 = LocalProver(ts_38,cutoff = 1.5*math.pow(10,-6)).noIsles
Out[11]:
In [12]:
val lem_47 = lp_47.lemmas.runSyncUnsafe()
Out[12]: