首页 > 其他分享 >AlphaProof IMO 2024 P1 in LEAN 之 cases 策略(Tactic)

AlphaProof IMO 2024 P1 in LEAN 之 cases 策略(Tactic)

时间:2024-11-28 09:03:38浏览次数:7  
标签:case P1 目的 LEAN IMO inl intro ind AlphaProof

         书接上文,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.inlcase this.ind.intro.inr。这个是由主目的 case this.ind.intro 派生而来的。也就是,当 case this.ind.intro.inlcase 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

相关文章

  • AlphaProof IMO 2024 P1 in LEAN 之 induction 策略(Tactic)
        在AlphaProof使用intro策略后,此时的目的(Goal)为:    这时,AlphaProof使用induction策略,对 n:ℕ进行,归纳证明:    induction策略,在假设中,增加了,在归纳证明中使用的,前值假设,即:    改写后的目的(Goal)的高亮部分,a:∀m<n,......
  • CS61B srping 2018 disc02 sol https://sp18.datastructur.es/
    第19行的变量level是静态方法change方法内部的本地变量,他对main方法里的level或者是实例变量level没什么影响。publicclassPokemon{//一个名为Pokemon的类publicStringname;//实例变量namepublicintlevel;//实例变量levelpublicPokemon(String......
  • CS61B srping 2018 disc02 https://sp18.datastructur.es/
    passbywhat?a.下列程序每一行怎么运行?b.画出box-and-pointer指示图c.在第19行,level被赋值为50,level是什么?是Pokemon的实例变量?(instancevariable)还是change方法的本地变量?(localvariable?)还是main方法里的变量?还是其他什么东西?1publicclassPokemon{2public......
  • P1217 [USACO1.5] 回文质数 Prime Palindromes
    标题:P1217[USACO1.5]回文质数PrimePalindromes链接:https://www.luogu.com.cn/problem/P1217思路:1.暴力枚举,超时2.回文和质数共同判断,超时3.数字通过strings=to_string(n);转化为字符串,超时+:字符串转为数字intx=stoi(n);4.找规律,有偶数位的回文数(除了11)必然不是质数......
  • P10974 换根 dp 解题报告
    题目传送门题目大意:给定一颗无根树,有一个节点是源点,度数为\(1\)的点是汇点,树上的边有最大流量。除源点和汇点外,其它点不储存水,即流入该点的水量之和等于从该点流出的水量之和。整个水系的流量定义为原点单位时间内能发出的水量。现在需要求出:在流量不超过最大流量的前提下,选......
  • 【Unity 插件】MiniMonsters - Turn Based Monster Battles快速构建回合制怪物对战游
    MiniMonsters-TurnBasedMonsterBattles是一款专为Unity开发者设计的插件,旨在帮助开发者快速构建回合制怪物对战游戏。该插件提供了一整套完整的系统,包括怪物战斗逻辑、技能系统、回合制战斗管理等功能,使得开发者能够专注于游戏内容的创作,而不需要从零开始编写复杂的战......
  • 【Unity 插件】Lean Touch 快速创建基于触摸的交互功能,适合用于移动端游戏和应用开发
    LeanTouch是一款轻量级且功能强大的Unity插件,专门设计用于实现移动设备上的触摸输入控制,同时也支持鼠标输入。它能够帮助开发者快速创建基于触摸的交互功能,例如平移、缩放、旋转等操作,非常适合用于移动端游戏和应用开发。以下是其详细介绍:功能特点1.多点触控支持支持......
  • [luoguSP10707] Count on a tree II
    题意原题链接给定一棵树,节点\(i\)上有颜色\(c_i\),多次询问,每次查询两点之间的路径中的不同颜色数。sol这是一道类似普通莫队[luoguSP3267]D-query的题目,但是是在树上询问的,因此考虑将树转化为序列计算。将树转化为序列包括DFS序,欧拉序和树链剖分三种,树链剖分复杂度更......
  • GaussDB SQL基础语法示例-BOOLEAN表达式
    一、前言SQL是用于访问和处理数据库的标准计算机语言。GaussDB支持的SQL标准(默认支持SQL2、SQL3和SQL4的主要特性)。本系列将以《云数据库GaussDB—SQL参考》为主线进行介绍。二、GaussDBSQL中的BOOLEAN表达式介绍1、概念在GaussDB数据库中,BOOLEAN表达式是一种很常见的表达......
  • P1321 单词覆盖还原
    带点小思维首先,这题的意思就是boy,girl,。这三个单词会相应覆盖,但每个单词至少有一个单词不会被覆盖,那我们观察这三个单词发现,其里面每个字符都没有重复的,也就是说,假设我看到了一个o,那很明显就是boy的,假如看到一个l,那就是girl的,由于我们不知道每个字符被覆盖前是啥字符,那我们可以......