书接上文,AlphaProof 通过 suffices 和 have 策略,产生其需要的假设后,使用了一系列的 norm_num 与 rw 策略,进行简化,如下:
使得目的被改写为:
此后,再通过 连续使用两次 zify 策略,如下
其中,at *,意思是,作用于当前目的的所有假设与目标。
[*],意思是,使用所有的假设进行 zify 简化。
使得,主目的(main goal)被改写为:
其中,两个 this: True,可以忽略。
此时,AlphaProof 使用了 cases 策略,如下:
通过,其策略参数的值,进行分类讨论,
lt_or_ge c (A * (l-.floor ↑x)+⌊x⌋ + 1)
也就是,下图中 c :
即,在 case this.ind.intor.inl 中的,h : c < ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1;
与 在 case this.ind.intro.inr 中的,h : c ≥ ↑A * (l - ⌊x⌋) + ⌊x⌋ + 1;
之后,AlphaProof 使用 点(·)策略,专注于 目的 case this.ind.intro.inl 的证明。这个,在后文进行讲述,敬请期待。
那么,此时,还有那些未被证明的目的呢?
包括,刚刚 cases 产生的两个目的,case this.ind.intro.inl,case this.ind.intro.inr。这个是由主目的 case this.ind.intro 派生而来的。也就是,当 case this.ind.intro.inl,case this.ind.intro.inr 被证明后,case this.ind.intro 也随之被证明。
另外两个是,上面的 suffices 策略产生的。都叫 this 的目的,如下:
因此,目前还有 4 个目的需要解决。
标签:case,P1,目的,LEAN,IMO,inl,intro,ind,AlphaProof From: https://blog.csdn.net/sinat_36821938/article/details/143962603