英文:
Assume in lean 4
问题
在Lean 4中，与Lean 3中的assume相似的结构化假设方式似乎已被移除。要将Lean 3中使用assume的证明转换为Lean 4，通常的方法是使用不同的策略和构造来重写证明。以下是如何将您提供的Lean 3证明转换为Lean 4的一般方法：
theorem WetTheorem :
forall Rain Hydrant Wet : Prop,
(Rain ∨ Hydrant) →
(Rain → Wet) →
(Hydrant → Wet) →
Wet :=
begin
intros Rain Hydrant Wet, -- Introduce the universal quantifiers
intros RainingOrHydrantRunning RainMakesWet HydrantMakesWet, -- Introduce the assumptions
cases RainingOrHydrantRunning with raining running,
-- Case 1: RainingOrHydrantRunning is true because of Rain
{ exact RainMakesWet raining }, -- Use "exact" to prove the goal
-- Case 2: RainingOrHydrantRunning is true because of Hydrant
{ exact HydrantMakesWet running }, -- Use "exact" to prove the goal
end
在Lean 4中，您可以使用intros来引入全称量词和假设，而使用cases来分情况讨论。注意，在每种情况下，使用exact来证明目标，就像在Lean 3中使用show一样。
请注意，Lean 4具有不同的语法和构造，因此需要适应这些变化来迁移Lean 3的证明。您可以根据实际的证明结构和需要进行调整。
英文:
A lot of proofs in Lean 3 were structured via the assume syntax e.g.
theorem WetTheorem :
forall Rain Hydrant Wet: Prop,
(Rain ∨ Hydrant) → -- raining or hydrant on;
(Rain → Wet) → -- if raining then wet;
(Hydrant → Wet) → -- if hydrant on then wet;
Wet -- then wet
:=
begin
-- setup
assume Rain Hydrant Wet,
assume RainingOrHydrantRunning: (Rain ∨ Hydrant),
assume RainMakesWet: (Rain → Wet),
assume HydrantMakesWet: (Hydrant → Wet),
-- the core of the proof
cases RainingOrHydrantRunning with raining running,
show Wet, from RainMakesWet raining,
show Wet, from HydrantMakesWet running,
end
I was unable find a similar reference section for tactics in lean 4 like in 3, and it seems assume has been dropped. What would be the general method of converting a lean 3 proof with assume into a lean 4 without it?
答案1
得分: 3
在Lean 4中，策略模式中的assume可以被带有类型说明的intro替代，因此你的整个代码可以如下编写：
theorem WetTheorem :
forall Rain Hydrant Wet: Prop,
(Rain ∨ Hydrant) → -- 下雨或者开着水龙头；
(Rain → Wet) → -- 如果下雨就湿；
(Hydrant → Wet) → -- 如果开着水龙头就湿；
Wet -- 那么湿
:=
by
-- 设置
intro Rain Hydrant Wet
intro (RainingOrHydrantRunning : (Rain ∨ Hydrant))
intro (RainMakesWet: (Rain → Wet))
intro (HydrantMakesWet: (Hydrant → Wet))
-- 证明的核心部分
cases RainingOrHydrantRunning
case inl raining =>
exact RainMakesWet raining
case inr running =>
exact HydrantMakesWet running
请注意，这里我将箭头=>替换为了=>以匹配常见的Lean 4语法。
英文:
assume in tactic mode can be replaced by intro with a type ascription in lean 4, so your entire code can be written as follows
theorem WetTheorem :
forall Rain Hydrant Wet: Prop,
(Rain ∨ Hydrant) → -- raining or hydrant on;
(Rain → Wet) → -- if raining then wet;
(Hydrant → Wet) → -- if hydrant on then wet;
Wet -- then wet
:=
by
-- setup
intro Rain Hydrant Wet
intro (RainingOrHydrantRunning : (Rain ∨ Hydrant))
intro (RainMakesWet: (Rain → Wet))
intro (HydrantMakesWet: (Hydrant → Wet))
-- the core of the proof
cases RainingOrHydrantRunning
case inl raining =>
exact RainMakesWet raining
case inr running =>
exact HydrantMakesWet running
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论