人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界:逆否策略的等效替代,提取假设 的已知,tauto另类理解,更 严格的归纳法假设。。。

本文主要是介绍人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界:逆否策略的等效替代,提取假设 的已知,tauto另类理解,更 严格的归纳法假设。。。,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

视频讲解:人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界:逆否策略的等效替代,提取假设 的已知,tauto另类理解,更 严格的归纳法假设。。。_哔哩哔哩_bilibili

import Game.Levels.AdvMultiplication.L08mul_eq_zero

World "AdvMultiplication"
Level 9
Title "mul_left_cancel"

TheoremTab "*"

namespace MyNat

/-- `mul_left_cancel a b c` is a proof that if `a ≠ 0` and `a * b = a * c` then `b = c`. -/
TheoremDoc MyNat.mul_left_cancel as "mul_left_cancel" in "*"

Introduction
"
In this level we prove that if `a * b = a * c` and `a ≠ 0` then `b = c`. It is tricky, for
several reasons. One of these is that
we need to introduce a new idea: we will need to understand the concept of
mathematical induction a little better.

Starting with `induction b with d hd` is too naive, because in the inductive step
the hypothesis is `a * d = a * c → d = c` but what we know is `a * succ d = a * c`,
so the induction hypothesis does not apply!

Assume `a ≠ 0` is fixed. The actual statement we want to prove by induction on `b` is
\"for all `c`, if `a * b = a * c` then `b = c`. This *can* be proved by induction,
because we now have the flexibility to change `c`.\"
"

Statement mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) (h : a * b = a * c) : b = c := by
  Hint "The way to start this proof is `induction b with d hd generalizing c`."
  induction b with d hd generalizing c
  · Hint (hidden := true) "Use `mul_eq_zero` and remember that `tauto` will solve a goal
  if there are hypotheses `a = 0` and `a ≠ 0`."
    rw [mul_zero] at h
    symm at h
    apply mul_eq_zero at h
    cases h with h1 h2
    · tauto
    · rw [h2]
      rfl
  · Hint "The inductive hypothesis `hd` is \"For all natural numbers `c`, `a * d = a * c → d = c`\".
    You can `apply` it `at` any hypothesis of the form `a * d = a * ?`. "
    Hint (hidden := true) "Split into cases `c = 0` and `c = succ e` with `cases c with e`."
    cases c with e
    · rw [mul_succ, mul_zero] at h
      apply add_left_eq_zero at h
      tauto
    · rw [mul_succ, mul_succ] at h
      apply add_right_cancel at h
      apply hd at h
      rw [h]
      rfl

这篇关于人工智能数学验证工具LEAN4【入门介绍9】高级乘法世界:逆否策略的等效替代,提取假设 的已知,tauto另类理解,更 严格的归纳法假设。。。的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/792430

相关文章

详解C#如何提取PDF文档中的图片

《详解C#如何提取PDF文档中的图片》提取图片可以将这些图像资源进行单独保存,方便后续在不同的项目中使用,下面我们就来看看如何使用C#通过代码从PDF文档中提取图片吧... 当 PDF 文件中包含有价值的图片,如艺术画作、设计素材、报告图表等,提取图片可以将这些图像资源进行单独保存,方便后续在不同的项目中使

Spring Boot + MyBatis Plus 高效开发实战从入门到进阶优化(推荐)

《SpringBoot+MyBatisPlus高效开发实战从入门到进阶优化(推荐)》本文将详细介绍SpringBoot+MyBatisPlus的完整开发流程,并深入剖析分页查询、批量操作、动... 目录Spring Boot + MyBATis Plus 高效开发实战:从入门到进阶优化1. MyBatis

Python基于wxPython和FFmpeg开发一个视频标签工具

《Python基于wxPython和FFmpeg开发一个视频标签工具》在当今数字媒体时代,视频内容的管理和标记变得越来越重要,无论是研究人员需要对实验视频进行时间点标记,还是个人用户希望对家庭视频进行... 目录引言1. 应用概述2. 技术栈分析2.1 核心库和模块2.2 wxpython作为GUI选择的优

opencv图像处理之指纹验证的实现

《opencv图像处理之指纹验证的实现》本文主要介绍了opencv图像处理之指纹验证的实现,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的朋友们下面随着小编来一起学... 目录一、简介二、具体案例实现1. 图像显示函数2. 指纹验证函数3. 主函数4、运行结果三、总结一、

使用Java实现通用树形结构构建工具类

《使用Java实现通用树形结构构建工具类》这篇文章主要为大家详细介绍了如何使用Java实现通用树形结构构建工具类,文中的示例代码讲解详细,感兴趣的小伙伴可以跟随小编一起学习一下... 目录完整代码一、设计思想与核心功能二、核心实现原理1. 数据结构准备阶段2. 循环依赖检测算法3. 树形结构构建4. 搜索子

利用Python开发Markdown表格结构转换为Excel工具

《利用Python开发Markdown表格结构转换为Excel工具》在数据管理和文档编写过程中,我们经常使用Markdown来记录表格数据,但它没有Excel使用方便,所以本文将使用Python编写一... 目录1.完整代码2. 项目概述3. 代码解析3.1 依赖库3.2 GUI 设计3.3 解析 Mark

SpringBoot如何通过Map实现策略模式

《SpringBoot如何通过Map实现策略模式》策略模式是一种行为设计模式,它允许在运行时选择算法的行为,在Spring框架中,我们可以利用@Resource注解和Map集合来优雅地实现策略模式,这... 目录前言底层机制解析Spring的集合类型自动装配@Resource注解的行为实现原理使用直接使用M

利用Go语言开发文件操作工具轻松处理所有文件

《利用Go语言开发文件操作工具轻松处理所有文件》在后端开发中,文件操作是一个非常常见但又容易出错的场景,本文小编要向大家介绍一个强大的Go语言文件操作工具库,它能帮你轻松处理各种文件操作场景... 目录为什么需要这个工具?核心功能详解1. 文件/目录存javascript在性检查2. 批量创建目录3. 文件

Python实现常用文本内容提取

《Python实现常用文本内容提取》在日常工作和学习中,我们经常需要从PDF、Word文档中提取文本,本文将介绍如何使用Python编写一个文本内容提取工具,有需要的小伙伴可以参考下... 目录一、引言二、文本内容提取的原理三、文本内容提取的设计四、文本内容提取的实现五、完整代码示例一、引言在日常工作和学

C++字符串提取和分割的多种方法

《C++字符串提取和分割的多种方法》在C++编程中,字符串处理是一个常见的任务,尤其是在需要从字符串中提取特定数据时,本文将详细探讨如何使用C++标准库中的工具来提取和分割字符串,并分析不同方法的适用... 目录1. 字符串提取的基本方法1.1 使用 std::istringstream 和 >> 操作符示