LEAN4入门教程1,自然数游戏Tutorial World章节

视频链接,制作不易记得投币哦:LEAN4入门教程,自然数游戏Tutorial World章节_哔哩哔哩_bilibili

import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L07add_succ

World "Tutorial"
Level 8
Title "2+2=4"

LemmaTab "012"

namespace MyNat

TacticDoc nth_rewrite "
## Summary

If `h : X = Y` and there are several `X`s in the goal, then
`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.

## Example

If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
will change the goal to `succ 1 + succ 1 = 4`.
"

NewHiddenTactic nth_rewrite

Introduction
" Good luck!

  One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.
  If you only want to change one of them, say the 3rd one, then use
  `nth_rewrite 3 [h]`.
"

/-- $2+2=4$. -/
Statement : (2 : ℕ) + 2 = 4 := by
  Hint (hidden := true) "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
  nth_rewrite 2 [two_eq_succ_one]
  Hint (hidden := true) "Now you can `rw [add_succ]`"
  rw [add_succ]
  rw [one_eq_succ_zero]
  rw [add_succ]
  rw [add_zero]
  rw [four_eq_succ_three]
  rw [three_eq_succ_two]
  rfl

Conclusion
"
Here is an example proof of 2+2=4 showing off various techniques.

```lean
nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ, add_zero] -- two rewrites at once
rw [← three_eq_succ_two] -- change `succ 2` to `3`
rw [← four_eq_succ_three]
rfl
```

Optional extra: you can run this proof yourself. Switch the game into \"Editor mode\" by clicking
on the `</>` button in the top right. You can now see your proof
written as several lines of code. Move your cursor between lines to see
the goal state at any point. Now cut and paste your code elsewhere if you
want to save it, and paste the above proof in instead. Move your cursor
around to investigate. When you've finished, click the `>_` button in the top right to
move back into command line mode.

You have finished tutorial world!
Click \"Leave World\" to go back to the
overworld, and select Addition World, where you will learn
about the `induction` tactic.
"

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/640471.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

[java基础揉碎]位运算符

java中有7个位运算&#xff08;&、|、^、~、>>、<<和>>>&#xff09; 第一组 分别是按位与&、按位或|、按位异或^&#xff0c;按位取反~&#xff0c;它们的运算规则是&#xff1a; 按位与& : 两位全为1&#xff0c;结果为1&#xff0c;否则…

熄灭LED

这段代码是用于STM32F10x系列微控制器的程序&#xff0c;主要目的是初始化GPIOA的Pin 0并使其输出高电平。下面是对这段代码的逐行解释&#xff1a; #include "stm32f10x.h"&#xff1a;这一行包含了STM32F10x系列微控制器的设备头文件。这个头文件包含了该系列微控…

蓝桥杯官网填空题(奇怪的分式)

题目描述 本题为填空题&#xff0c;只需要算出结果后&#xff0c;在代码中使用输出语句将所填结果输出即可。 上小学的时候&#xff0c;小明经常自己发明新算法。一次&#xff0c;老师出的题目是&#xff1a;1/4乘以8/5 小明居然把分子拼接在一起&#xff0c;分母拼接在一起&…

基于SpringBoot的高校学科竞赛平台管理系统

基于SpringBoot的高校学科竞赛平台管理系统的设计与实现~ 开发语言&#xff1a;Java数据库&#xff1a;MySQL技术&#xff1a;SpringBootMyBatis工具&#xff1a;IDEA/Ecilpse、Navicat、Maven 系统展示 前台界面 管理员界面 教师界面 学生界面 摘要 本文详细介绍了一款基于…

Google Colab运行Pytorch项目

Google Colab运行Pytorch项目 连接google drive切换到某一文件夹显示当前目录文件安装依赖执行py文件numpy相关numpy.random.randn() 参考文章&#xff1a;文章1 文章2 连接google drive from google.colab import drive import os drive.mount(/content/drive)切换到某一文件…

革新区块链:代理合约与智能合约升级的未来

作者 张群&#xff08;赛联区块链教育首席讲师&#xff0c;工信部赛迪特聘资深专家&#xff0c;CSDN认证业界专家&#xff0c;微软认证专家&#xff0c;多家企业区块链产品顾问&#xff09;关注张群&#xff0c;为您提供一站式区块链技术和方案咨询。 代理合约&#xff08;Prox…

WEB前端3D变换效果以及如何应用js代码

WEB前端DAY8 变换效果3d <!DOCTYPE html> <html><head><meta charset"utf-8"><title></title><style>body{/* 视距&#xff1a;设置距离xy轴构成的平面有多少像素距离 */perspective: 500px;}div{/* 设置变化效果为3d *…

开源项目_大模型应用_Chat2DB

1 基本信息 项目地址&#xff1a;https://github.com/chat2db/Chat2DBStar&#xff1a;10.7K 2 功能 Chat2DB 是一个智能且多功能的 SQL 客户端和报表工具&#xff0c;适用于各种数据库。 对于那些平时会用到数据库&#xff0c;但又不是数据库专家的程序员来说&#xff0c;…

9月大湾区塑料橡胶工业博览会,佛山潭洲国际会展中心

PLAS SHOW 2024大湾区塑料橡胶工业博览会 时间&#xff1a;2024年9月5日-7日 地点&#xff1a;佛山潭洲国际会展中心 中国大型塑料橡胶展&#xff0c;全国塑料橡胶产品的优选平台 共同塑造未来&#xff0c;双循环协作发展 大湾区塑料机械展|大湾区橡胶机械展|大湾区注塑机…

盘点几种有线扩展Wifi覆盖范围方式的优缺点

前言 前几天小白到一个朋友的家里&#xff0c;发现她家的主路由是放在玄关的。 这个方式就导致了她家三个卧室的Wifi信号都很弱。 她叫我过去帮忙弄一下网络的问题&#xff0c;这个对于有一点电脑知识的小伙伴来说&#xff0c;基本上不是什么难事&#xff0c;因为每个房间基本…

AVL树底层实现

目录 AVL树简介 AVL树节点定义​编辑 AVL树特性 AVL树的建立 AVL树的插入 AVL树的旋转 验证AVL树 AVL树的实现&#xff08;代码部分&#xff09; AVL树简介 AVL树是对二叉搜索树的改进&#xff0c;二叉搜索树虽可以缩短查找的效率&#xff0c;但如果数据有序或接近有序…

PDsehell16连接pgsql出现“Could not initialize JavaVM“时的解决步骤

问题原因:PowerDesigned16是32位的&#xff0c;只能使用32位的JDK来运行JDBC驱动 解决方案&#xff1a; 一、弄一个32为jdk的免安装包 二、 接下来就是配置系统环境变量了&#xff08;注意是系统不是用户环境变量&#xff09; JAVA_HOME配置刚刚32位的存放地址&#xff0c; …

(二十四)Kubernetes系列之Helm3

Helm为kubernetes的包管理工具&#xff0c;就像Linux下的包管理器&#xff08;yum/apt等&#xff09;&#xff0c;可以很方便的将之前打包好的yaml文件部署到kubernetes上。 1.安装访问地址&#xff1a;https://github.com/helm/helm/releases 点击查看最新的版本&#xff0c…

文件操作与IO(3)

文件内容的读写--数据流 这里我们将要讲到文件操作中的重要概念--流. 之前也在C语言讲解中提到了文件流的概念---读写文件内容 分为这几步:(1)打开文件;(2)读/写文件;(3)关闭文件. 数据流主要分为字节流和字符流. 字节流:以字节为单位进行读写(代表:InputStream,OutputStrea…

【Java网络编程01】网络原理初识

【Java网络编程01】网络原理初识 1. 网络通信基础概念 网络通信&#xff1a;网络互连的目的就是网络通信&#xff0c;即网络数据传输&#xff0c;再直白点而言就是不同主机的不同进程之间基于网络进行数据的传输交互。 那么&#xff0c;在组建的网络上有各种各样的主机&#…

Python量化交易- mplfinance库 -画K线图

mplfinance库 1. mplfinance 模块说明2. mplfinance安装3. mplfinance 模块 plot 基本用法参数typestylemake_addplot设置图表颜色 make_marketcolors添加图表样式 make_mpf_style 4. mplfinance 的基本K线图实现自定义风格和颜色图表尺寸调整、相关信息的显示添加完整移动平均…

Vue 实例创建流程

✨ 专栏介绍 在当今Web开发领域中&#xff0c;构建交互性强、可复用且易于维护的用户界面是至关重要的。而Vue.js作为一款现代化且流行的JavaScript框架&#xff0c;正是为了满足这些需求而诞生。它采用了MVVM架构模式&#xff0c;并通过数据驱动和组件化的方式&#xff0c;使…

CentOs7 安装Mysql(5.7和8.0版本)密码修改跳过 超详细教程

CSDN 成就一亿技术人&#xff01; 今天出一期Centos下安装Mysql&#xff08;详细教程&#xff09;包括数据库密码跳过修改 CSDN 成就一亿技术人&#xff01; 目录 1.获取安装包 2.安装程序 安装下载的rpm包 查看安装包 修改5.7版本&#xff08;重要&#xff09; 安装M…

设置代码模板创建sql映射文件、Mybatis主配置文件

目录 1、Sql映射&#xff08;Sql Mapper&#xff09;文件的介绍 2、Mybatis的主配置文件的介绍 3、通过代码模板创建Sql映射文件 4、通过代码模板创建Mybatis主配置文件 1、Sql映射&#xff08;Sql Mapper&#xff09;文件的介绍 <?xml version"1.0" encod…

太太二字的由来?

“太太”这个称谓的由来可以追溯到周朝时期的“周室三母”。这三位贤妃分别是太姜、太任和太姒。她们以母仪天下的德范&#xff0c;养育和辅佐了开创太平盛世的数位君王&#xff0c;成为了夫君的良佐、胎教的典范。因此&#xff0c;后世尊称别人的妻子为“太太”&#xff0c;以…