phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

merge

Browse Source
This commit is contained in:
Marcus Zibrowius
2023-03-15 14:08:56 +01:00
parent fc493635d1 07ec94b7c2
commit 588c362aa3
130 changed files with 2232 additions and 1665 deletions
Download Patch File Download Diff File Expand all files Collapse all files
NOTES.md
+1 -1
View File
@@ -38,7 +38,7 @@ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
source ~/.bashrc
nvm install node npm
sudo npm install -g http-server
npm install -g http-server
```
# Clone NNG interface
UPDATE_LEAN.sh
Executable → Regular
View File
client/src/components/Inventory.tsx
+5 -12
View File
@@ -6,17 +6,14 @@ import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-s
import Markdown from './Markdown';
import { useLoadDocQuery, ComputedInventoryItem } from '../state/api';
function Inventory({ tactics, lemmas, definitions } :
export function Inventory({ tactics, lemmas, definitions, setInventoryDoc } :
{lemmas: ComputedInventoryItem[],
tactics: ComputedInventoryItem[],
definitions: ComputedInventoryItem[]}) {
const [docName, setDocName] = useState(null)
const [docType, setDocType] = useState(null)
definitions: ComputedInventoryItem[],
setInventoryDoc: (inventoryDoc: {name: string, type: string}) => void}) {
function openDoc(name, type) {
setDocName(name)
setDocType(type)
setInventoryDoc({name, type})
}
return (
@@ -31,8 +28,6 @@ function Inventory({ tactics, lemmas, definitions } :
<h2>Lemmas</h2>
<InventoryList items={lemmas} docType="Lemma" openDoc={openDoc} />
{docName && <Documentation name={docName} type={docType} />}
</div>
)
}
@@ -81,7 +76,7 @@ function InventoryItem({name, locked, disabled, showDoc}) {
return <div className={`item ${className}`} onClick={handleClick}>{icon} {name}</div>
}
function Documentation({name, type}) {
export function Documentation({name, type}) {
const doc = useLoadDocQuery({type: type, name: name})
@@ -90,5 +85,3 @@ function Documentation({name, type}) {
<Markdown>{doc.data?.text}</Markdown>
</>
}
export default Inventory;
client/src/components/Level.tsx
+72 -77
View File
@@ -9,7 +9,7 @@ import { Link, useParams } from 'react-router-dom';
import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material';
import MuiDrawer from '@mui/material/Drawer';
import Grid from '@mui/material/Unstable_Grid2';
import Inventory from './Inventory';
import {Inventory, Documentation} from './Inventory';
import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter';
import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
import 'lean4web/client/src/editor/vscode.css';
@@ -61,6 +61,17 @@ function Level() {
const levelId = parseInt(params.levelId)
const worldId = params.worldId
useLoadWorldFiles(worldId)
if (levelId == 0) {
return <Introduction worldId={worldId} />
} else {
return <PlayableLevel worldId={worldId} levelId={levelId} />
}
}
function PlayableLevel({worldId, levelId}) {
const codeviewRef = useRef<HTMLDivElement>(null)
const introductionPanelRef = useRef<HTMLDivElement>(null)
@@ -115,8 +126,6 @@ function Level() {
const gameInfo = useGetGameInfoQuery()
useLoadWorldFiles(worldId)
const level = useLoadLevelQuery({world: worldId, level: levelId})
const dispatch = useAppDispatch()
@@ -132,79 +141,14 @@ function Level() {
const {editor, infoProvider, editorConnection} =
useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
// TODO: This is a hack for having an introduction (i.e. level 0)
// for each world.
if (levelId == 0) {
return <>
<div className="app-bar">
<div>
<Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button>
<span className="app-bar-title">
{gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
</span>
</div>
<div>
<span className="app-bar-title">
{`Einführung`}
</span>
<Button disabled={levelId <= 1} inverted={true}
to={`/world/${worldId}/level/0`}
><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
<Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
to={`/world/${worldId}/level/1`}
>Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
</div>
</div>
<div className="exercise-panel">
<div ref={introductionPanelRef} className="introduction-panel">
<Alert severity="info" sx={{ mt: 1 }}>
<Markdown>
{gameInfo.data?.worlds.nodes[worldId].introduction}
</Markdown>
</Alert>
<div ref={codeviewRef} className={`codeview ${commandLineMode ? 'hidden' : ''}`}></div>
</div>
<div className="conclusion">
{levelId >= gameInfo.data?.worldSize[worldId] ?
<Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/world/${worldId}/level/1`}>
Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
</Button>}
</div>
</div>
</>
}
const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null)
const levelTitle = <>{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}</>
return <>
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<div style={level.isLoading ? {display: "none"} : null} className="app-bar">
<div>
<Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button>
<span className="app-bar-title">
{gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
</span>
</div>
<div>
<span className="app-bar-title">
{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`}
</span>
<Button disabled={levelId <= 0} inverted={true}
to={`/world/${worldId}/level/${levelId - 1}`}
><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
<Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
to={`/world/${worldId}/level/${levelId + 1}`}
>Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
</div>
</div>
<Split minSize={0} snapOffset={200} sizes={[0, 50, 25, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<div className="side-panel">
{/*
<div ref={introductionPanelRef} className="introduction-panel">
<Markdown>{level?.data?.introduction}</Markdown>
</div>
*/}
</div>
<LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
<Split minSize={0} snapOffset={200} sizes={[50, 25, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<div className="exercise-panel">
<div ref={introductionPanelRef} className="introduction-panel">
<Alert severity="info" sx={{ mt: 1 }}>
@@ -241,11 +185,13 @@ function Level() {
</div>}
</div>
<div className="doc-panel">
{!level.isLoading && <Inventory tactics={level?.data?.tactics} lemmas={level?.data?.lemmas} definitions={level?.data?.definitions} />}
<div className="inventory-panel">
{!level.isLoading &&
<Inventory tactics={level?.data?.tactics} lemmas={level?.data?.lemmas}
definitions={level?.data?.definitions} setInventoryDoc={setInventoryDoc} />}
</div>
<div className="side-panel">
<p>Display Tactic documentation here?</p>
<div className="doc-panel">
{inventoryDoc && <Documentation name={inventoryDoc.name} type={inventoryDoc.type} />}
</div>
</Split>
</>
@@ -253,6 +199,55 @@ function Level() {
export default Level
function Introduction({worldId}) {
const gameInfo = useGetGameInfoQuery()
return <>
<div style={gameInfo.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<LevelAppBar isLoading={gameInfo.isLoading} levelTitle="Einführung" worldId={worldId} levelId={0} />
<div style={gameInfo.isLoading ? {display: "none"} : null} className="exercise-panel">
<div className="introduction-panel">
<Alert severity="info" sx={{ mt: 1 }}>
<Markdown>
{gameInfo.data?.worlds.nodes[worldId].introduction}
</Markdown>
</Alert>
</div>
<div className="conclusion">
{0 == gameInfo.data?.worldSize[worldId] ?
<Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button> :
<Button to={`/world/${worldId}/level/1`}>
Start&nbsp;<FontAwesomeIcon icon={faArrowRight} />
</Button>}
</div>
</div>
</>
}
function LevelAppBar({isLoading, levelId, worldId, levelTitle}) {
const gameInfo = useGetGameInfoQuery()
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
<div>
<Button to={`/`}><FontAwesomeIcon icon={faHome} /></Button>
<span className="app-bar-title">
{gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`}
</span>
</div>
<div>
<span className="app-bar-title">
{levelTitle}
</span>
<Button disabled={levelId <= 0} inverted={true}
to={`/world/${worldId}/level/${levelId - 1}`}
><FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous</Button>
<Button disabled={levelId >= gameInfo.data?.worldSize[worldId]} inverted={true}
to={`/world/${worldId}/level/${levelId + 1}`}
>Next&nbsp;<FontAwesomeIcon icon={faArrowRight} /></Button>
</div>
</div>
}
function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, onDidChangeContent) {
client/src/components/inventory.css
+12 -6
View File
@@ -8,12 +8,6 @@
margin-bottom: .2em;
}
.inventory h2.doc {
margin-top: 1.5em;
font-weight: 900;
}
.inventory-list {
display: flex;
gap: .5em;
@@ -58,3 +52,15 @@
color: black;
border-bottom: 0.3em solid var(--clr-primary);
}
.doc-panel {
padding: 0 1em;
}
.doc-panel h2 {
font-size: 1.5em;
margin-top: 1em;
margin-bottom: .2em;
font-weight: 900;
}
client/src/components/level.css
+1 -7
View File
@@ -24,17 +24,11 @@
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
}
.side-panel, .exercise-panel, .doc-panel {
.inventory-panel, .exercise-panel, .doc-panel {
height: 100%;
overflow: auto;
}
.side-panel {
display: flex;
flex-flow: column;
background-color: #e9f2fb;
}
.introduction-panel, .infoview, .exercise, .conclusion {
padding-top: 1em;
padding-left: 1em;
server/build.sh
Executable → Regular
View File
server/leanserver/GameServer/AbstractCtx.lean
+26
View File
@@ -0,0 +1,26 @@
import Lean
section AbstractCtx
open Lean
open Meta
structure AbstractCtxResult :=
(abstractMVarsResult : AbstractMVarsResult)
/-- Abstract LCtx and MCtx to transport an expression into different contexts -/
def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
let goalDecl ← goal.getDecl
let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId)
let goal ← mkLambdaFVars (usedLetOnly := false) fvars goalDecl.type
let goal ← abstractMVars goal
return {
abstractMVarsResult := goal
}
def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
let (mvars, binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
lambdaLetTelescope (← instantiateMVars expr) k
-- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
-- If the goal is a function, this will not work.
end AbstractCtx
server/leanserver/GameServer/Commands.lean
+128 -39
View File
@@ -1,6 +1,7 @@
import Lean
import GameServer.EnvExtensions
import GameServer.StrInterpolation
open Lean Meta
@@ -61,36 +62,117 @@ partial def reprintCore : Syntax → Option Format
def reprint (stx : Syntax) : Format :=
reprintCore stx |>.getD ""
-- macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
syntax hintArg := " (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")"
/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
see hints. The tactic does not affect the goal state. -/
elab "Hint" args:hintArg* msg:Lean.Parser.interpolatedStrNoIndent : tactic => do
let mut strict := false
let mut hidden := false
for arg in args do
match arg with
| `(hintArg| (strict := true)) => strict := true
| `(hintArg| (strict := false)) => strict := false
| `(hintArg| (hidden := true)) => hidden := true
| `(hintArg| (hidden := false)) => hidden := false
| _ => throwUnsupportedSyntax
let goal ← Tactic.getMainGoal
goal.withContext do
-- We construct an expression that can produce the hint text. The difficulty is that we
-- want the text to possibly contain quotation of the local variables which might have been
-- named differently by the player.
let varsName := `vars
let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
let mut text ← expandInterpolatedStr ⟨msg.raw⟩ (← `(MessageData)) (← `(toMessageData))
let goalDecl ← goal.getDecl
let decls := goalDecl.lctx.decls.toArray.filterMap id
for i in [:decls.size] do
text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize text none
let textmvar ← mkFreshExprMVar none
guard $ ← isDefEq textmvar text -- Store the text in a mvar.
-- The information about the hint is logged as a message using `logInfo` to transfer it to the
-- `Statement` command defined below:
logInfo $
.tagged `Hint $
.nest (if strict then 1 else 0) $
.nest (if hidden then 1 else 0) $
.compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
proof state. We use it to define Hints for alternative proof methods or dead ends. -/
elab "Branch" t:tacticSeq : tactic => do
let b ← saveState
Tactic.evalTactic t
let msgs ← Core.getMessageLog
b.restore
Core.setMessageLog msgs
/-- Define the statement of the current level.
Arguments:
- ident: (Optional) The name of the statemtent.
- descr: The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
- descr: (Optional) The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
-/
elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : command => do
elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
let lvlIdx ← getCurLevelIdx
let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
("level" ++ toString lvlIdx : String)
-- save the messages before evaluation of the proof
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
-- let thmStatement' ← match statementName with
-- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
-- | some name => `(lemma $name $sig $val)
elabCommand thmStatement
let msgs := (← get).messages
let mut hints := #[]
let mut nonHintMsgs := #[]
for msg in msgs.msgs do
-- Look for messages produced by the `Hint` tactic. They are used to pass information about the
-- intermediate goal state
if let MessageData.withNamingContext _ $ MessageData.withContext ctx $
.tagged `Hint $
.nest strict $
.nest hidden $
.compose (.ofGoal text) (.ofGoal goal) := msg.data then
let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
return {
goal := ← abstractCtx goal
text := ← instantiateMVars (mkMVar text)
strict := strict == 1
hidden := hidden == 1
}
hints := hints.push hint
else
nonHintMsgs := nonHintMsgs.push msg
-- restore saved messages and non-hint messages
modify fun st => { st with
messages := initMsgs ++ ⟨nonHintMsgs.toPArray'⟩
}
let scope ← getScope
let env ← getEnv
elabCommand thmStatement
modifyCurLevel fun level => pure {level with
module := env.header.mainModule
goal := sig,
scope := scope,
descrText := descr.getString,
descrText := match descr with
| none => ""
| some s => s.getString
descrFormat := match statementName with
| none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
| some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10 -- "lemma " ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
hints := hints
} -- Format.pretty <| format thmStatement.raw }
/-- Define the conclusion of the current game or current level if some
@@ -138,38 +220,40 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
| [] => return s
def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
(goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
let (g, decls) ← elabBinders binders fun xs => do
let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
synthesizeSyntheticMVarsNoPostponing false
return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
let varsName := `vars
let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
let mut msg ← `(m! $msg)
for i in [:decls.size] do
msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
-- def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
-- (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
-- liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
-- let (g, decls) ← elabBinders binders fun xs => do
-- let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
-- synthesizeSyntheticMVarsNoPostponing false
-- return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
-- let varsName := `vars
-- let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
-- let mut msg ← `(m! $msg)
-- for i in [:decls.size] do
-- msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
-- return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
-- if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
modifyCurLevel fun level => pure {level with hints := level.hints.push {
goal := g,
intros := decls.size,
hidden := hidden,
text := msg }}
-- modifyCurLevel fun level => pure {level with hints := level.hints.push {
-- goal := g,
-- intros := decls.size,
-- hidden := hidden,
-- text := msg }}
/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
local elab "Hint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command =>
elabHint false binders goal msg
-- elabHint false binders goal msg
pure ()
/--
Declare a hint. This version doesn't prevent the unused linter variable from running.
A hidden hint is only displayed if explicitly requested by the user.
-/
local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
elabHint true binders goal msg
-- elabHint true binders goal msg
pure ()
/-- Declare a hint in reaction to a given tactic state in the current level. -/
macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
@@ -201,19 +285,19 @@ elab "TacticDoc" name:ident content:str : command =>
content := content.getString })
/-- Declare tactics that are introduced by this level. -/
elab "NewTactics" args:ident* : command => do
elab "NewTactic" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
/-- Declare tactics that are temporarily disabled in this level -/
elab "DisabledTactics" args:ident* : command => do
elab "DisabledTactic" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Tactic name
-- for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
/-- Temporarily disable all tactics except the ones declared here -/
elab "OnlyTactics" args:ident* : command => do
elab "OnlyTactic" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
@@ -231,19 +315,19 @@ elab "DefinitionDoc" name:ident content:str : command =>
content := content.getString })
/-- Declare definitions that are introduced by this level. -/
elab "NewDefinitions" args:ident* : command => do
elab "NewDefinition" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
/-- Declare definitions that are temporarily disabled in this level -/
elab "DisabledDefinitions" args:ident* : command => do
elab "DisabledDefinition" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Definition name
-- for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
/-- Temporarily disable all definitions except the ones declared here -/
elab "OnlyDefinitions" args:ident* : command => do
elab "OnlyDefinition" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
@@ -264,19 +348,19 @@ elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : c
content := content.getString })
/-- Declare lemmas that are introduced by this level. -/
elab "NewLemmas" args:ident* : command => do
elab "NewLemma" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
/-- Declare lemmas that are temporarily disabled in this level -/
elab "DisabledLemmas" args:ident* : command => do
elab "DisabledLemma" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Lemma name
-- for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
/-- Temporarily disable all lemmas except the ones declared here -/
elab "OnlyLemmas" args:ident* : command => do
elab "OnlyLemma" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
@@ -347,13 +431,18 @@ elab "MakeGame" : command => do
for item in (level.getInventory inventoryType).new do
let category := (← getInventoryDoc? item inventoryType).get!.category
items := items.insert item {name := item, category, locked := false, disabled := false}
let mut disabled : HashSet Name := {}
for item in (level.getInventory inventoryType).disabled do
let category := (← getInventoryDoc? item inventoryType).get!.category
items := items.insert item {name := item, category, locked := false, disabled := true}
items := items.insert item {name := item, category, locked := false, disabled := false}
-- (we set disabled to false at first because it applies only to the current level)
disabled := disabled.insert item
let itemsArray := items.toArray
|>.insertionSort (fun a b => a.1.toString < b.1.toString)
|>.map (·.2)
|>.map (fun item => {item with disabled := disabled.contains item.name})
modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
return level.setComputedInventory inventoryType itemsArray
server/leanserver/GameServer/EnvExtensions.lean
+8 -5
View File
@@ -1,5 +1,6 @@
import Lean
import GameServer.Graph
import GameServer.AbstractCtx
/-! # Environment extensions
@@ -16,15 +17,17 @@ open Lean
A hint to help the user with a specific goal state
-/
structure GoalHintEntry where
goal : Expr
/-- Number of variables to intro in the beginning of goal -/
intros : Nat
goal : AbstractCtxResult
/-- Text of the hint as an expression of type `Array Expr → MessageData` -/
text : Expr
/-- If true, then hint should be hidden by default -/
/-- If true, then hint should be hidden and only be shown on player's request -/
hidden : Bool := false
deriving Repr
/-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
strict : Bool := false
instance : Repr GoalHintEntry := {
reprPrec := fun a n => reprPrec a.text n
}
/-! ## Tactic/Definition/Lemma documentation -/
server/leanserver/GameServer/RpcHandlers.lean
+86 -29
View File
@@ -25,26 +25,83 @@ def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option G
| return none
return ← getLevel? levelId
/-- Check if each meta variable in `declMvars` has a matching fvar in `declFvars` -/
def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do
structure FVarBijection :=
(forward : HashMap FVarId FVarId)
(backward : HashMap FVarId FVarId)
instance : EmptyCollection FVarBijection := ⟨{},{}⟩
def FVarBijection.insert (bij : FVarBijection) (a b : FVarId) : FVarBijection :=
⟨bij.forward.insert a b, bij.backward.insert b a⟩
def FVarBijection.insert? (bij : FVarBijection) (a b : FVarId) : Option FVarBijection :=
let a' := bij.forward.find? a
let b' := bij.forward.find? b
if (a' == none || a' == some b) && (b' == none || b' == some a)
then some $ bij.insert a b
else none
/-- Checks if `pattern` and `e` are equal up to FVar identities. -/
partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : Option FVarBijection :=
match pattern, e with
| .bvar i1, .bvar i2 => if i1 == i2 then bij else none
| .fvar i1, .fvar i2 => bij.insert? i1 i2
| .mvar _, .mvar _ => bij
| .sort u1, .sort u2 => bij -- TODO?
| .const n1 ls1, .const n2 ls2 =>
if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
| .app f1 a1, .app f2 a2 =>
some bij
|> (Option.bind · (fun bij => matchExpr f1 f2 bij))
|> (Option.bind · (fun bij => matchExpr a1 a2 bij))
| .lam _ t1 b1 _, .lam _ t2 b2 _ =>
some bij
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
| .forallE _ t1 b1 _, .forallE _ t2 b2 _ =>
some bij
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
| .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ =>
some bij
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|> (Option.bind · (fun bij => matchExpr v1 v2 bij))
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
| .lit l1, .lit l2 =>
if l1 == l2 then bij else none
| .proj i1 n1 e1, .proj i2 n2 e2 =>
if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none
-- ignore mdata:
| .mdata _ pattern', _ =>
matchExpr pattern' e bij
| _, .mdata _ e' =>
matchExpr pattern e' bij
| _, _ => none
/-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
-- We iterate through the array backwards hoping that this will find us faster results
-- TODO: implement backtracking
let mut usedFvars := (List.replicate declFvars.size false).toArray
-- `usedFvars` keeps track of the fvars that were already used to match an mvar.
for i in [:declMvars.size] do
let declMvar := declMvars[declMvars.size - i - 1]!
let mut found := false
for j in [:declFvars.size] do
let declFvar := declFvars[declFvars.size - j - 1]!
let usedFvar := usedFvars[declFvars.size - j - 1]!
if ¬ usedFvar then
if ← isDefEq declMvar declFvar then
usedFvars := usedFvars.set! (declFvars.size - j - 1) true
found := true
break
else
let mut bij := initBij
for i in [:patterns.size] do
let pattern := patterns[patterns.size - i - 1]!
if bij.forward.contains pattern.fvarId! then
continue
for j in [:fvars.size] do
let fvar := fvars[fvars.size - j - 1]!
if bij.backward.contains fvar.fvarId! then
continue
if ¬ found then return false
if let some bij' := matchExpr
(← instantiateMVars $ ← inferType pattern)
(← instantiateMVars $ ← inferType fvar) bij then
-- usedFvars := usedFvars.set! (fvars.size - j - 1) true
bij := bij'.insert pattern.fvarId! fvar.fvarId!
break
if ! bij.forward.contains pattern.fvarId! then return false
if strict then
return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
return true
unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
@@ -62,19 +119,19 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName
| throwError "Level not found: {doc.meta.mkInputContext.fileName}"
let hints ← level.hints.filterMapM fun hint => do
let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros
-- TODO: Protect mvars in the type of `goal` to be instantiated?
if ← isDefEq hintGoal (← inferType $ mkMVar goal)
then
let lctx ← getLCtx -- Local context of the `goal`
if ← matchDecls declMvars lctx.getFVars
openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
then
let text := (← evalHintMessage hint.text) declMvars
let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
let text ← (MessageData.withContext ctx text).toString
return some { text := text, hidden := hint.hidden }
else return none
else return none
let lctx := (← goal.getDecl).lctx
if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
then
let text := (← evalHintMessage hint.text) hintFVars
let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
let text ← (MessageData.withContext ctx text).toString
return some { text := text, hidden := hint.hidden }
else return none
else
return none
return hints
open RequestM in
server/leanserver/GameServer/StrInterpolation.lean
+149
View File
@@ -0,0 +1,149 @@
/- Adapted from `Lean.Parser.StrInterpolation`
This version of interpolated strings deletes any initial spaces from
new lines. This keeps Markdown from interpreting indented material
as quotes.
-/
import Lean
namespace Lean.Parser
/-- Push `(Syntax.node tk <new-atom>)` onto syntax stack if parse was successful. -/
def mkNodeTokenNoWs (n : SyntaxNodeKind) (startPos : String.Pos) : ParserFn := fun c s => Id.run do
if s.hasError then
return s
let input := c.input
let stopPos := s.pos
let leading := mkEmptySubstringAt input startPos
let val := input.extract startPos stopPos
let wsStopPos := s.pos
let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }
let info := SourceInfo.original leading startPos trailing stopPos
s.pushSyntax (Syntax.mkLit n val info)
partial def interpolatedStrNoIndentFn (p : ParserFn) : ParserFn := fun c s =>
let input := c.input
let stackSize := s.stackSize
let rec parse (startPos : String.Pos) (c : ParserContext) (s : ParserState) : ParserState :=
let i := s.pos
if input.atEnd i then
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "unterminated string literal"
else
let curr := input.get i
let s := s.setPos (input.next i)
if curr == '\"' then
let s := mkNodeToken interpolatedStrLitKind startPos c s
s.mkNode interpolatedStrKind stackSize
else if curr == '\n' then
-- Ignore initial spaces on a new line
let s := mkNodeTokenNoWs interpolatedStrLitKind startPos c s
let s := takeWhileFn (fun curr => curr == ' ') c s
parse s.pos c s
else if curr == '\\' then
andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s
else if curr == '{' then
let s := mkNodeToken interpolatedStrLitKind startPos c s
let s := p c s
if s.hasError then s
else
let i := s.pos
let curr := input.get i
if curr == '}' then
let s := s.setPos (input.next i)
parse i c s
else
let s := s.pushSyntax Syntax.missing
let s := s.mkNode interpolatedStrKind stackSize
s.setError "'}'"
else
parse startPos c s
let startPos := s.pos
if input.atEnd startPos then
s.mkEOIError
else
let curr := input.get s.pos;
if curr != '\"' then
s.mkError "interpolated string"
else
let s := s.next input startPos
parse startPos c s
@[inline] def interpolatedStrNoIndentNoAntiquot (p : Parser) : Parser := {
fn := interpolatedStrNoIndentFn (withoutPosition p).fn,
info := mkAtomicInfo "interpolatedStrNoIndent"
}
def interpolatedStrNoIndent : Parser :=
withAntiquot (mkAntiquot "interpolatedStrNoIndent" interpolatedStrKind) $ interpolatedStrNoIndentNoAntiquot termParser
open Lean.PrettyPrinter
open Lean.PrettyPrinter.Parenthesizer
open Lean.PrettyPrinter.Formatter
@[combinator_parenthesizer interpolatedStrNoIndent]
def interpolatedStrNoIndent.parenthesizer := interpolatedStr.parenthesizer
@[combinator_formatter interpolatedStrNoIndent]
def interpolatedStrNoIndent.formatter := interpolatedStr.formatter
end Lean.Parser
/- Adapted from Init/Meta -/
open Lean
private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do
match Syntax.decodeQuotedChar s i with
| some r => some r
| none =>
let c := s.get i
let i := s.next i
if c == '{' then pure ('{', i)
else none
private partial def decodeInterpStrLit (s : String) : Option String :=
let rec loop (i : String.Pos) (acc : String) : Option String :=
let c := s.get i
let i := s.next i
if c == '\"' || c == '{' then
pure acc
else if c == '\n' then
pure (acc.push c)
else if s.atEnd i then
pure acc
else if c == '\\' then do
let (c, i) ← decodeInterpStrQuotedChar s i
loop i (acc.push c)
else
loop i (acc.push c)
let c := s.get 0
if c == '\"' || c == '}' then
loop ⟨1⟩ ""
else
loop ⟨0⟩ ""
partial def isInterpolatedStrLit? (stx : Syntax) : Option String :=
match Syntax.isLit? interpolatedStrLitKind stx with
| none => none
| some val => decodeInterpStrLit val
open Elab
def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → TermElabM Syntax) (mkElem : Syntax → TermElabM Syntax) : TermElabM Syntax := do
let mut i := 0
let mut result := Syntax.missing
for elem in chunks do
let elem ← match isInterpolatedStrLit? elem with
| none => mkElem elem
| some str => mkElem (Syntax.mkStrLit str)
if i == 0 then
result := elem
else
result ← mkAppend result elem
i := i+1
return result
open TSyntax.Compat in
def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : TermElabM Term := do
let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
`(($r : $type))
server/leanserver/lean-toolchain
+1 -1
View File
@@ -1 +1 @@
leanprover/lean4:nightly-2023-02-10
leanprover/lean4:nightly-2023-03-09
server/testgame/TestGame.lean
+4 -3
View File
@@ -6,7 +6,7 @@ import TestGame.Levels.Predicate
import TestGame.Levels.Contradiction
import TestGame.Levels.Prime
import TestGame.Levels.Sum
import TestGame.Levels.Induction
-- import TestGame.Levels.Induction
import TestGame.Levels.Numbers
import TestGame.Levels.Inequality
@@ -34,8 +34,9 @@ Path Proposition → Implication → Predicate
Path Predicate → Contradiction → Sum → LeanStuff
Path LeanStuff → SetTheory → SetTheory2 → SetFunction
Path Predicate → Prime → Induction
Path Sum → Inequality → Induction
Path Predicate → Prime -- → Induction
Path Sum → Inequality -- → Induction
Path Inequality → Function
Path SetTheory2 → Numbers
Path Module → Basis → Module2
server/testgame/TestGame/LemmaDocs.lean
+35 -9
View File
@@ -75,40 +75,53 @@ Die Definition kann man mit `unfold odd at *` einsetzen.
DefinitionDoc Injective
"
`Injective f` ist als
`Injective f` ist definiert als
```
∀ {a b : U}, a < b → f a < f b
∀ a b, f a = f b → a = b
```
definiert.
"
DefinitionDoc Surjective
"
`Surjective f` ist definiert als
```
∀ a, (∃ b, f a = b)
```
"
DefinitionDoc Bijective
"
"
DefinitionDoc LeftInverse
"
"
DefinitionDoc RightInverse
"
"
DefinitionDoc StrictMono
"
`StrictMono`
`StrictMono f` ist definiert als
```
∀ {a b : U}, f a f b → a = b
∀ a b, a < b → f a < f b
```
"
LemmaDoc not_odd as not_odd in "Nat"
"`¬ (odd n) ↔ even n`"
LemmaDoc even_iff_not_odd as even_iff_not_odd in "Nat"
"`Even n ↔ ¬ (Odd n)`"
LemmaDoc not_even as not_even in "Nat"
"`¬ (even n) ↔ odd n`"
LemmaDoc odd_iff_not_even as odd_iff_not_even in "Nat"
"`Odd n ↔ ¬ (Even n)`"
LemmaDoc even_square as even_square in "Nat"
"`∀ (n : ℕ), even n → even (n ^ 2)`"
"`∀ (n : ℕ), Even n → Even (n ^ 2)`"
@@ -178,3 +191,16 @@ LemmaDoc StrictMono.add as StrictMono.add in "Function"
LemmaDoc Odd.strictMono_pow as Odd.strictMono_pow in "Function"
""
LemmaDoc Exists.choose as Exists.choose in "Function"
""
LemmaDoc Exists.choose_spec as Exists.choose_spec in "Function"
""
LemmaDoc congrArg as congrArg in "Function"
""
LemmaDoc congrFun as congrFun in "Function"
""
LemmaDoc Iff.symm as Iff.symm in "Logic"
""
server/testgame/TestGame/Levels/Contradiction.lean
+6
View File
@@ -8,3 +8,9 @@ import TestGame.Levels.Contradiction.L06_Summary
Game "TestGame"
World "Contradiction"
Title "Widerspruch"
Introduction "
Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
eine Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
gebeten.
"
server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
+35 -45
View File
@@ -15,56 +15,46 @@ Title "Have"
Introduction
"
Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
Zwischenresultat beweisen, welches wir dann benützen können.
Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
dass man anschliessen beweisen muss.
Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
du mit
```
have g : ¬ B
apply h
assumption
```
eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
bevor du dann mit dem Beweis forfährst.
**Oddeus**: Willkommen Reisende! Ich muss eingestehen ich bin in Gedanken noch
an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen?
"
Statement
"Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
$A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
(A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
-- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
-- Zwischenresultat beweisen, welches wir dann benützen können.
-- Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
-- dass man anschliessen beweisen muss.
-- Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
-- du mit
-- ```
-- have g : ¬ B
-- apply h
-- assumption
-- ```
-- eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
-- bevor du dann mit dem Beweis forfährst.
Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
Hint "**Du**: Also als erstes Teile ich wohl mal das Und (`∧`) auf."
rcases k with ⟨h₁, h₂⟩
have h₃ : ¬ B
apply h
assumption
contradiction
Hint "**Du**: Aber jetzt…
Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
"
**Robo**: Du könntest dir ein passendes Zwischenresultat zurechtlegen, das dir hilft:
Mach mal `have g : ¬ B`!"
have g : ¬ B
· Hint "**Du**: Was und jetzt hab ich einfach angenommen das sei richtig?
Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
"
Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"
**Robo**: Ne, jetzt musst du das zuerst beweisen bevor du es dann benützen kannst."
Hint (hidden := true) "**Robo**: `apply` scheint passend zu sein."
apply h
assumption
· Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen?
In Lean :
**Robo**: `contradiction`."
contradiction
```
have k : ¬ B
[Beweis von k]
```
"
NewTactic «have»
DisabledTactic «suffices»
-- example (n : ℕ) : n.succ + 2 = n + 3 := by
-- ring_nf
Conclusion ""
NewTactics «have»
DisabledTactics «suffices»
NewDefinitions Even Odd
NewLemmas not_even not_odd
Conclusion "*Oddeus*: Das stimmt wohl."
server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
+33 -36
View File
@@ -15,52 +15,49 @@ Title "Suffices"
Introduction
"
Die Taktik `suffices` funktioniert genau gleich wie `have`,
vertauscht aber die beiden Beweisblöcke:
```
suffices h : [Aussage]
[Beweis des Goals (mithilfe von h)]
[Beweis der Aussage h]
```
Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
\"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
`suffices` schöner gewesen:
*Oddeus*' Partner meldet sich.
**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
"
-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
-- vertauscht aber die beiden Beweisblöcke:
-- ```
-- suffices h : [Aussage]
-- [Beweis des Goals (mithilfe von h)]
-- [Beweis der Aussage h]
-- ```
-- Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
-- \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
-- Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
-- `suffices` schöner gewesen:
Statement
"Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
$A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
(A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
rcases k with ⟨h₁, h₂⟩
suffices k : ¬ B
(A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
brauchen. Das funktioniert genau gleich, aussert dass dann die beiden Goals vertauscht sind.
**Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
abschliesst bevor ich `g` beweise?
**Robo**: Genau! Verwendende `have` und `suffices` einfach nach gutdünken."
suffices g : ¬ B
Hint "**Robo**: Also hier beendest du den Beweis angenommen {g} sei wahr."
contradiction
Hint "**Robo**: Und hier beweist du das Zwischenresultat."
apply h
assumption
Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
"
NewTactic «suffices»
DisabledTactic «have»
Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
" Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\"
Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
In Lean :
**Oddeus**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
```
suffices k : ¬ B
contradiction
[...]
```
"
Conclusion ""
NewTactics «suffices»
DisabledTactics «have»
NewDefinitions Even Odd
NewLemmas not_even not_odd
Und er führt euch durch seinen Rosengarten."
server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
+39 -29
View File
@@ -15,41 +15,51 @@ Level 3
Title "Per Widerspruch"
Introduction
"
Eine sehr nützliche Beweismethode ist per Widerspruch.
"**Oddeus**: Ich verstehe *Evenine* einfach nicht. Ich will euch auch gleich zeigen,
was sie mir letzthin geschrieben hat, aber zuerst schaut einmal unseren
wunderschönen Absurda-Tempel an!
Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
sucht, und damit jegliches beweisen kann.
Damit kommt ihr vor einen sehr hohen Turm, der ausschliesslich aus Dornenranken gewachsen
scheint.
Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
steht:
**Oddeus**: Versteht ihr, was hier über dem Eingang steht?
"
Statement
"Angenommen $B$ ist falsch und es gilt $A \\Rightarrow B$. Zeige, dass $A$ falsch sein
muss."
(A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
by_contra a
suffices b : B
-- Eine sehr nützliche Beweismethode ist per Widerspruch.
-- Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
-- sucht, und damit jegliches beweisen kann.
-- Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
-- Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
-- Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
-- steht:
Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
Hint "**Robo**: Ein `¬` im Goal heisst häufig, dass du einen Widerspruchsbeweis führen
möchtest.
**Du**: Und wie mach ich das? Mit `contradiction`?
**Robo**: Mit `by_contra h` fängst du einen an. Mit `contradiction` schliesst du ihn dann
später ab."
by_contra h
Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : ¬ {A}`, und damit musst du einen
Widerspruch herbeileiten.
Ein Methode ist, dass du jetzt mit `suffices` sagts, zu was du denn gerne den Widerspruch
haben möchtest, zum Beispiel `suffices k : B`
"
suffices k : B
Hint "**Du**: Ah und jetzt kann ich einfach sagen dass sich die Anahmen `{B}` und `¬{B}`
widersprechen."
contradiction
Hint "**Robo**: Und jetzt kannst du noch das Ergebnis zeigen, das zu einem Widerspruch
geführt hat."
apply g
assumption
NewTactic by_contra
HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) : ¬ A =>
"`by_contra h` nimmt das Gegenteil des Goal als Annahme `(h : A)` und setzt das
Goal auf `False`."
Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
"Jetzt kannst du mit `suffices` oder `have` Fortschritt machen."
HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
"Zum Beispiel `suffices hb : B`."
Conclusion ""
NewTactics by_contra contradiction apply assumption
Conclusion "**Oddeus**: Sehr gut, kommt mit hinein!"
server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
+16 -14
View File
@@ -16,34 +16,36 @@ Title "Per Widerspruch"
Introduction
"
Als Übung zu `by_contra` und dem bisher gelernten, zeige folgendes Lemma welches
wir für die Kontraposition brauchen werden:
*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
**Oddeus**: Ich hab's gleich. Hier ist eine Notiz meiner Gelehrter, die mir
mit solchen kryptischen Nachrichten helfen wollten.
Auf dem Pergament steht das ein Lemma mit dem Namen `not_imp_not`:
"
Statement not_imp_not
"$A \\Rightarrow B$ ist äquivalent zu $\\neg B \\Rightarrow \\neg A$."
(A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
Hint "**Du**: Ich glaube, dafür kenn ich das meiste schon."
Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
constructor
intro h b
by_contra a
Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
herbeiführen."
suffices b : B
contradiction
apply h
assumption
intro h a
Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruch anfangen."
by_contra b
Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
suffices g : ¬ A
contradiction
apply h
assumption
-- TODO: Forbidden Tactics: apply, rw
-- TODO: forbidden Lemma: not_not
DisabledTactic rw
DisabledLemma not_not
HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
""
Conclusion ""
NewTactics contradiction constructor intro by_contra apply assumption
Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"
server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
+44 -40
View File
@@ -14,53 +14,57 @@ Title "Kontraposition"
Introduction
"
Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
*Oddeus* reicht euch das Papier.
```
lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
[...]
```
**Du**: Da steht etwas über `contrapose` hier…
Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
entsprechend umdreht.
**Oddeus**: Das ist doch klar eine Aggression uns gegenüber!
Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
im Goal erstellt.
Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
logisch equivalent sind.
Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
**Robo**: Wartet mal, vielleicht wollte euch eure Schwester einfach von ihren neuen
Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
"
Statement
"Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
(n : ℕ) (h : Odd (n ^ 2)): Odd n := by
-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
-- ```
-- lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
-- [...]
-- ```
-- Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
-- entsprechend umdreht.
-- Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
-- im Goal erstellt.
-- Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
-- Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
-- logisch equivalent sind.
-- Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
Hint "**Oddeus**: Wie soll das den gehen?
**Robo**: `contrapose` benutzt das Lemma eurer Gelehrter, `not_imp_not`. Also es wandelt
ein Goal `A → B` zu `¬B → ¬A ` um.
**Du**: Aber das Goal ist doch gar keine Implikation?
**Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
schieben."
revert h
Hint "*Oddeus*: Ob man jetzt wohl dieses `contrapose` benutzen kann?"
contrapose
rw [not_odd]
rw [not_odd]
Hint (hidden := true) "**Du**: Warte mal, jetzt kann man wohl `even_iff_not_odd` verwenden…"
rw [← even_iff_not_odd]
rw [← even_iff_not_odd]
Hint "**Robo**: Und den Rest hast du bei *Evenine* als Lemma gezeigt!"
apply even_square
HiddenHint (n : ℕ) (h : Odd (n ^ 2)) : Odd n =>
"Um `contrapose` anzuwenden, brauchen wir eine Implikation `Odd (n ^ 2) → Odd n` im
Goal. Benutze `revert h`!"
NewTactic contrapose
DisabledTactic by_contra
Hint (n : ℕ) : Odd (n ^ 2) → Odd n =>
"Mit `contrapose` kann man die Implikation zu
`¬ (Not n) → ¬ (Odd n^2)` umkehren."
Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`."
HiddenHint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden."
Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
"rw [not_odd] muss hier zweimal angewendet werden."
Hint (n : ℕ) : Even n → Even (n ^ 2) =>
"Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
NewTactics contrapose rw apply
NewDefinitions Even Odd
NewLemmas not_even not_odd even_square
Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
Ich danke euch, darauf wäre ich nie gekommen."
server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
+24 -44
View File
@@ -14,63 +14,43 @@ Title "Contradiction"
Introduction
"
**Du**: Sag mal Robo, das hätte ich aber auch als Widerspruch anstatt Kontraposition
beweisen können?
**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
Probiers doch einfach!
In diesem Kapitel hast du also folgende Taktiken kennengelernt:
| | Taktik | Beispiel |
|:------|:----------------|:-------------------------------------------------------|
| 16 | `have` | Zwischenresultat annehmen. |
| 17 | `suffices` | Zwischenresultat annehmen. |
| 18 | `by_contra` | Widerspruch. (startet einen Widerspruch) |
| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* |
| 19 | `contrapose` | Contraposition. |
| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. |
Als Vergleich zwischen Beweisen \"per Widerspruch\"
und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
du mit `by_contra` einen Widerspruch suchst.
"
Statement
"Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
(n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
Hint "**Robo**: Fang diesmal mit `by_contra g` an!"
by_contra g
Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
suffices d : ¬ Odd (n ^ 2)
contradiction
rw [not_odd] at *
rw [←even_iff_not_odd] at *
apply even_square
assumption
HiddenHint (n : ℕ) (h : Odd (n^2)) : Odd n =>
"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten."
DisabledTactic contrapose revert
Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False =>
Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
Mond gelernt haben:
| | Taktik | Beispiel |
|:------|:----------------|:-------------------------------------------------------|
| 177 | `have` | Zwischenresultat annehmen. |
| 18 | `suffices` | Zwischenresultat annehmen. |
| 19 | `by_contra` | Widerspruch. (startet einen Widerspruch) |
| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* |
| 20 | `contrapose` | Kontraposition. |
| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. |
"
Am sinnvollsten ist es, hier einen Widerspruch zu `Odd (n^2)` zu suchen.
Dafür kannst du
```
suffices k : ¬ Odd (n ^ 2)
contradiction
```
benützen.
"
HiddenHint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False =>
"Hier brauchst du nur `contradiction`."
Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) =>
"Das Zwischenresultat `¬Odd (n^2)` muss auch bewiesen werden.
Hier ist wieder das Lemma `not_Odd` hilfreich."
HiddenHint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) =>
"Mit `rw [not_Odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben."
Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
"Diese Aussage hast du bereits als Lemma bewiesen."
HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
"Probiers mit `apply ...`"
NewTactics contradiction by_contra rw apply assumption -- TODO: suffices, have
NewDefinitions Even Odd
NewLemmas not_odd not_even even_square
server/testgame/TestGame/Levels/Function.lean
+18 -7
View File
@@ -1,13 +1,24 @@
import TestGame.Levels.Function.L01_Function
import TestGame.Levels.Function.L02_Let
import TestGame.Levels.Function.L03_Composition
import TestGame.Levels.Function.L06_Piecewise
import TestGame.Levels.Function.L07_Injective
import TestGame.Levels.Function.L07'_Injective
import TestGame.Levels.Function.L08_Injective
import TestGame.Levels.Function.L09_Surjective
import TestGame.Levels.Function.L10_Bijective
import TestGame.Levels.Function.L03_Piecewise
import TestGame.Levels.Function.L04_Injective
import TestGame.Levels.Function.L05_Injective
import TestGame.Levels.Function.L06_Injective
import TestGame.Levels.Function.L07_Surjective
import TestGame.Levels.Function.L08_Bijective
import TestGame.Levels.Function.L09_Inverse
import TestGame.Levels.Function.L11_Inverse
Game "TestGame"
World "Function"
Title "Abbildungen"
Introduction "
Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf
eine Insel komplett mit Wasser bedeckt zu sein scheint.
Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,
vereinzelte aus Lehm.
Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt.
"
server/testgame/TestGame/Levels/Function/L01_Function.lean
+46 -18
View File
@@ -5,31 +5,59 @@ Game "TestGame"
World "Function"
Level 1
Title ""
Title "Anonyme Funktionen"
Introduction
"
Funktionen werden in Lean mit `ℕ → ℕ` geschrieben (`\\to`), also dem gleichen
Pfeil wie Implikationen.
Eine abstrakte Funktion ist ein entsprechendes Element `(f : ℕ → ℕ)` oder `(g : ℕ → ℝ)`.
Dies sagt aber gar nichts darüber, wie `f` tatsächlich definiert ist.
Hat man eine Funktion `(f : A → B)` und ein Element `(x : A)` dann ist `f x` der
Bildpunkt in `B`. In Lean braucht man also keine Klammern um $f(x)$ zu schreiben.
Eplizite, anonyme Funktionen kann man mit dem Syntax `fun (n : ℕ) ↦ n ^ 2` definieren
(entweder `↦` (`\\map`) oder `=>` als Pfeil in der Mitte).
Auf die Frage hin, ob sie von einem Bibliothek wisse, erzählt euch das kleine Mädchen,
dass es auf der Insel nur einen gäbe, aber sie bedrängt euch so mit einer Frage,
dass sie euch gar nicht sagt, wo dieser zu finden sei.
"
Statement
"Zeige, dass es eine Funktion $\\mathbb{N} \\to \\mathbb{Z}$ gibt, für die $f(x) < x$ gilt."
: ∃ f : ℕ → ℤ, ∀ x, f x < x := by
Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by
use (fun x ↦ x - 1)
simp
Hint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
Hint : ∃ f : ℤ → ℤ, ∀ x, f x < x =>
"
Benütze eine anonyme Funktion `use (fun n ↦ _)` wobei `_` durch einen Ausdruck ersetzt
werden muss, so dass die Aussage erfüllt wird.
**Robo**: `f : ℤ → ℤ` ist die Notation für eine Funktion und `f x` ist diese Funktion
angewendet auf ein Element `(x : ℤ)`.
**Du**: War `→` nicht eben noch eine Implikation?
**Robo**: Doch, die brauchen das gleiche Zeichen für beides.
**Du**: Dann ist `f : ℤ → ℤ` also einfach abstrakt irgendeine Funktion,
wie definier ich aber jetzt konkret eine Abbildungsvorschrift?
**Robo**: Man kennt hier eine Notation für eine anonyme Funktion:
`fun (x : ℤ) ↦ x ^ 2` ist
$$
\\begin\{aligned}
f : \\mathbb\{ℤ} &\\to \\mathbb\{ℤ} \\\\
x &\\mapsto x ^ 2
\\end\{aligned}
$$
**Robo**: PS, `↦` ist `\\mapsto`. Aber man kann auch stattdessen `=>` benützen.
"
HiddenHint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
"
**Du**: Ja aber was mach ich damit?
**Robo**: Wie immer gehst du ein `∃` mit `use …` an.
"
-- TODO: Why does this not show?
HiddenHint : ∀ (x : ℤ), (fun (y : ℤ) => y - 1) x < x =>
"**Du**: Zu was sich das wohl vereinfacht?"
HiddenHint (x : ℤ) : (fun y => y - 1) x < x =>
"**Du**: Zu was sich das wohl vereinfacht?"
Conclusion "Das Mädchen wird kurz ruhig, dann beginnt es zu lächeln und zeigt strahlend
in eine Richtung. Ihr folgt ihrem Finger und euch fällt in weiter ferne eine pompöse Struktur
auf einem flachen Hügel auf.
"
server/testgame/TestGame/Levels/Function/L02_Let.lean
+58 -52
View File
@@ -5,72 +5,78 @@ Game "TestGame"
World "Function"
Level 2
Title ""
Title "let"
Introduction
"
Ausserhalb eines Beweises kann man Funktionen mit `def`
(anstatt `lemma`/`example`/`theorem`) definieren:
Ihr macht euch auf Richtung Bibliothek entlang kleiner Pfade zwischen verschiedenster Behausungen.
**Du**: Sag mal, ich weiss jetzt dass ich eine Funktion als `fun x ↦ x - 1` definieren kann,
aber wie kann ich der einen Namen geben?
**Robo**: Wenn jemand hier eine Funktion definiert, werden die dir
`def f (x : ℤ) : ℤ := x - 1` oder `def f : ℤ → ℤ := (fun x ↦ x - 1)` geben.
**Du**: Und das bedeutet beides das gleiche?
**Robo**: Praktisch, ja. Aber! Wenn du eine Funktion in einer Aufgabe benennen willst,
schreibst du `let f := fun (x : ℤ) ↦ x - 1`!
**Du**: Und was ist der Unterschied?
**Robo**: Deines mit `let` ist für innerhalb von einem Beweis, das andere mit `def`
ist für ausserhalb von einem Beweis. Hier, ich geb dir mal eine Aufgabe:
```
def f (x : ℚ) : ℚ := 1 / (1 + x^2)
def f : ℚ → ℚ := fun x ↦ 1 / (1 + x^2)
def f (x : ℤ) : ℤ := (x + 4)
```
(die beiden Varianten sind äquivalent.)
Um eine anonyme Funktion `fun x ↦ 1 / (1 + x^2)` **innerhalb** eines Beweis einem Namen
zuzuordnen, benützt man `let`:
```
let f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
```
`def` und `let` funktionieren also fast gleich wie `lemma`/`example`/`theorem` und `have` mit
einem wichtigen Unterschied:
```
have f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
let f₂ : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
```
`have` vergisst sofort den \"Beweis\", das heisst, Lean weiss dann nur, dass es eine
Funktion `(f : ℕ → ℕ)` gibt, aber nicht, wie diese definiert ist. `let` hingegen speichert
die Definition der Funktion.
Manchmal muss man Definitionen (von einem `def` oder `let` Statement) mit `unfold` einsetzen.
und:
"
def f (x : ℤ) : ℤ := (x + 1) ^ 2
def f (x : ℤ) : ℤ := (x + 4)
Statement
"
Given the function
```
def f (x : ℤ) : ℤ := (x + 1) ^ 2
```
show that $f(x) = x^2 + 2x + 1$.
"
: ∀ x, f x = x ^ 2 + 2 * x + 1 := by
intro x
Statement "" (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by
let g := fun (x : ℤ) ↦ x - 3
use g
simp
unfold f
ring
NewTactics «let»
OnlyTactics «let» intro unfold ring
NewTactic «let»
NewLemma Function.comp_apply
HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 =>
"Fang zuerst wie immer mit `intro x` an."
Hint (x : ℤ) : ∃ g, (g ∘ f) x = x + 1 =>
"**Du**: Ist `g ∘ f` Komposition von Funktionen?
Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
"
Definitionen muss man manchmal manuell einsetzen um den Taktiken zu helfen.
**Robo**: Richtig! Das schreibt man mit `\\comp`.
Das macht man mit `unfold f` (oder alternativ mit `rw [f]`).
**Du** Und hier könnte ich also zuerst
`let g := fun (x : ℤ) ↦ _` definieren, anstatt direkt
`use fun (x : ℤ) ↦ _`?
**Robo**: Genau! Das ist zwar praktisch das gleiche, aber kann manchmal nützlich sein.
"
HiddenHint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
"
Nachdem die Definition von `f` eingesetzt ist, übernimmt `ring` den Rest"
-- TODO: Make some hints work here
Hint (x : ℤ) : ((fun (x : ℤ) ↦ x - 3) ∘ f) x = x + 1 =>
"**Robo**: Manchmal must du nachhelfen und Funktionen mit `unfold f` öffnen, manchmal nicht.
Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
-- TODO : Make this work
Hint (x : ℤ) (g := (fun (x : ℤ) ↦ x - 3)) : (g ∘ f) x = x + 1 =>
"**Robo**: `(g ∘ f) x` ist per Definition `g (f x)`, aber mit
`rw [Function.comp_apply]` kann man das explizit umschreiben, aber `simp` kennt das
Lemma auch."
Hint (x : ℤ) : f x - 3 = x + 1 =>
"**Robo**: Manchmal must du nachhelfen und Definitionen mit `unfold f` öffnen, mamchmal klappts
ohne.
Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
-- TODO: Block simp-Lemma
Conclusion "**Du**: Dann verstehst du etwas Mathe?
**Robo**: Ich hatte ja keine Ahnung ob die generierte Aufgabe beweisbar ist…
Und damit erreicht ihr den Hügel mit der Bibliothek."
server/testgame/TestGame/Levels/Function/L03_Composition.lean
-22
View File
@@ -1,22 +0,0 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 3
Title ""
Introduction
"
Komposition von Funktionen kann als `g ∘ f` geschrieben werden.
TODO
"
Statement
"TODO: Find an exercise."
(U T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x) := by
simp only [Function.comp_apply]
NewLemmas Function.comp_apply
server/testgame/TestGame/Levels/Function/L06_Piecewise.lean → server/testgame/TestGame/Levels/Function/L03_Piecewise.lean
+13 -15
View File
@@ -3,13 +3,14 @@ import Mathlib
Game "TestGame"
World "Function"
Level 4
Level 3
Title ""
Title "Komposition"
Introduction
"
Du kommst an eine Tür mit zwei Wächtern. Der eine hat ein Schild
Endlich kommt ihr zur Bibliothek. Komischerweise stehen an der Tür
zwei Wächtern. Der eine zeigt euch ein Blatt mit
```
def f : ℚ → ℚ := fun x ↦ 5 * x
@@ -21,11 +22,9 @@ der andere eines mit
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
```
Auf der Tür steht groß:
und gibt Dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
"
example (P : Prop) [Decidable P] (a b : ℕ) (h : P) : ite P a b = a := if_pos h
open Set
namespace LevelFunction4
@@ -33,11 +32,6 @@ namespace LevelFunction4
def f : ℚ → ℚ := fun x ↦ 5 * x
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
-- #eval (f2 + f2) 2
-- #check range f2
Statement ""
: f ∘ g = g ∘ f := by
funext x
@@ -57,9 +51,9 @@ Statement ""
unfold f
ring
NewTactics funext by_cases simp_rw linarith
NewTactic funext by_cases simp_rw linarith
NewLemmas not_le if_pos if_neg
NewLemma not_le if_pos if_neg
Hint : f ∘ g = g ∘ f =>
@@ -72,6 +66,7 @@ Hint : f ∘ g = g ∘ f =>
dann für dieses.
"
-- TODO : This does not trigger.
-- TODO: These 5 hints should be mutually exclusive. i.e. they should not trigger
-- if a assumption is missing.
Hint (x : ℚ) : (f ∘ g) x = (g ∘ f) x =>
@@ -92,12 +87,15 @@ könnte mit dem Lemma `not_le` zwischen `¬(0 ≤ {x})` und `0 < {x}` wechseln.
Hint (x : ℚ) (h : 0 ≤ x) : f (g x) = g (f x) =>
"
**Robo**: Um das ausrechnen zu können, brauchst du nicht nur `0 ≤ x` sondern auch noch
eine Annahme `0 ≤ f x`.
eine neue Annahme `0 ≤ f x`.
**Du**: Also `have h₂ : _`?
"
Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = g (f x) =>
"
**Du**: Mit den beiden Annahmen habe ich ja jetzt `(if 0 ≤ x then _)` wobei `0 ≤ x` wahr ist,
**Du**: Mit den beiden Annahmen sagt die Definition von `g` ja z.B.
`(if 0 ≤ x then _)` wobei ich weiss dass `0 ≤ x` wahr ist,
kann ich das dann einfach vereinfachen?
**Robo**: Dafür must du zuerst die Definition von `g` öffnen, also `unfold`. Und dann mit
server/testgame/TestGame/Levels/Function/L07_Injective.lean → server/testgame/TestGame/Levels/Function/L04_Injective.lean
+3 -3
View File
@@ -3,13 +3,13 @@ import Mathlib
Game "TestGame"
World "Function"
Level 5
Level 4
Title ""
Introduction
"
Ihr läuft durch verschiedenste Leere Gänge des Funktionentempels.
Ihr läuft durch verschiedenste Gänge der Bibliothek, allesamt mit Büchern entlang der Wände.
**Du**: Wenn wir wüssten, dass nur ein möglicher Weg hierhin führt, könnten wir
ausschliessen, dass wir im Kreis laufen.
@@ -22,7 +22,7 @@ Statement "" : Injective (fun (n : ℤ) ↦ n + 3) := by
intro a b
simp
NewDefinitions Injective
NewDefinition Injective
Hint : Injective (fun (n : ℤ) ↦ n + 3) =>
"**Robo**: `Injective` ist als `∀ \{a b : U}, f a = f b → a = b`
server/testgame/TestGame/Levels/Function/L07'_Injective.lean → server/testgame/TestGame/Levels/Function/L05_Injective.lean
+4 -4
View File
@@ -5,7 +5,7 @@ set_option tactic.hygienic false
Game "TestGame"
World "Function"
Level 6
Level 5
Title ""
@@ -29,8 +29,8 @@ Statement "" : Injective (fun (n : ℤ) ↦ n^3 + (n + 3)) := by
intro a b
simp
NewDefinitions Injective
NewLemmas StrictMono.injective StrictMono.add Odd.strictMono_pow
NewDefinition Injective
NewLemma StrictMono.injective StrictMono.add Odd.strictMono_pow
Hint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
@@ -76,4 +76,4 @@ Hint (a b : ℤ) (h : a ^ 3 + (a + 3) = b ^ 3 + (b + 3)) : a = b =>
Conclusion "**Du**: Danke vielmals!
Und ihr läst das Wesen mit im Gang stehen weiter über Injectivität nachdenkend."
Und damit lässt das Wesen mitten im Gang stehen, wo es weiter über Injektivität nachdenkt."
server/testgame/TestGame/Levels/Function/L08_Injective.lean → server/testgame/TestGame/Levels/Function/L06_Injective.lean
+3 -3
View File
@@ -3,7 +3,7 @@ import Mathlib
Game "TestGame"
World "Function"
Level 7
Level 6
Title "Injektive"
@@ -13,13 +13,13 @@ Weiterirrend kommt ihr an eine Verzweigung.
**Robo**: Sieht beides gleich aus.
Ein paar Schritte in den linken Korridor hinein seht ihr gekritzel an der Wand:
Ein paar Schritte in den linken Korridor hinein seht ihr auf dem Boden ein Blatt mit Gekritzel:
```
def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
```
**Du**: Hier haben wir eine stückweis definierte Funktion
**Du**: Hier haben wir wieder eine stückweise Funktion
$$
f(n) = \\begin{cases}
server/testgame/TestGame/Levels/Function/L07_Surjective.lean
+37
View File
@@ -0,0 +1,37 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 7
Title "Surjektive"
Introduction
"
Endlich kommt ihr in einen große, beleuchteten zentralen Raum.
Alle Wände sind voll mit Büchern und
in der Mitte sitzt an einem einsamen
Tisch ein Gelehrter, der tatsächlich das gesuchte Buch zeigen kann.
Bevor er dieses aushändigt, will er aber folgendes wissen:
"
open Function
Statement "" : Surjective (fun (n : ℤ) ↦ n + 1) := by
intro y
use y-1
simp
NewDefinition Surjective
Hint : Surjective (fun (n : ℤ) ↦ n + 1) =>
"**Robo**: Die Definition von `Surjective f` ist `∀ y, (∃ x, f x = y)`.
**Du**: Dann kann ich das auch einfach wie Quantifier behandeln?
**Robo**: Schieß drauf los!"
Conclusion
"Der Gelehrte händigt euch schmunzelnd das Buch aus."
server/testgame/TestGame/Levels/Function/L08_Bijective.lean
+38
View File
@@ -0,0 +1,38 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 8
Title ""
Introduction
"
**Du**: Ehm, und wie kommen wir da wieder raus?
**Gelehrter**: Gerne zeige ich euch den Weg, nachdem ihr mir auch noch folgendes erklärt:
"
open Function
Statement "" : Bijective (fun (n : ℤ) ↦ n + 1) := by
unfold Bijective
constructor
intro a b
simp
intro y
use y-1
simp
Hint : Bijective (fun (n : ℤ) ↦ n + 1) =>
"**Robo** *(flüsternd)*: `Bijectve f` ist als `Injective f ∧ Surjective f` definiert.
**Du**: Dann ist das ja ganz simpel!
"
Conclusion
"Zufrieden drückt euch der Gelehrte eine neue Fackel in die Hand und
zeigt euch den Weg nach draussen."
NewDefinition Bijective
server/testgame/TestGame/Levels/Function/L09_Inverse.lean
+61
View File
@@ -0,0 +1,61 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 9
Title "Inverse"
Introduction
"
Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
und der Gelehrte möchte wissen, wie das den genau ginge.
Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
"
open Function
--TODO: This is a really hard proof
Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
constructor
intro h
use fun x => (h.2 x).choose
constructor
· intro x
simp
apply h.1
apply Exists.choose_spec (h.2 (f x))
· intro x
simp
apply Exists.choose_spec (h.2 x)
intro ⟨g, h₁, h₂⟩
constructor
· intro a b hab
have h : g (f a) = g (f b)
· apply congrArg
assumption
rw [h₁, h₁] at h
assumption
· intro x
use g x
rw [h₂]
NewDefinition LeftInverse RightInverse
NewLemma Exists.choose Exists.choose_spec congrArg congrFun
DisabledLemma Function.bijective_iff_has_inverse
Hint {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f =>
"**Du**: Nah da sagt mir so manches nichts, aber ich kann ja mal mit dem `↔` anfangen, das kenn
ich ja schon."
Conclusion
"Endlich entkommt ihr der Bibliothek.
**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"
server/testgame/TestGame/Levels/Function/L09_Surjective.lean
-19
View File
@@ -1,19 +0,0 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 8
Title "Surjektive"
Introduction
"
"
Statement
""
: (fun (n : ℤ) ↦ n + 1).Surjective := by
intro y
use y-1
simp
server/testgame/TestGame/Levels/Function/L10_Bijective.lean
-23
View File
@@ -1,23 +0,0 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 9
Title ""
Introduction
"
"
Statement
""
: (fun (n : ℤ) ↦ n + 1).Bijective := by
constructor
intro a b hab
simp at hab
assumption
intro y
use y-1
simp
server/testgame/TestGame/Levels/Function/L11_Inverse.lean
+93
View File
@@ -0,0 +1,93 @@
import TestGame.Metadata
import Mathlib
Game "TestGame"
World "Function"
Level 10
Title "Inverse"
Introduction
"
Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
und der Gelehrte möchte wissen, wie das den genau ginge.
Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
"
open Function
set_option pp.rawOnError true
Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
Branch
exfalso
Hint "Das war eine blöde Idee
dd
ddds
"
Hint (hidden := true) "constructor"
constructor
Hint "intro h" -- does not show
intro h
Hint "rcases h with ⟨h₁, h₂⟩" -- shows too late: 1, 2 after
rcases h with ⟨h₁, h₂⟩
Hint (strict := true) "let g := fun x => (h₂ x).choose" -- shows correct + 1 after
let g := fun x => (h₂ x).choose
Hint "use g"
use g
Hint "constructor" -- does not show
constructor
Hint "intro x" -- does not show
intro x
Hint "simp" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
simp
Hint "apply h₁"
apply h₁
Hint "apply Exists.choose_spec (h₂ (f x))"
apply Exists.choose_spec (h₂ (f x))
Hint "intro y" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
intro y
Hint "simp"
simp
Hint "apply Exists.choose_spec (h₂ y)"
apply Exists.choose_spec (h₂ y)
Hint "intro ⟨g, h₁, h₂⟩"
intro ⟨g, h₁, h₂⟩
Hint "constructor"
constructor
Hint "intro a b hab"
intro a b hab
Hint (strict := true) "have h : g (f a) = g (f b)"
have h : g (f a) = g (f b)
Hint "apply congrArg"
apply congrArg
Hint "assumption"
assumption
Hint "rw [h₁, h₁] at h"
rw [h₁, h₁] at h
Hint "assumption"
assumption
Hint "intro x"
intro x
Hint "use g x"
use g x
Hint "rw [h₂]"
rw [h₂]
-- NewDefinition LeftInverse RightInverse
-- NewLemma Exists.choose Exists.choose_spec congrArg congrFun
-- DisabledLemma Function.bijective_iff_has_inverse
Hint (A B: Type) (f : A → B) (h : Bijective f) :
(∃ g, LeftInverse g f ∧ RightInverse g f) → Bijective f =>
"Test"
Conclusion
"Endlich entkommt ihr dem Tempel.
**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"
server/testgame/TestGame/Levels/Implication.lean
+8 -4
View File
@@ -8,8 +8,9 @@ import TestGame.Levels.Implication.L07_Rw
import TestGame.Levels.Implication.L08_Iff
import TestGame.Levels.Implication.L09_Iff
import TestGame.Levels.Implication.L10_Apply
import TestGame.Levels.Implication.L11_Rw
import TestGame.Levels.Implication.L12_Summary
import TestGame.Levels.Implication.L11_ByCases
import TestGame.Levels.Implication.L12_Rw
import TestGame.Levels.Implication.L13_Summary
Game "TestGame"
World "Implication"
@@ -21,10 +22,13 @@ Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die
beide bewohnt zu sein scheinen.
**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
aber niemand von den Einwohnern...
aber niemand von den Einwohnern wusste was davon...
**Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
erzählen…
Und damit leitet Robo den Landeanflug ein.
Und damit leitet Robo den Landeanflug ein. Implis scheint ein riesiger Tagbau zu sein auf
dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und queer.
Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
"
server/testgame/TestGame/Levels/Implication/L01_Intro.lean
+13 -20
View File
@@ -1,4 +1,5 @@
import TestGame.Metadata
import Mathlib.Tactic.Tauto
set_option tactic.hygienic false
@@ -10,31 +11,23 @@ Title "Intro"
Introduction
"
## Implikationen
In diesem Kapitel lernst du Implikation ($\\Rightarrow$) und Genau-dann-wenn
($\\Leftrightarrow$) kennen.
Dazu lernst du, wie man bereits bewiesene Sätze verwendet.
Seien `(A B : Prop)` zwei logische Aussagen. Eine Implikation $A \\Rightarrow B$ schreibt
man in Lean als `A → B` (`\\to`).
Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit
`intro ha` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen.
**Operationsleiter**: Sagt mal, könnt ihr mir hier weiterhelfen?
"
Statement
"Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr."
(A B : Prop) (hb : B) : A → (A ∧ B) := by
Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
Hint "**Du**: Einen Moment, das ist eine Implikation (`\\to`),
also `A` impliziert `A und B`, soweit so gut, also eine Tautologie.
**Robo**: Die scheinen hier `tauto` auch nicht zu verstehen.
Implikationen kannst du aber mit `intro h` angehen."
intro hA
Hint "**Du**: Jetzt habe ich also angenommen, dass `A` wahr ist und muss `A ∧ B` zeigen,
das kennen wir ja schon."
constructor
assumption
assumption
HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
"Mit `intro ha` kann man annehmen, dass $A$ wahr ist. danach muss man $A \\land B$ zeigen."
Conclusion "Der Operationsleiter nickt bedacht."
Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
"Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
NewTactics intro constructor assumption
NewTactic intro
DisabledTactic tauto
server/testgame/TestGame/Levels/Implication/L02_Revert.lean
+12 -24
View File
@@ -9,34 +9,22 @@ Level 2
Title "Revert"
Introduction
"
Mit `intro` kann man also eine Implikation aus dem Goal entfernen, indem man
die Implikationsprämisse zu den *Annahmen* hinzufügt:
"Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
```
example : A → B :=
[Beweis]
```
Statement (A B : Prop) (ha : A) (h : A → B) : B := by
Hint "**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
wird zu
**Du**: Das wirkt etwas unnatürlich.
```
example (ha : A) : B :=
[Beweis]
```
Seltener kann auch die andere Richtung nützlich sein. Mit `revert ha` kann man die Annahme
`ha` entfernen und als Implikationsprämisse vor's Goal hängen.
"
Statement
"Angenommen $A$ ist eine wahre Aussage und man hat eine Implikation $A \\Rightarrow B$, zeige
dass $B$ wahr ist."
(A B : Prop) (ha : A) (h : A → B) : B := by
**Robo**: Schon, ja. Aber als Tool kann das manchmal nützlich sein."
revert ha
assumption
HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
"Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
NewTactics revert assumption
Daraufhin lächelt der Fragende nur vorahnend."
NewTactic revert
DisabledTactic tauto
server/testgame/TestGame/Levels/Implication/L03_Apply.lean
+12 -11
View File
@@ -9,6 +9,8 @@ Title "Apply"
Introduction
"
Sein Kollege zieht eine Linie unter deinen Beweis, schreibt ein durchgestrichenes ~`revert`~
hin und gibt dir das Blatt wieder.
`revert` ist aber nur selten der richtige Weg.
Im vorigen Beispiel würde man besser die Implikation $A \\Rightarrow B$ *anwenden*, also
@@ -18,21 +20,20 @@ Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die K
(also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen.
"
Statement
"Seien $A, B$ logische Aussagen, wobei $A$ wahr ist und $A \\Rightarrow B$.
Zeige, dass $B$ wahr ist."
(A B : Prop) (hA : A) (g : A → B) : B := by
apply g
Statement (A B : Prop) (hA : A) (h : A → B) : B := by
Hint "**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
`apply {h}` die Implikation anzuwenden."
apply h
Hint "**Du**: Und jetzt genügt es also `A` zu zeigen."
assumption
HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B =>
"Mit `apply g` kannst du die Implikation `g` anwenden."
Conclusion "**Robo** Übrigens mit `apply LEMMA` kannst auch jedes Lemma anwenden, dessen
Aussage mit dem Goal übereinstimmt.
HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
dafür hast du bereits einen Beweis in den Annahmen."
Die beiden Fragenden schauen das Blatt an und murmeln zustimmend."
NewTactics apply assumption
NewTactic apply
DisabledTactic revert tauto
-- Katex notes
-- `\\( \\)` or `$ $` for inline
server/testgame/TestGame/Levels/Implication/L04_Apply.lean
+17 -14
View File
@@ -10,26 +10,29 @@ Title "Implikation"
Introduction
"
Hier eine Übung zu Implikationen.
Fast immer ist es der richtige Weg, wenn du mit `intro` anfängst.
**Du** *(zu Robo)*: Testen die uns eigentlich hier?
Ein älteres Gruppenmitglied schiebt ein Tablet über den Tisch und beginnt in leiser
Stimme zu erklären.
**Mitarbeiterin**: Eines unserer Kontrollelemente ist kaputt und ist verwirrt, wo Sachen hinkommen.
Gesteuert werden diese über Panels, und hier hab ich das Übungspanel, mit dem wir neue
Ingeneure ausbilden:
"
Statement
"Angenommen man weiss $A \\Rightarrow B \\Rightarrow C$, zeige dass $A \\Rightarrow C$."
(A B C : Prop) (f : A → B) (g : B → C) : A → C := by
Statement (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
Hint "**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
kombinieren?
**Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch."
intro hA
Hint (hidden := true) "**Robo**: Das ist wieder eine Anwendung von `apply`."
apply g
apply f
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
"Mit `intro hA` kann man annehmen, dass $A$ wahr ist. danach muss man $B$ zeigen."
Conclusion "**Du**: Ich hab das Konzept verstanden.
Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
"Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
Die Mitarbeiterin ist zufrieden und wünscht euch Glück auf der Mission."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
"Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
diese mit `apply` an."
NewTactics intro apply assumption revert
DisabledTactic tauto
server/testgame/TestGame/Levels/Implication/L05_Apply.lean
+24 -24
View File
@@ -8,46 +8,46 @@ Title "Implikation"
Introduction
"
Noch eine Übung: Angenommen man hat folgende Implikationen:
Selbstsicher folgt ihr den Anweisungen und geht nach draussen zum
defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
$$
\\begin{CD}
A @>{f}>> B @<{g}<< C \\\\
@. @V{h}VV @V{m}VV \\\\
D @>{i}>> E @>{k}>> F
D @>{i}>> E @>{k}>> F \\\\
@A{m}AA @A{n}AA @V{p}VV \\\\
G @<{q}<< H @>{r}>> I
\\end{CD}
$$
"
Statement
"Beweise $A \\Rightarrow F$."
(A B C D E F : Prop) (f : A → B) (g : C → B) (h : B → E)
(i : D → E) (k : E → F) (m : C → F) : A → F := by
(A B C D E F G H I : Prop)
(f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
(n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
**Robo**: Und dann fängst du am besten wieder mit `intro` an."
intro ha
Branch
apply r
Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
apply p
apply k
apply h
Branch
apply g
Hint "**Robo**: Nah, da stimmt doch was nicht…"
apply f
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
(f : A → B) (g : C → B) (h : B → E)
(i : D → E) (k : E → F) (m : C → F) : A → F =>
"Wieder ist es schlau, mit `intro` anzufangen."
Conclusion
"Mit einem lauten Ratteln springen die Förderbänder wieder an.
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
(hA : A) (f : A → B) (g : C → B) (h : B → E)
(i : D → E) (k : E → F) (m : C → F) : F =>
"Versuch mit `apply` den richtigen Weg zu finden."
**Operationsleiter**: Vielen Dank euch! Kommt ich geb euch eine Führung und stell euch den
Technikern hier vor."
Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
(hA : A) (f : A → B) (g : C → B) (h : B → E)
(i : D → E) (k : E → F) (m : C → F) : C =>
"Sackgasse. Probier doch einen anderen Weg."
Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
(hA : A) (f : A → B) (g : C → B) (h : B → E)
(i : D → E) (k : E → F) (m : C → F) : D =>
"Sackgasse. Probier doch einen anderen Weg."
NewTactics apply assumption revert intro
DisabledTactic tauto
-- https://www.jmilne.org/not/Mamscd.pdf
server/testgame/TestGame/Levels/Implication/L06_Iff.lean
+22 -19
View File
@@ -8,36 +8,39 @@ Title "Genau dann wenn"
Introduction
"
Genau-dann-wenn, $A \\Leftrightarrow B$, wird als `A ↔ B` (`\\iff`) geschrieben.
`A ↔ B` ist eine Struktur (ähnlich wie das logische UND), die aus zwei Teilen besteht:
Als erstes kommt ihr in einen kleinen Raum mit ganz vielen Bildschirmen.
- `mp`: die Implikation $A \\Rightarrow B$.
- `mpr`: die Implikation $B \\Rightarrow A$.
Ein junges Wesen dreht sich auf dem Stuhl um, und sagt:
Hat man ein $\\Leftrightarrow$ im Goal, nimmt man dieses ebenfalls mit der Taktik
`constructor` auseinander und zeigt dann beide Richtungen einzeln.
**Mitarbeiter**: Oh hallo! Schaut euch mal das hier an!
"
Statement
"Zeige dass `B ↔ C`."
(A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
Hint "**Robo**: Das ist ein genau-dann-wenn Pfeil: `\\iff`. Er besteht aus zwei Teilen:
`A ↔ B` ist als `⟨A → B, B → A⟩` definiert.
**Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
**Robo**: Genau. Entsprechend kannst du hier auch mit `constructor` anfangen."
constructor
Hint "**Du**: Ah und die beiden hab ich schon in den Annahmen."
assumption
assumption
HiddenHint (A : Prop) (B : Prop) : A ↔ B =>
"Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen."
HiddenHint (A : Prop) (B : Prop) (h : A → B) : A → B =>
"Such mal in den Annahmen."
Conclusion
"
Die Taktik `constructor` heisst so, weil `↔` als \"Struktur\" definiert ist, die
aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, es soll versuchen,
ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen,
hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
**Operationsleiter**: \"Modulo Ponens\" ist ein lokaler Begriff hier,
aber das ist doch nicht wichtig.
**Robo**: Und das \"r\" in `mpr` stünde für \"reverse\" weils die Rückrichtung ist.
"
NewTactics constructor assumption
NewTactic constructor
DisabledTactic tauto rw
-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
server/testgame/TestGame/Levels/Implication/L07_Rw.lean
+24 -53
View File
@@ -11,64 +11,35 @@ Title "Genau dann wenn"
Introduction
"
Hat man ein `(h : A ↔ B)` in den Annahmen, hat man die gleichen beiden Optionen wie beim
logischen UND plus noch eine neue:
Als nächstes begenet ihr jemandem im Flur.
1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
direkt auswählen.
2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
3. **Mit** `rw [h]` **kann man im Goal `A` durch `B` ersetzen.**
Wir widmen uns zuerst `rw`. Dies steht für \"rewrite\". Da $A$ und $B$ logisch äquivalent
sind, kann man beliebig das eine mit dem anderen vertauschen.
`rw [h]` ersetzt $A$ durch $B$.
Dabei gibt es noch einige Tricks:
- `rw [← h]` ersetzt umgekehrt $B$ durch $A$ (`\\l`, kleines L).
- `rw [h, g]` ist das gleiche wie `rw [h]` gefolgt von `rw [g]`.
Dieser hat schon von euch gehört und will sofort wissen, ob ihr ihm helfen könnt:
"
Statement
"Zeige dass `B ↔ C`."
(A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
Hint "**Du**: $B \\iff A \\iff D \\iff C$, die sind doch alle äquivalent…
**Robo**: Ja aber du musst ihm helfen umzuschreiben. Mit `rw [h₁]` kannst du `C` durch `D`
ersetzen."
rw [h₁]
Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
**Robo**: Dann schreibst du ein `←` vor den Namen, also `rw [← hₓ]`."
Branch
rw [← h₃]
Hint "**Du**: Ehm, das ist verkehrt.
**Robo**: Andersrum wär's besser gewesen, aber wenn du jetzt einfach weitermachst bis du
sowas wie `A ↔ A` kriegst, kann `rfl` das beweisen.
**Robo: Da fällt mir ein, `rw` versucht automatisch `rfl` am Ende. Das heisst, du musst
das nicht einmal mehr schreiben."
rw [h₂]
rw [←h₂]
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C =>
"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
Probiers doch mit `rw [h₁]`."
Conclusion "Ihr geht weiter und der Operationsleiter zeigt euch die Küche."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : A ↔ C =>
"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
Probiers doch mit `rw [h₁]`."
Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D =>
"Man kann auch rückwärts umschreiben:
`rw [←h₂]` ersetzt man im Goal `B` durch `a` (`\\l`, also ein kleines L)"
HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B =>
"Schau mal durch die Annahmen durch."
-- These should not be necessary if they don't use `rw [] at`.
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ C) : B ↔ C =>
"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
dass es mit einer Annahme übereinstimmt?"
HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : B ↔ D) : B ↔ C =>
"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
Hint (A : Prop) (B : Prop) (h : B ↔ A) : A ↔ B =>
"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `A ↔ A` umschreibst, kann man es mit
`rfl` beweisen (rsp. das passiert automatisch.)"
Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : D ↔ A) : B ↔ C =>
"Das ist nicht der optimale Weg..."
Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : A ↔ D) : B ↔ C =>
"Das ist nicht der optimale Weg..."
NewTactics rw assumption
NewTactic rw assumption
DisabledTactic tauto
-- NewLemma Iff.symm
server/testgame/TestGame/Levels/Implication/L08_Iff.lean
+22 -22
View File
@@ -10,35 +10,35 @@ Title "Genau dann wenn"
Introduction
"
Nun schauen wir uns Option 1) an, die du schon von UND kennst:
Der Koch kommt erfreut hinter einem grossen Topf hervor.
1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
direkt auswählen.
`h.mp` und `h.mpr` (oder `h.1` und `h.2`) sind die einzelnen Implikationen, und du kannst
mit denen ensprechend arbeiten. Insbesondere kannst du mit `apply h.mp` die Implikation
$A \\Rightarrow B$ anwenden, wenn das Goal $B$ ist.
*(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.)*
**Koch**: Sagt mal, gestern hat mir jemand was erzählt und es will einfach nicht aus
meinem Kopf…
"
Statement
"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
(A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
Hint "**Du**: Naja ich kann wohl immerhin mal mit `intro` anfangen und annehmen,
dass `{A}` wahr sei…
**Robo**: und dann schauen wir weiter!"
intro hA
Hint "**Robo**: Also eine Implikation wendet man mit apply an…
**Du**: Weiss ich ja!"
apply g
Hint "**Robo**: …und du kannst die Implikation `{A} → {B}` genau gleich mit
`apply {h}.mp` anwenden.
**Du**: Aber ich könnte hier auch `rw [← h]` sagen, oder?
**Robo**: Klar, aber offenbar versteht der Koch das `rw` nicht.
"
apply h.mp
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C =>
"Fange wie immer mit `intro` an."
Conclusion "**Koch**: Danke vielmals! Jetzt muss ich aber schauen dass die Suppe nicht verkocht!
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C =>
"Wie im Implikationen-Level kannst du nun `apply` verwenden."
Und er eilt davon."
Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
Conclusion "Im nächsten Level findest du die zweite Option."
NewTactics apply assumption
NewTactic apply assumption
DisabledTactic tauto rw
server/testgame/TestGame/Levels/Implication/L09_Iff.lean
+21 -19
View File
@@ -10,33 +10,35 @@ Title "Genau dann wenn"
Introduction
"
Und noch die letzte Option:
Noch während der Koch wieder zu seiner Suppe geht, kommt sein erster Gehilfe hervor.
2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
Als letzte Option kannst du `rcases h with ⟨h₁, h₂⟩` auch auf eine Annahme `(h : A ↔ B)`
anwenden, genau wie du dies bei einer Annahme `(h' : A ∧ B)` gemacht hast.
**Gehilfe**: Ich hab gestern noch was anderes gehört, könnt ihr mir da auch helfen?
Aber ich versteh nicht ganz was ihr meinem Chef erklärt habt.
"
Statement
"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
(A B : Prop) : (A ↔ B) → (A → B) := by
Statement (A B : Prop) : (A ↔ B) → (A → B) := by
Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
Hint (hidden := true) "**Robo**: Genau, das war `intro`."
intro h
rcases h
Hint "**Du**: Also ich kenn `rw [h]` und `apply h.mp`, aber das will er wohl nicht hören.
**Robo**: Was du machen könntest ist mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
Teile aufteilen."
Branch
intro a
Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benützen, aber der
Gehilfe will, dass du zwingend eine dritte Variante benützt. Geh doch einen
Schritt zurück so dass das Goal `A → B` ist."
rcases h with ⟨mp, mpr⟩
Hint (hidden := true) "**Du**: Ah und jetzt ist das Resultat in den Annahmen."
assumption
HiddenHint (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A → B =>
"Mit `rcases h with ⟨h₁, h₂⟩` kannst du jetzt die Annahme `(h : A ↔ B)` zerlegen."
Conclusion
"
**Gehilfe**: Ah danke! Und jetzt versteh ich auch die Zusammenhänge!
"
NewTactics intro apply rcases assumption
OnlyTactic intro rcases assumption
DisabledTactic rw apply tauto
-- -- TODO: The new `cases` works differntly. There is also `cases'`
-- example (A B : Prop) : (A ↔ B) → (A → B) := by
server/testgame/TestGame/Levels/Implication/L10_Apply.lean
+25 -31
View File
@@ -11,45 +11,39 @@ Title "Lemmas"
Introduction
"
Bewiesene Resultate möchte man in späteren Aufgaben als Sätze wieder verwenden.
Ihr setzt euch hin und der Gehilfe bringt euch allen Suppe. Neben euch sitzt eine Mechanikerin
über ihre Suppe geneigt.
In Lean sind das Lemmas und Theoreme (wobei es keinen Unterschied zwischen `lemma` und `theorem`
gibt).
Links in der Bibliothek findest du bekannte Lemmas. Wenn das Goal mit der Aussage des Lemmas
übereinstimmt, kannst du es mit `apply [Lemma-Name]` anwenden, wie du das mit Implikationen auch
machst.
Zum Beispiel gibt es ein Lemma, das sagt, dass wenn
$A \\Rightarrow B$ dann $(\\neg A \\lor B)$:
```
lemma not_or_of_imp : (A B : Prop) (h : A → B) :
¬A ∨ B := by
...
```
Wenn also dein Goal `¬A ∨ B` ist, kannst du mit `apply not_or_of_imp` dieses
Lemma anwenden. Danach musst du noch alle Annahmen zeigen.
**Mechanikerin**: Sagt mal, ich hab unten über folgendes tiefgründiges Problem nachgedacht:
"
Statement
"Benutze `not_or_of_imp` um zu zeigen, dass $\\neg A \\lor A$ wahr ist."
(A : Prop) : ¬A ∨ A := by
Statement (A : Prop) : ¬A ∨ A := by
Hint "**Du**: Das scheint ziemlich offensichtlich.
**Robo**: Ich glaube, sie will eine detailierte Antwort. Ich kenne ein Lemma
`not_or_of_imp`, was sagt `(A → B) → ¬ A ∨ B`. Da das Resultat des Lemmas mit
deinem Goal übreinstimmt, kannst du es mit `apply not_or_of_imp` anwenden."
Branch
right
Hint "**Du**: Und jetzt?
**Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
ist."
Branch
left
Hint "**Du**: Und jetzt?
**Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
ist."
apply not_or_of_imp
Hint (hidden := true) "**Robo**: Ich würd wieder mit `intro` weitermachen."
intro
assumption
HiddenHint (A : Prop) : ¬A ∨ A =>
"Das Lemma wendest du mit `apply not_or_of_imp` an."
HiddenHint (A : Prop) : A → A =>
"Wie immer, `intro` ist dein Freund."
Conclusion
"
**Mechanikerin**: Danke vielmals, jetzt bin ich schon viel ruhiger.
"
NewTactics apply left right assumption
NewLemmas not_or_of_imp
NewLemma not_or_of_imp
DisabledTactic tauto
server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
+38
View File
@@ -0,0 +1,38 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Cases
import Mathlib
Game "TestGame"
World "Implication"
Level 11
Title "by_cases"
Introduction
"
**Du**: Sagt mal, hätte ich da nicht auch einfach zwei Fälle anschauen können:
Wenn `A` wahr ist, beweis ich die rechte Seite, sonst die Linke.
**Robo**: Tatsächlich, `by_cases h : A` würde genau das machen!
"
Statement (A : Prop) : ¬A ∨ A := by
Hint (hidden := true) "**Du**: Wie?
**Robo**: Also `by_cases h : A` erstellt zwei Goals. Im ersten hast Du `(h : A)` zur
Verfügung, im zweiten `(h : ¬ A)`."
by_cases h : A
Hint "**Du**: "
right
assumption
left
assumption
Conclusion
"
**Du**: Das kann noch ganz nützlich sein.
"
NewTactic by_cases
DisabledTactic tauto
server/testgame/TestGame/Levels/Implication/L11_Rw.lean
-39
View File
@@ -1,39 +0,0 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Cases
import Mathlib.Logic.Basic
Game "TestGame"
World "Implication"
Level 11
Title "Lemmas"
Introduction
"
Wenn die Aussage eines Lemmas eine Äquivalenz ist, kann man dieses auch mit `rw` brauchen,
wie du es von Äquivalenzen kennst.
Ein wichtiges Lemma ist dass $\\neg(\\neg A))$ und $A$ äquivalent sind:
```
lemma not_not (A : Prop) : ¬¬A ↔ A := by
...
```
Mit `rw [not_not]` sucht Lean also im Goal ein Term `¬¬(·)` und entfernt dort das `¬¬`.
"
Statement
"Zeige, dass $A ∨ (¬¬B) ∧ C$ und $A ∨ B ∧ C$ äquivalent sind."
(A B C : Prop) : A ∨ (¬¬B) ∧ C ↔ A ∨ B ∧ C := by
rw [not_not]
Conclusion
"
`rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
"
NewTactics rw
NewLemmas not_not not_or_of_imp
server/testgame/TestGame/Levels/Implication/L12_Rw.lean
+50
View File
@@ -0,0 +1,50 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Cases
import Mathlib.Logic.Basic
Game "TestGame"
World "Implication"
Level 12
Title "Lemmas"
Introduction
"
Der Arbeitskollegin der Mechanikerin, der die ganze Zeit gespannt zugehört hat, dreht sich zu
euch.
Er ist offensichtlich interessiert and existierenden Resultaten zu sein, aber offenbar
kann er nicht viel mit `apply` anfangen.
Er hat aber folgendes Resultat bereit:
```
lemma not_not (A : Prop) : ¬¬A ↔ A
```
und stellt euch folgende Frage:
"
Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
Hint "**Robo**: Ein Lemma, das wie `not_not` ein `↔` oder `=` im Statement hat, kann
auch mit `rw [not_not]` verwendet werden."
rw [not_not]
Hint "**Du**: Häh, wieso hat das jetzt 2 von 3 der `¬¬` umgeschrieben?
**Robo**: `rw` schreibt nur das erste um, das es findet, also `¬¬C`. Aber weil dieses
mehrmals vorkommt, werden die alle ersetzt…
**Du**: Ah, und `¬¬B` ist was anderes, also brauch ich das Lemma nochmals."
rw [not_not]
Conclusion
"
**Du**: Ah und wir sind fertig…?
**Robo**: Ja, `rw` versucht immer anschliessend `rfl` aufzurufen, und das hat hier
funktioniert.
"
DisabledTactic tauto apply
NewLemma not_not
server/testgame/TestGame/Levels/Implication/L12_Summary.lean
-81
View File
@@ -1,81 +0,0 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight
import Mathlib
set_option tactic.hygienic false
Game "TestGame"
World "Implication"
Level 12
Title "Zusammenfassung"
Introduction
"
Damit bist du am Ende der zweiten Lektion angekommen.
Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
Abschlussaufgabe.
## Notationen / Begriffe
| | Beschreibung |
|:--------------|:---------------------------------------------------------|
| → | Eine Implikation. |
| ↔ | Genau-dann-wenn / Äquivalenz. |
| `lemma` | Ein Resultat mit einem Namen. |
| `theorem` | Das gleiche wie ein Lemma. |
| `example` | Wie ein Lemma aber ohne Namen (nicht weiter verwendbar.) |
## Taktiken
| | Taktik | Beispiel |
|:----|:--------------------------|:-------------------------------------------------------|
| 8 | `intro` | Für eine Implikation im Goal. |
| 9 | `revert` | Umkehrung von `intro`. |
| 10 | `apply` | Wendet eine Implikation auf das Goal an. |
| 10ᵇ | `apply` | Wendet ein Lemma an. |
| 11 | `rw` | Umschreiben zweier äquivalenter Aussagen. |
| 11ᵇ | `rw` | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
Als Abschlussübung kannst du folgende Äquivalenz zeigen:
"
Statement imp_iff_not_or
"$A \\Rightarrow B$ ist äquivalent zu $\\neg A \\lor B$."
(A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
constructor
apply not_or_of_imp
intro h ha
rcases h with h | h
contradiction
assumption
HiddenHint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B =>
"Eine Äquivalenz im Goal geht man immer mit `constructor` an."
HiddenHint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B =>
"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
HiddenHint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B =>
"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
HiddenHint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) =>
"Eine Implikation geht man fast immer mit `intro h` an."
HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
"Nochmals `intro`."
HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
"Findest du einen Widerspruch?"
NewTactics rfl assumption trivial left right constructor rcases
NewLemmas not_not not_or_of_imp
server/testgame/TestGame/Levels/Implication/L13_Summary.lean
+77
View File
@@ -0,0 +1,77 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight
import Mathlib
set_option tactic.hygienic false
Game "TestGame"
World "Implication"
Level 13
Title "Zusammenfassung"
Introduction
"
**Operationsleiter**: Damit endet unsere Führung langsam. Bevor ihr weitergeht
habe ich noch ein Problem, an dem ich mir die Zähne ausbeisse. Wir haben die
Herleitung eines unserer Programme `imp_iff_not_or` verloren, und wissen nicht mehr
ob es einwandfrei funktioniert.
**Du**: Nah gut, mal sehen. Robo, was hab ich denn alles hier gelernt?
**Robo**: Hier ist die Übersicht:
## Notationen / Begriffe
| | Beschreibung |
|:--------------|:---------------------------------------------------------|
| → | Eine Implikation. |
| ↔ | Genau-dann-wenn / Äquivalenz. |
## Taktiken
| | Taktik | Beispiel |
|:----|:--------------------------|:-------------------------------------------------------|
| 8 | `intro` | Für eine Implikation im Goal. |
| 9 | `revert` | Umkehrung von `intro`. |
| 10 | `apply` | Wendet eine Implikation auf das Goal an. |
| 10ᵇ | `apply` | Wendet ein Lemma an. |
| 11 | `by_cases` | Fallunterscheidung `P` und `¬P` |
| 12 | `rw` | Umschreiben zweier äquivalenter Aussagen. |
| 12ᵇ | `rw` | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
"
Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
constructor
Hint "**Du**: Das sieht kompliziert aus…
**Robo** *(flüsternd)*: Ja, aber die Richtung kennst du ja schon also Lemma,
wend doch einfach das an."
apply not_or_of_imp
Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma?
**Robo**: Leider nicht. Da musst du manuell ran."
Hint (hidden := true) "**Robo**: Na Implikationen fangst du immer mit `intro` an."
intro h
intro ha
Hint (hidden := true) "**Robo**: Ich wür mal die Annahme `h` mit `rcases` aufteilen."
rcases h with h | h
contradiction
assumption
DisabledTactic tauto
Conclusion "**Operationsleiter**: Damit gehen unsere Wege auseinander. Da fällt mir ein, seit
ihr auf dem Weg zu unserem Schwestermond?
**Du**: Könnten wir sein…
**Operationsleiter**: Ich hab hier einen Brief für *Evenine*, könntet ihr diesen mit euch führen?
**Du**: Klar! Robo, halt den mal.
Robo nimmt den Brief und lässt ihn irgendwo in seinem Innern verschwinden. Dabei bemerkt er
den besorgten Blick des Operationsleiters.
**Robo**: Keine Angst, ich verdaue nichts!"
server/testgame/TestGame/Levels/Induction/L01_Induction.lean
+1 -1
View File
@@ -24,7 +24,7 @@ Statement
rw [Nat.pow_succ, Nat.mul_succ, add_assoc, h, mul_comm, ←mul_add]
simp
--NewLemmas Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
--NewLemma Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
-- example (n : ℕ) : Even (n^2 + n) := by
-- induction n
server/testgame/TestGame/Levels/Inequality/L02_Pos.lean
+2 -2
View File
@@ -34,8 +34,8 @@ Statement Nat.pos_iff_ne_zero
intro
apply Nat.succ_pos
NewTactics simp
NewLemmas Nat.succ_pos
NewTactic simp
NewLemma Nat.succ_pos
Hint : 0 < Nat.zero ↔ Nat.zero ≠ 0 =>
"Den Induktionsanfang kannst du oft mit `simp` lösen."
server/testgame/TestGame/Levels/Inequality/L03_Linarith.lean
+2 -2
View File
@@ -18,6 +18,6 @@ Statement
(n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
linarith
NewTactics linarith
NewTactic linarith
NewLemmas Nat.pos_iff_ne_zero
NewLemma Nat.pos_iff_ne_zero
server/testgame/TestGame/Levels/Inequality/T_Induction.lean
+1 -1
View File
@@ -38,4 +38,4 @@ Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
In diesem Beispiel kannst du `apply` benützen."
NewTactics induction
NewTactic induction
server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean
+2 -2
View File
@@ -43,9 +43,9 @@ Statement
rw [Fin.sum_univ_castSucc (n := m + 1)]
rfl
OnlyTactics rw rfl
OnlyTactic rw rfl
NewLemmas Fin.sum_univ_castSucc
NewLemma Fin.sum_univ_castSucc
HiddenHint (m : ℕ) :
∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
server/testgame/TestGame/Levels/LeanStuff/L04_InstanceArguments.lean
+2 -2
View File
@@ -49,9 +49,9 @@ Statement
rw [Fin.sum_univ_castSucc (n := m + 1)]
rfl
OnlyTactics rw rfl
OnlyTactic rw rfl
NewLemmas Fin.sum_univ_castSucc
NewLemma Fin.sum_univ_castSucc
Hint (m : ℕ) :
∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
+1 -1
View File
@@ -67,4 +67,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
NewTactics left right assumption constructor rcases
NewTactic left right assumption constructor rcases
server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
+1 -1
View File
@@ -20,4 +20,4 @@ Conclusion
"
"
NewTactics ring
NewTactic ring
server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
+1 -1
View File
@@ -20,4 +20,4 @@ Conclusion
"
"
NewTactics ring
NewTactic ring
server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
+1 -1
View File
@@ -58,4 +58,4 @@ Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even
"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
`(x : ℕ) → `"
NewTactics ring intro unfold
NewTactic ring intro unfold
server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
+1 -1
View File
@@ -22,4 +22,4 @@ Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
Conclusion ""
NewTactics use simp
NewTactic use simp
server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
+27 -25
View File
@@ -62,28 +62,30 @@ Im nachfolgenden beweisen wir die Eigenschaften einzeln.
Statement
"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
: Module ℚ ℝ :=
{ smul := fun a r ↦ ↑a * r,
smul_zero := by
intro a
rw [smul_zero]
zero_smul := by
intro a
change (0 : ℚ) * a = 0
simp
one_smul := by
intro b
change (1 : ℚ) * b = b
rw [Rat.cast_one, one_mul]
smul_add := by
intro a x y
change a * (x + y) = a * x + a * y
rw [mul_add]
add_smul := by
intro r s x
change (r + s : ℚ) * x = r * x + s * x
rw [Rat.cast_add, add_mul]
mul_smul := by
intro x y b
change (x * y : ℚ) * b = x * (y * b)
rw [Rat.cast_mul, mul_assoc]}
: Module ℚ ℝ := by
refine {
smul := fun a r => ↑a * r
smul_zero := ?smul_zero
zero_smul := ?zero_smul
one_smul := ?one_smul
smul_add := ?smul_add
add_smul := ?add_smul
mul_smul := ?mul_smul }
· intro b
change (1 : ℚ) * b = b
rw [Rat.cast_one, one_mul]
· intro x y b
change (x * y : ℚ) * b = x * (y * b)
rw [Rat.cast_mul, mul_assoc]
· intro a
rw [smul_zero]
· intro a x y
change a * (x + y) = a * x + a * y
rw [mul_add]
· intro r s x
change (r + s : ℚ) * x = r * x + s * x
rw [Rat.cast_add, add_mul]
· intro a
change (0 : ℚ) * a = 0
simp
server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
+1 -1
View File
@@ -72,4 +72,4 @@ Statement
simp <;>
ring
NewTactics fin_cases funext
NewTactic fin_cases funext
server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean
+1 -1
View File
@@ -40,4 +40,4 @@ Statement
-- fin_cases i;
-- simp,
--NewLemmas top_le_span_range_iff_forall_exists_fun le_top
--NewLemma top_le_span_range_iff_forall_exists_fun le_top
server/testgame/TestGame/Levels/Predicate.lean
+17 -3
View File
@@ -4,10 +4,24 @@ import TestGame.Levels.Predicate.L03_Rewrite
import TestGame.Levels.Predicate.L04_Ring
import TestGame.Levels.Predicate.L05_Rfl
import TestGame.Levels.Predicate.L06_Exists
import TestGame.Levels.Predicate.L07_Forall
import TestGame.Levels.Predicate.L08_PushNeg
import TestGame.Levels.Predicate.L09_Summary
import TestGame.Levels.Predicate.L07_Exists
import TestGame.Levels.Predicate.L08_Forall
import TestGame.Levels.Predicate.L09_PushNeg
Game "TestGame"
World "Predicate"
Title "Prädikate"
Introduction "Eure Reise geht weiter zum zweiten Mond. Dieser ist etwas grösser und
komplett mit buschartigen Pflanzen überwachsen. Der Landeanflug sit etwas kniffliger,
aber offenbar kann Robo nicht nur Lean übersetzen, sondern auch mit maschineller Genauigkeit
navigieren.
Ihr werdet sofort empfangen und man führt euch zur lokalen Machthaberin.
Ihr kommt an verschiedensten riesigen Büschen vorbei, die offensichtlich innen Ausgehöhlt sind
und so als Wände für Behausungen der Wesen hier dienen.
Man führt euch in einen der Büsche. Nun entdecksts du dass das Blätterdach künstlich verstärkt ist,
offensichtlich um Regen abzuweisen.
Vor euch steht eine Frau, die euch als Machthabering *Evenine* vorgestellt wird."
server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
+15 -23
View File
@@ -11,34 +11,26 @@ Title "Natürliche Zahlen"
Introduction
"
Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon kurz begegnet.
Gleichungen, die nur die Operationen `+, -, *, ^` (Addition, Subtraktion, Multiplikation, Potenz)
und Variablen enthalten, kann Lean mit der Taktik `ring` beweisen.
Diese Taktik funktioniert nicht nur über den natürlichen Zahlen,
sondern auch in (kommutativen) Gruppen, Ringen, und Körpern. Sie heisst `ring`, weil sie für Ringe
entwickelt wurde.
(Note: Division `/` ignorieren wir hier erst einmal, weil diese auf `ℕ`
nicht kanonisch definiert ist.)
**Evenine**: Willkommen Reisende! Wir leben hier in Einklang mit der Natur und allem natürlichen,
so sagt mir, könnt ihr mit natürlichen Zahlen umgehen?
"
Statement
"Zeige $(x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2$."
(x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
ring
Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
Hint "**Du**: Das hab ich in der Schule gelernt, man rechnet das einfach aus,
indem man die Terme umsortiert.
HiddenHint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 =>
"`ring` übernimmt den ganzen Spaß."
**Robo**: Behaupte doch mit `ring`, dass das so ist.
**Du**: Aber `ℕ` ist doch gar kein Ring?
**Robo**: `ring` funktioniert schon für Halbringe, aber sie heisst ring, weil sie auf
(kommutativen) Ringen am besten funktioniert.
"
ring
Conclusion
"
Die Taktik heisst übrigens `ring` weil sie dafür entwickelt wurde, Gleichungen in einem abstrakten
Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
(erst `ℤ` ist ein Ring).
*Evenine: Ja das stimmt schon. Und das genügt uns auf diesem Planet auch als Antwort.*
"
NewTactics ring
#eval 4 / 6
NewTactic ring
server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
+18 -49
View File
@@ -9,62 +9,31 @@ Title "Rewrite"
Introduction
"
Wir haben gesehen, dass man mit `rw` Äquivalenzen wie `A ↔ B` brauchen kann, um im Goal
$A$ durch $B$ zu ersetzen.
Robo spuckt den Brief aus, den er dabei hatte, und gibt ihn *Evenine*.
Genau gleich kann man auch Gleichungen `a = b` mit `rw` verwenden.
**Evenine**: Das verstehe ich nicht, wisst ihr was damit gemeint ist?
Und sie händigt Dir den Brief:
"
Statement umschreiben
"Angenommen man hat die Gleichheiten
Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
Hint "**Du**: Schau mal, das ist ja fast genau, was wir auf *Implis* gemacht haben,
nur jetzt mit Gleichheiten von Zahlen anstatt Genau-Dann-Wenn-Aussagen!
$$
\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
$$
**Robo**: `=` und `↔` kannst du praktisch gleich behandeln wenns um `rw` geht."
Hint (hidden := true) "**Du**: Also auch `rw [hₓ]` und `rw [← hₓ]`?
Zeige dass $b = c$."
(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
**Robo**: Probiers doch einfach."
rw [h₁]
Hint (hidden := true) "**Du**: Wie war das nochmals mit rückwärts umschreiben?
**Robo**: `←` ist `\\l`. Und dann `rw [← hₓ]`"
rw [←h₂]
assumption
HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
"Im Goal kommt `c` vor und `h₁` sagt `c = d`.
Probiers doch mit `rw [h₁]`."
Conclusion
"
**Evenine**: Danke viemals, das hilft uns vermutlich, jetzt Frage ich mich aber…
"
HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = c =>
"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
Probiers doch mit `rw [h₁]`."
HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
" Man kann auch rückwärts umschreiben: `h₂` sagt `a = b` mit
`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
HiddenHint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
"Schau mal durch die Annahmen durch."
-- These should not be necessary if they don't use `rw [] at`.
HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = c) : b = c =>
"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
dass es mit einer Annahme übereinstimmt?"
HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : b = d) : b = c =>
"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
Hint (a : ℕ) (b : ℕ) (h : b = a) : a = b =>
"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `a = a` umschreibst, kann man es mit
`rfl` beweisen (rsp. das passiert automatisch.)"
Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c =>
"das ist nicht der optimale Weg..."
Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c =>
"das ist nicht der optimale Weg..."
Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
NewTactics assumption rw
NewTactic assumption rw
server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
+17 -21
View File
@@ -9,32 +9,28 @@ Title "Rewrite"
Introduction
"
Als Übung erinnern wir daran, dass man mit `rw [h] at g` auch in anderen Annahmen umschreiben
kann:
Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
`g` das `X` durch `Y`.
**Evenine**: Mit diesem neuen Wissen, könnt ihr mir bei folgendem helfen:
"
Statement umschreiben
"Angenommen man hat die Gleichheiten
Statement
"
$$
\\begin{aligned} a &= b \\\\ a + a ^ 2 &= b + 1 \\end{aligned}
\\begin{aligned}
a &= b \\\\
a + a ^ 2 &= b + 1 \\\\
\\vdash b + b ^ 2 = b + 1
\\end{aligned}
$$
Zeige dass $b + b ^ 2 = b + 1$."
"
(a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
Hint "**Du**: Ah da ersetzt man ja einfach `{a}` durch `{b}` in der anderen Annahme!
**Robo**: Genau! Das machst du mit `rw [{h}] at {g}`."
rw [h] at g
Hint (hidden := true) "**Robo**: Schau mal durch die Annahmen."
assumption
Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 =>
"`rw [ ... ] at g` schreibt die Annahme `g` um."
Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 =>
"Sackgasse. probiers doch mit `rw [h] at g` stattdessen."
Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
dem Goal umschreiben."
NewTactics assumption rw
Conclusion "
**Robo**: Noch ein Trick: Mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
dem Goal umschreiben.
"
server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
+16 -14
View File
@@ -9,25 +9,27 @@ Title "Natürliche Zahlen"
Introduction
"
Oft braucht man eine Kombination von `rw` und `ring` um Gleichungen zu lösen.
*Evenines* Berater meldet sich.
Zuerst setzt man mit `rw` die vorhandenen Annahmen ein, und sobald die beiden Seiten
einer Gleichung im Goal rechnerisch gleich sind, kan `ring` dies beweisen.
**Berater**: Das stimmt wohl, aber das Problem, das uns eigentlich beschäftigt hat, eure
Natürlichkeit, war folgendes:
"
Statement
"Angenommen, man hat die Gleichung $x = 2 * y + 1$, zeige
$x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y$. "
(x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
rw [h]
(x y z : ℕ) (h : x = 2 * y + 1) (g : z = 3 * y + 1): x ^ 2 = 4 * y ^ 2 + z + y := by
Hint "**Du**: Ich versteh das Pattern. Wenn ich zuerst alles so umschreibe, dass
das Goal nur noch rechnen und umsortieren ist, dann kann `ring` den Rest machen!
**Robo**: Noch ein Trick: Entweder kannst du zwei Befehle `rw [h₁]` und `rw [h₂]` schreiben,
oder du kannst das gleich in einem machen : rw [h₁, h₂]."
rw [h, g]
ring
Hint (x : ℕ) (y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
"Die Annahme `h` kannst du mit `rw [h]` benützen."
Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
"Jetzt kann `ring` übernehmen."
Conclusion
"
*Evenine* bedankt sich nochmals für die Botschaft und ihr werdet zu einem kleineren Busch geführt,
der ein gemütlich warmes Innenleben an den Tag legt.
"
Conclusion ""
NewTactics ring rw
NewTactic ring rw
server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
+18 -13
View File
@@ -8,24 +8,29 @@ Title "Definitionally equal"
Introduction
"
Als kleine Nebenbemerkung:
Müde ruht ihr euch in eurer Bleibe aus. Du schaust doch eine Lücke in den Blättern vielen
kleinen Vögeln bei der Nahrungssuche zu.
Auf Grund der Implementation in Lean brauchst du die Taktik `ring` gar nicht, wenn
du Gleichungen über `ℕ` hast, die keine Variablen enthalten:
So ist zum Beispiel `2` als `1 + 1` definiert, deshalb kannst du $1 + 1 = 2$ einfach mit
`rfl` beweisen.
**Du**: Sag mal Robo, ich hab vorhin ein Kind überhört, dass seinem Spielgefährten erklärt hat,
folgendes sei mit `rfl` zu beweisen:
"
Statement
"Zeige dass $1 + 1$ zwei ist." :
1 + 1 = 2 := by
Statement : 1 + 1 = 2 := by
Hint "**Du**: Wieso nicht `ring`?
**Robo**: Klar, `ring` geht auch und ist intuitiver.
Für `rfl` kommt es darauf an, wie die Sachen genau definiert sind: `1 + 1` ist als
`(0.succ).succ` definiert und `2` halt ebenfalls.
"
rfl
OnlyTactic rfl
Conclusion
"
**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl`
aufzurufen, deshalb brauchst du das nur noch selten.
"
**Du**: Dann war das mehr Glück?
NewTactics rfl
**Robo**: Das ist eine Art die Welt zu sehen…
Damit fällst du in einen ruhigen Schlaf.
"
server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
+45 -43
View File
@@ -6,6 +6,8 @@ import Mathlib.Tactic.Ring
import Mathlib.Algebra.Parity
set_option tactic.hygienic false
Game "TestGame"
World "Predicate"
Level 6
@@ -14,58 +16,58 @@ Title "Gerade/Ungerade"
Introduction
"
Gerade/ungerade werden in Lean wie folgt definiert:
Am nächsten Tag erklärt euch *Evenine*, dass es auf dem Mond zwei Gruppierungen gibt,
ihre und die ihres Halbbruders *Oddeus*. Die Mottos sind
```
def Even (n : ℕ) : Prop := ∃ r, n = r + r
def Odd (n : ℕ) : Prop := ∃ r, n = r + r + 1
```
Also dadurch, dass ein `(r : ℕ)` existiert sodass `n = r + r (+1)`.
Beachte das Komma `,` welches die Variablen des `∃` (`\\exists`) von der Aussage trennen.
Hierzu gibt es 3 wichtige Taktiken:
und
1) Definitionen wie `Even` kann man mit `unfold Even at *` im Infoview einsetzen.
Das ändert Lean-intern nichts und ist nur für den Benutzer. Man kann auch einen
Term `(h : Even x)` einfach so behandeln als wäre es ein Term `(h : ∃ r, x = 2 * r)`.
2) Bei einer Annahme `(h : ∃ r, ...)` kann man mit `rcases h with ⟨y, hy⟩` ein solches `y`
Auswählen, dass die Annahme `h` erfüllt.
3) Bei einem `∃` im Goal muss man ein Element `y` angeben, welches diese Aussage erfüllen
soll. Das macht man mit `use y`
```
def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
```
**Evenine**: Hier, ich zeige euch mal etwas was man bei uns machen kann:
"
Statement even_square
"Wenn $n$ gerade ist, dann ist $n^2$ gerade."
(n : ℕ) (h : Even n) : Even (n ^ 2) := by
Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
Branch
unfold Even
Hint "Rob**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst was los ist."
Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
dass ein `r` existiert so dass `r + r = n`. Am besten
öffnest du diese Definition mit `unfold Even at *` einmal, dann siehst du besser, was los ist. "
unfold Even at *
rcases h with ⟨x, hx⟩
use 2 * x ^ 2
rw [hx]
Hint "**Du**: Also von `{h}` weiss ich jetzt dass ein `r` existiert, so dass `r + r = n`…
**Robo**: Mit `rcases h with ⟨r, hr⟩` kannst du dieses `r` tatsächlich einführen."
rcases h with ⟨r, hr⟩
Hint "**Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = n^2`?
**Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
dir leider nicht sagen, welche Zahl passt.
"
Branch
rw [hr]
Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
use 2 * r ^ 2
ring
use 2 * r ^ 2
Hint "**Du**: Ah und jetzt `ring`!
**Robo**: Aber zuerst must du noch mit
`rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiss."
rw [hr]
ring
Hint (n : ℕ) (h : Even n) : Even (n ^ 2) =>
"Wenn du die Definition von `Even` nicht kennst, kannst du diese mit `unfold Even` oder
`unfold Even at *` ersetzen.
Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
genau gleich, wenn du das `unfold` rauslöscht."
-- TODO: [Comment] For me the expected behaviour of `(strict := true)` would
-- be that it distinguishes between the defEq states while `(strict := false)`
-- would show the hint regardless of a `unfold Even`.
Hint (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
ein `x` erhalten, dass die Aussage erfüllt."
NewTactic unfold use
NewDefinition Even Odd
Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
die Aussage erfüllen soll."
Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r =>
"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
die Aussage erfüllen soll."
Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu
`x + x` umschreiben..."
Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
"Die Taktik `ring` löst solche Gleichungen."
NewTactics unfold rcases use rw ring
NewDefinitions Even Odd
Conclusion "**Evenine**: Seht ihr?"
server/testgame/TestGame/Levels/Predicate/L07_Exists.lean
+43
View File
@@ -0,0 +1,43 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.Use
import Mathlib.Tactic.Ring
import Mathlib.Algebra.Parity
set_option tactic.hygienic false
Game "TestGame"
World "Predicate"
Level 7
Title "Gerade/Ungerade"
Introduction
"
**Du**: Aber, das sagt doch gar nichts aus, genau das gleiche könnte ich für `Odd`
auch sagen. Hier seht!
"
Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by
unfold Odd at *
rcases h with ⟨r, hr⟩
Hint "**Robo**: Ich hab noch einen Trick auf Lager:
Wenn du jetzt herausfinden willst, welche Zahl du einsetzen musst, könntest
du schon jetzt mit `rw [{hr}]` weitermachen…"
rw [hr]
Hint "**Robo**: Wenn du jetzt `ring` benötigst, dann schreibt es einfach alles in
Normalform um, das hilft beim vergleichen."
ring
Hint "**Du**: Was bedeutet `ring_nf`?
**Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
schreiben, aber die funktionieren praktisch gleich."
use 2 * (r + r ^ 2)
ring
-- TODO: Allow `ring_nf` as part of `ring`.
Conclusion "**Evenine**: Tatsächlich. Vielleicht sind wir gar nich tso unterschiedlich. Könntet
ihr mal mit ihm reden gehen?"
server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
-53
View File
@@ -1,53 +0,0 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.Use
import Mathlib.Tactic.Ring
import Mathlib.Algebra.Parity
import Mathlib
Game "TestGame"
World "Predicate"
Level 7
Title "Für alle"
Introduction
"
Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
Also folgende Annahme und Lemma sind genau :
- `(le_square : ∀ (n : ℕ), n ≤ n^2)`
- `lemma le_square (n : ℕ) : n ≤ n^2`
Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
TODO: 1-2 Aufgaben mehr.
"
Statement
" Für alle natürlichen Zahlen $x$ gilt, falls $x$ gerade ist, dann ist $x + 1$
ungerade." : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
intro x h
unfold Even at h
unfold Odd
rcases h with ⟨y, hy⟩
use y
rw [hy]
ring
Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even (n + 1) =>
"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
`(x : ℕ) → `"
Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
praktisch gleich. Mehr dazu später."
NewTactics ring intro unfold
server/testgame/TestGame/Levels/Predicate/L08_Forall.lean
+53
View File
@@ -0,0 +1,53 @@
import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.Use
import Mathlib.Tactic.Ring
import Mathlib.Algebra.Parity
import Mathlib
Game "TestGame"
World "Predicate"
Level 8
Title "Für alle"
Introduction
"
Ihr macht euch also auf den Weg. Unterwegs trefft ihr einen Händler und ihr lässt euch von
ihm den Weg zeigen, sowie einige Tipps zu den beiden Geschwistern geben.
**Händler**: Also seht, die beiden sind gar nicht so verschieden. Ein altes Sprichwort sagt:
"
-- Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
-- Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
-- Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
-- auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
-- Also folgende Annahme und Lemma sind genau :
-- - `(le_square : ∀ (n : ℕ), n ≤ n^2)`
-- - `lemma le_square (n : ℕ) : n ≤ n^2`
-- Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
-- TODO: 1-2 Aufgaben mehr.
Statement : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
Hint "**Du**: Das `∀` heisst sicher \"für alle\".
**Robo**: Und man schreibt `\\forall`. Ein `∀ x, …` im Goal kannst du wie eine
Implikation mit `intro x` angehen."
intro x h
unfold Even at h
unfold Odd
rcases h with ⟨y, hy⟩
use y
rw [hy]
ring
Conclusion "**Händler**: Sichere Reise!"
server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
-67
View File
@@ -1,67 +0,0 @@
import TestGame.Metadata
import Mathlib.Tactic.PushNeg
import Mathlib
import Mathlib.Algebra.Parity
import TestGame.ToBePorted
Game "TestGame"
World "Predicate"
Level 8
Title "PushNeg"
Introduction
"
Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
mit `push_neg` das `¬` durch den Quantor hindurchschieben.
Das braucht intern die Lemmas
- `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
- `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
(welche man auch mit `rw` explizit benutzen könnte.)
"
Statement
"Es existiert keine natürliche Zahl $n$, sodass $n + k$ immer ungerade ist.":
¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
push_neg
intro n
use n
rw [not_odd]
unfold Even
use n
Hint : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) =>
"`push_neg` schiebt die Negierung an den Quantoren vorbei."
Hint (n : ℕ) : (∃ k, ¬Odd (n + k)) =>
"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutze `use`
mit der richtigen Zahl."
HiddenHint (n : ℕ) : ¬Odd (n + n) =>
"Du kennst ein Lemma um mit `¬odd` umzugehen."
-- HiddenHint (n : ℕ) (k : ℕ) : ¬odd (n + k) =>
-- "Du kennst ein Lemma um mit `¬odd` umzugehen."
HiddenHint (n : ℕ) : Even (n + n) =>
"`unfold even` hilft, anzuschauen, was hinter `even` steckt.
Danach musst du wieder mit `use r` ein `(r : ℕ)` angeben, dass du benützen möchtest."
-- HiddenHint (n : ℕ) (k : ℕ) : even (n + k) =>
-- "`unfold even` hilft hier weiter."
Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
Conclusion ""
NewTactics push_neg intro use rw unfold ring
NewDefinitions Even Odd
NewLemmas not_even not_odd not_exists not_forall
server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
+109
View File
@@ -0,0 +1,109 @@
import TestGame.Metadata
import Mathlib.Tactic.PushNeg
import Mathlib
import Mathlib.Algebra.Parity
import TestGame.ToBePorted
Game "TestGame"
World "Predicate"
Level 9
Title "PushNeg"
Introduction
"
Das Dorf von *Oddeus* scheint stärker befestigt zu sein, all jenes von *Evenine*. Ihr kommt
and eine Wand aus Dornenranken. Beim Eingang steht eine Wache, die auch zuruft:
"
-- Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
-- mit `push_neg` das `¬` durch den Quantor hindurchschieben.
-- Das braucht intern die Lemmas
-- - `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
-- - `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
-- (welche man auch mit `rw` explizit benutzen könnte.)
open Nat
Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
Hint "**Du**: Also ich kann mal das `¬` durch die Quantifier hindurchschieben.
**Robo**: `push_neg` macht genau das!
**Robo**: Intern braucht das zwei Lemmas
```
not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)
not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)
```
die du natürlich auch mit `rw` gebrauchen könntest."
Branch
unfold Odd
push_neg
Hint "**Robo**: Der Weg ist etwas schwieriger. Ich würde nochmals zurück und schauen,
dass du irgendwann `¬Odd` kriegst, was du dann mit `rw [←even_iff_not_odd]`
zu `Even` umwandeln.
kannst."
push_neg
intro n
Hint "**Robo**: Welche Zahl du jetzt mit `use` brauchst, danach wirst du vermutlich das
Lemma `←even_iff_not_odd` brauchen.
**Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` machen?
**Robo**: Ne, `rw` kann nicht innerhalb von Quantifiern umschreiben.
**Du**: Aber wie würde ich das machen?
**Robo**: Zeig ich dir später, die Wache wird schon ganz ungeduldig!
Im Moment würde ich zuerst mit `use` eine richtige Zahl angeben, und danach umschreiben."
Branch
use n + 2
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
Branch
use n + 4
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
use n
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
rw [←even_iff_not_odd]
unfold Even
use n
--ring
Conclusion "Damit werdet ihr eingelassen.
**Robo**: Entweder wir suchen direkt diesen *Oddeus*, oder wir schauen uns einmal um. Die Wahl
ist deine!
**Du**: Kannst du mir nochmals einen Überblick geben, was wir gelernt haben?
**Robo**:
| | Beschreibung |
|:--------------|:----------------------------|
| `ℕ` | Die natürlichen Zahlen. |
| `∃` | Existential-Quantifier |
| `∀` | Forall-Quantifier |
| `Even n` | `n` ist gerade |
| `Odd n` | `n` ist ungerade |
| | Taktik | Beispiel |
|:------|:--------------------------|:-------------------------------------------------------|
| *12ᶜ* | `rw` | Umschreiben mit Gleichungen. |
| 13 | `ring` | Löst Gleichungen mit `+, -, *, ^`. |
| 14 | `unfold` | Setzt visuell die Bedeutung einer Definition ein. |
| 15 | `use` | Um ein `∃` im Goal anzugehen. |
| *7ᶜ* | `rcases h with ⟨x, hx⟩` | Um ein `∃` in den Annahmen zu zerlegen. |
| *8ᵇ* | `intro` | Um ein `∀` im Goal anzugehen. |
| 16 | `push_neg` | Für `¬∃` und `¬∀` im Goal. |
"
NewTactic push_neg
NewLemma even_iff_not_odd odd_iff_not_even not_exists not_forall
server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
-55
View File
@@ -1,55 +0,0 @@
import TestGame.Metadata
import Mathlib.Tactic.PushNeg
import Mathlib
import TestGame.ToBePorted
Game "TestGame"
World "Predicate"
Level 9
Title "Zusammenfassung"
Introduction
"
Damit bist du am Ende der dritten Lektion angekommen.
Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
Abschlussaufgabe.
## Notationen / Begriffe
| | Beschreibung |
|:--------------|:----------------------------|
| `ℕ` | Die natürlichen Zahlen. |
| `∃` | Existential-Quantifier |
| `∀` | Forall-Quantifier |
| `Even n` | `n` ist gerade |
| `Odd n` | `n` ist ungerade |
## Taktiken
| | Taktik | Beispiel |
|:------|:--------------------------|:-------------------------------------------------------|
| *11ᶜ* | `rw` | Umschreiben mit Gleichungen. |
| 12 | `ring` | Löst Gleichungen mit `+, -, *, ^`. |
| 13 | `unfold` | Setzt visuell die Bedeutung einer Definition ein. |
| 14 | `use` | Um ein `∃` im Goal anzugehen. |
| *7ᶜ* | `rcases h with ⟨x, hx⟩` | Um ein `∃` in den Annahmen zu zerlegen. |
| *8ᵇ* | `intro` | Um ein `∀` im Goal anzugehen. |
| 15 | `push_neg` | Für `¬∃` und `¬∀` im Goal. |
Als Abschlussübung kannst du folgende Äquivalenz zeigen:
"
Statement
"TODO":
True := by
trivial
Conclusion ""
NewTactics push_neg intro use rw unfold ring
NewDefinitions Even Odd
NewLemmas not_even not_odd not_exists not_forall
server/testgame/TestGame/Levels/Prime/L04_Prime.lean
+1 -1
View File
@@ -43,4 +43,4 @@ Statement
rcases h with ⟨_, h₂⟩
assumption
NewLemmas Nat.prime_def_lt''
NewLemma Nat.prime_def_lt''
server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+14 -18
View File
@@ -21,25 +21,21 @@ Du siehst Robo hilflos an.
Statement ""
(A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
Hint "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
`{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
**Du** Ernsthaft?
**Robo** Ja. Schreib einfach `tauto`.
**Robo** Mach schon …"
tauto
Hint (A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
"**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
`{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
**Du** Ernsthaft?
**Robo** Ja. Schreib einfach `tauto`.
**Robo** Mach schon …
"
Conclusion
"
**Logisinde** (etwas konsterniert) Ja, das ist streng genommen richtig.
@@ -47,4 +43,4 @@ Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt!
Meine Untertanen verstehen `tauto` nicht. Da müsst Ihr Euch schon etwas mehr anstrengen.
"
NewTactics tauto
NewTactic tauto
server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+4 -7
View File
@@ -19,17 +19,14 @@ Er schreibt es Dir wieder auf.
Statement "" :
42 = 42 := by
Hint " **Robo** Ist doch klar. Du musst ihn einfach daran erinnern,
dass Gleichheit *reflexiv* ist. Probier mal `rfl`."
rfl
Hint : 42 = 42 => "
**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist.
Probier mal `rfl`.
"
Conclusion
"
**Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl …
"
NewTactics rfl
DisabledTactics tauto
NewTactic rfl
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+5 -7
View File
@@ -13,9 +13,7 @@ Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste
Statement ""
(n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
assumption
Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
Hint "
**Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl.
**Du** Warum schreibt er dann nicht `{n} ∈ ℕ`??
@@ -32,8 +30,8 @@ für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
**Du** ???
**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`.
"
**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`."
assumption
Conclusion
"
@@ -41,5 +39,5 @@ Conclusion
zerbrochen habe!
"
NewTactics assumption
DisabledTactics tauto
NewTactic assumption
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+6 -8
View File
@@ -14,9 +14,7 @@ Ein dritter Untertan kommt mit folgendem Problem.
Statement ""
(A : Prop) (hA : A) : A := by
assumption
Hint (A : Prop) (hA : A) : A => "
Hint "
**Robo** Hier bedeutet `{A} : Prop` wieder, dass `{A}` irgendeine Aussage ist.
Und `{hA}` ist eine Name für die Annahme, dass `{A}` wahr ist.
@@ -24,15 +22,15 @@ Hint (A : Prop) (hA : A) : A => "
**Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder?
"
HiddenHint (A : Prop) (hA : A) : A =>
"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
Hint (hidden := true) "Ist doch genau wie eben:
die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
Also wird `asumption` auch wieder funktionieren."
assumption
Conclusion
"
**Untertan** Das ging ja schnell. Super! Vielen Dank.
"
NewTactics assumption
DisabledTactics tauto
NewTactic assumption
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L04_True.lean
+5 -7
View File
@@ -11,11 +11,8 @@ Introduction
Der nächste Untertan in der Reihe ist ein Schelm.
"
Statement "" :
True := by
trivial
Hint : True => "
Statement "" : True := by
Hint "
**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
bedingungslos wahr ist.
@@ -23,6 +20,7 @@ bedingungslos wahr ist.
**Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben.
"
trivial
Conclusion
"
@@ -35,5 +33,5 @@ Wie in einer Mathe-Vorlesung?
Das funktioniert nur in einer Handvoll Situationen.
"
NewTactics trivial
DisabledTactics tauto
NewTactic trivial
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+14 -17
View File
@@ -11,27 +11,24 @@ Introduction
Der Schelm hat noch eine Schwester dabei.
"
Statement "" :
¬False := by
Statement "" : ¬False := by
Hint "
**Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
wahr ist, dann ist `¬A` falsch, und umgekehrt.
**Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
**Robo** Ja, richtig.
**Du** Ist das jetzt nicht doch wieder trivial?
**Robo** Probier mal!"
trivial
Hint : ¬False => "
**Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
wahr ist, dann ist `¬A` falsch, und umgekehrt.
**Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
**Robo** Ja, richtig.
**Du** Ist das jetzt nicht doch wieder trivial?
**Robo** Probier mal!
"
Conclusion
"
Die Schwester lacht und eilt ihrem Bruder hinterher.
"
NewTactics trivial
DisabledTactics tauto
NewTactic trivial
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L06_False.lean
+6 -10
View File
@@ -15,12 +15,8 @@ Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
Statement ""
(A : Prop) (h : False) : A := by
contradiction
Hint (A : Prop) (h : False) : A =>
"
**Du** Wenn ich das jetzt richtig lese, ist `{A}` eine Aussage, und wir haben außerdem eine
Annahme names `{h}`, die besagt …
Hint "**Du** Wenn ich das jetzt richtig lese, ist `{A}` eine Aussage,
und wir haben außerdem eine Annahme names `{h}`, die besagt …
**Robo** … die besagt, dass `False` gilt.
@@ -33,8 +29,8 @@ Insbesondere die gesuchte Aussage `{A}`.
**Du** Und wie erkläre ich das jetzt diesem Formalosophen?
**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen
Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`.
"
Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`."
contradiction
Conclusion
"Der erste Querulant ist offenbar zufrieden.
@@ -45,5 +41,5 @@ Conclusion
wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
"
NewTactics contradiction
DisabledTactics tauto
NewTactic contradiction
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+5 -9
View File
@@ -17,15 +17,11 @@ Auftritt zweiter Querulant.
Statement ""
(n : ℕ) (h : n ≠ n) : n = 37 := by
Hint "**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
**Robo** Probiers mal!"
contradiction
Hint (n : ℕ) (h : n ≠ n) : n = 37 =>
"
**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
**Robo** Probiers mal!
"
Conclusion
"
**Du** Ja, scheint funktioniert zu haben.
@@ -39,5 +35,5 @@ Und gleich 38, und gleich 39, …
**Du** Ok, ok, verstehe.
"
NewTactics contradiction
DisabledTactics tauto
NewTactic contradiction
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+5 -7
View File
@@ -17,14 +17,12 @@ Auftritt dritter Querulant.
Statement ""
(n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
Hint "**Du** Wieder ein Widerspruch in den Annahmen?
**Robo** Ich sehe, du hast langsam den Dreh raus."
contradiction
Hint (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 =>
"
**Du** Wieder ein Widerspruch in den Annahmen?
**Robo** Ich sehe, du hast langsam den Dreh raus.
"
Conclusion
"
@@ -33,5 +31,5 @@ worin der Widerspruch besteht: Die Annahme `n ≠ 10` ist genau die Negation vo
Man muss `≠` immer als `¬(· = ·)` lesen.
"
NewTactics contradiction
DisabledTactics tauto
NewTactic contradiction
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L09_And.lean
+25 -13
View File
@@ -15,34 +15,46 @@ Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht.
Er legt sie uns vor, setzt sich hin, und häkelt.
"
Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
constructor
assumption
assumption
Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B =>
Hint
"
**Du**: Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt. Auch. Und beweisen sollen wir
dass `{A} und {B}` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung.
Kann ich nicht wieder `trivial` sagen?
**Robo** Nee, diesmal wird das nicht funktionieren.
**Robo**: Nee, diesmal wird das nicht funktionieren.
Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
**Du** Du meinst, `destructor`??
**Du**: Du meinst, `destructor`??
**Robo** Nein, `constructor`. Ich weiß das ist verwirrend,
**Robo**: Nein, `constructor`. Ich weiß das ist verwirrend,
aber die nennen das hier so weil man die Aussage aus mehreren Teilen
konstruieren kann.
"
HiddenHint (A : Prop) (hA : A) : A =>
constructor
-- TODO: (BUG) Hier werden beide der folgenden Hints angezeigt.
-- Das logiste Verhalten wäre, wenn jeder nur am richtigen Ort
-- angezeigt würde.
-- Ein cooles Feature wäre, wenn man nur diesen ersten Hint schreiben könnte
-- und dieser dann automatisch auch beim zweiten Goal angezeigt wird, aber dann mit `B` statt `A`.
Hint (hidden := true)
"
**Robo** Schau mal, das ist Zauberpapier.
**Robo**: Schau mal, das ist Zauberpapier.
Jetzt haben wir auf einmal zwei Beweisziele.
Hier ist dast Ziel `{A}`.
Ich glaube, Du weißt schon, wie man die jeweils erreicht.
Die Ziele stehen ja jeweils in den *Annahmen*.
"
assumption
Hint (hidden := true)
"
**Robo**: Schau mal, das ist Zauberpapier.
Jetzt haben wir auf einmal zwei Beweisziele.
Hier ist dast Ziel `{B}`.
Ich glaube, Du weißt schon, wie man die jeweils erreicht.
Die Ziele stehen ja jeweils in den *Annahmen*.
"
assumption
Conclusion
"
@@ -54,5 +66,5 @@ Ihm scheinen diese Fragen inzwischen Spaß zu machen.
Oder ist der nur gemalt? Probier mal!
"
NewTactics constructor
DisabledTactics tauto
NewTactic constructor
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L10_And.lean
+9 -16
View File
@@ -16,10 +16,7 @@ Langsam wird die Schlange kürzer. Die nächste Formalosophin, ebenfalls häkeln
Statement ""
(A B C : Prop) (h : A ∧ (B ∧ C)) : B := by
rcases h with ⟨_, ⟨g , _⟩⟩
assumption
Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => "
Hint "
**Du** Jetzt müssen wir wohl die Annahme de-konstruieren.
**Robo** Ja, genau. Das geht am einfachsten mit `rcases {h} with ⟨h₁, h₂⟩`.
@@ -30,16 +27,12 @@ Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => "
Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen
für `h₁` und `h₂`, zum Beispiel `rcases {h} with ⟨hA, hBC⟩`
"
Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B =>
"
**Robo** Das sieht doch schon besser aus! Gleich nochmal!
"
HiddenHint (A : Prop) (hA : A) : A =>
"
**Robo** Du hast einen Beweis dafür in den *Annahmen*.
"
Branch
rcases h with ⟨h₁, h₂⟩
Hint "**Robo** Das sieht doch schon besser aus! Gleich nochmal!"
rcases h with ⟨_, ⟨g , _⟩⟩
Hint (hidden := true) "**Robo** Du hast einen Beweis dafür in den *Annahmen*."
assumption
Conclusion
"
@@ -47,5 +40,5 @@ Conclusion
`rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`.
"
NewTactics rcases
DisabledTactics tauto
NewTactic rcases
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+9 -15
View File
@@ -18,12 +18,7 @@ Der nächste bitte …
Statement
""
(A B : Prop) (hA : A) : A ∨ (¬ B) := by
left
assumption
Hint (A B : Prop) (hA : A) : A ∨ (¬ B) =>
"
**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
Hint "**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
**Robo** Nein, viel einfacher. Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich
einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
@@ -31,18 +26,17 @@ einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
**Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde?
Ich will natürlich `{A}` beweisen!
**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?
"
Hint (A B : Prop) (hA : A) : ¬ B =>
"
**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
"
**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?"
Branch
right
Hint "**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal."
left
assumption
Conclusion
"
Auch dieser Formalosoph zieht zufrieden von dannen.
"
NewTactics left right assumption
DisabledTactics tauto
NewTactic left right assumption
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+17 -34
View File
@@ -20,14 +20,7 @@ Der nächste bitte …
Statement ""
(A B : Prop) (h : (A ∧ B) ∨ A) : A := by
rcases h with h | h
rcases h with ⟨h₁, h₂⟩
assumption
assumption
Hint (A B : Prop) (h :(A ∧ B) ∨ A) : A =>
"
**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
Hint "**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
wie die Klammern gesetzt sind. Irre…
**Du** Ah ich sehe, also `({A} ∧ {B}) ∨ {A}`!
@@ -41,34 +34,24 @@ Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten we
**Du** Also, wieder `rcases …`?
**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`.
"
-- -- TODO: This also triggers later under the assumptions
-- -- `(A : Prop) (B : Prop) (h₁ : A) (h₂ : B) : A`
-- -- Could we do something about that?
-- Hint (A : Prop) (B : Prop) (h : A) : A =>
-- "
-- **Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
-- Einmal unter Annahme der linken Seite `{A}`,
-- und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
-- sei wahr.
-- "
Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"
**Robo**
**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`."
rcases h with h | h
Hint "**Robo**
Jetzt musst Du Dein Ziel zweimal beweisen:
Einmal unter Annahme der linken Seite `{A} ∨ {B}`,
und einmal unter Annahme der rechten Seite `{A}`.
Hier haben nehmen wir an, die linke Seite
sei wahr.
"
HiddenHint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"
**Robo** Wie man mit einem Und in den Annahmen umgeht, weißt Du doch schon:
`rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`.
"
sei wahr."
Hint (hidden := true) " **Robo** Wie man mit einem Und in den Annahmen umgeht,
weißt Du doch schon:
`rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`."
rcases h with ⟨h₁, h₂⟩
Hint "**Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
Einmal unter Annahme der linken Seite `{A}`,
und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
sei wahr."
assumption
assumption
Conclusion
"**Du** Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele…
@@ -125,5 +108,5 @@ Die Worte, die Du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`. H
"
NewTactics assumption rcases
DisabledTactics tauto
NewTactic assumption rcases
DisabledTactic tauto
server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+77 -38
View File
@@ -14,7 +14,9 @@ Introduction
"
Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vorherigen.
**Robo** Wirf einfach alles drauf, was Du gelernt hast. Hier, ich bin sogar so nett und zeig Dir noch einmal die vier wichtigsten Taktiken für diese Situation an.
**Robo** Wirf einfach alles drauf, was Du gelernt hast.
Hier, ich bin sogar so nett und zeig Dir noch einmal die vier
wichtigsten Taktiken für diese Situation an.
| (Übersicht) | Und (`∧`) | Oder (`∨`) |
|-------------|:-------------------------|:------------------------|
@@ -26,46 +28,83 @@ Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vor
Statement ""
(A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
constructor
rcases h with h | h
left
assumption
rcases h with ⟨h₁, h₂⟩
right
assumption
rcases h with h | h
left
assumption
rcases h with ⟨h₁, h₂⟩
right
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
"**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
Hint (hidden := true)
"**Robo**: Ich würd zuerst die Annahme {h} mit `rcases {h}` aufteilen."
Branch
constructor
· rcases h with h' | h'
· left
assumption
· rcases h' with ⟨h₁, h₂⟩
right
assumption
· rcases h with h' | h'
· left
assumption
· rcases h' with ⟨h₁, h₂⟩
right
assumption
rcases h
Hint (hidden := true) "**Robo**: Jetzt kannst Du das `∧` im Goal mit `constructor` angehen."
· constructor
· left
assumption
· left
assumption
· Hint (hidden := true)
"**Robo**: Hier würde ich die Annahme {h} nochmals mit `rcases` aufteilen."
Branch
constructor
· Hint "**Robo**: Der Nachteil an der Reihenfolge ist, dass du jetzt in jedem Untergoal
`rcases h` aufrufen musst."
Branch
right
rcases h with ⟨h₁, h₂⟩
assumption
rcases h with ⟨h₁, h₂⟩
right
assumption
· Branch
right
rcases h with ⟨h₁, h₂⟩
assumption
rcases h with ⟨h₁, h₂⟩
right
assumption
rcases h with ⟨h₁, h₂⟩
constructor
· right
assumption
· right
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
-- "**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
-- TODO: Hint nur Anhand der Annahmen?
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
"**Robo** `left` oder `right`?"
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
-- -- TODO: Hint nur Anhand der Annahmen?
-- HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
-- "**Robo** `left` oder `right`?"
Conclusion
"
@@ -74,5 +113,5 @@ Conclusion
Königin *Logisinde* ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
"
NewTactics left right assumption constructor rcases rfl contradiction trivial
DisabledTactics tauto
NewTactic left right assumption constructor rcases rfl contradiction trivial
DisabledTactic tauto
server/testgame/TestGame/Levels/SetTheory.lean
+15
View File
@@ -23,6 +23,21 @@ Game "TestGame"
World "SetTheory"
Title "Mengenlehre"
Introduction
"Der größere der beiden Monde sieht dunkelrot und karg aus. Trotzdem sollen dort nomadische
Gesellschaften wohnen, die sich in der Einöde zurechtfinden.
Ihr steuert einen der wenigen befestigten Standorte am Fusse eines Berges an.
**Robo**: Die Bevölkerung hier lebt so abgekapselt vom Rest des Universums, dass sie sich
vermutlich noch viel besser mit alter Sprache und Schrift auskennt.
**Du**: Hoffen wir, dass sie uns weiterhelfen können dieses Buch der Urbilder zu entschlüsseln.
Sofort begrüßt euch eine ältere Frau, die sich als *Mengitte*, die Beschützerin des Mondes,
vorstellt.
"
Game "TestGame"
World "SetTheory2"
Title "Mehr Mengenlehre"
server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
+35 -17
View File
@@ -14,29 +14,47 @@ Title "Mengen"
Introduction
"
In diesem Kapitel schauen wir uns Mengen an.
**Mengitte**: Ich würde leider den Inhalt jenes Buches eh nicht verstehen. Aber der beste Weg für
euch, dieses zu entschlüsseln ist, euch ausgiebig mit der Bevölkerung hier zu unterhalten.
Lebt mit ihnen, redet mit ihnen und ihr werdet die Sprache automatisch lernen.
Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst,
alle Elemente in einer Menge haben den gleichen Typ.
**Mengitte**: Seit aber vorgewarnt, die Leute hier denken ganz viel über Mengen nach,
womit sie immer *homogene Mengen* meinen. Eine Menge natürlicher Zahlen `{1, 4, 6}` ist
verständlich, aber sowas wie eine Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` gibt es hier
einfach nicht. Punkt.
Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine
Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben.
**Robo**: Als Kontext: Wenn `A` ein beliebiger `Type` ist, dann ist `(U : Set A)` eine Menge
mit Elementen aus `A`
Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus
`X`. `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied
zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht
austauschbar!
Um zu beweisen, dass etwas in `univ` ist, kannst du verschiedenste deiner Taktiken anwenden,
zum Beispiel `tauto`.
**Mengitte**: Damit ich weiss, dass ihr euch grundsätzlich mit den Leuten austauschen könnt,
erklärt mir doch folgendes:
"
open Set
Statement mem_univ
"4 ist ein Element der Menge aller natürlichen Zahlen." {A : Type _} (x : A) :
x ∈ (univ : Set A) := by
Statement mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by
trivial
-- tauto
NewTactics tauto trivial
Hint (A : Type) (x : A) : x ∈ (univ : Set A) =>
"**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
**Robo** … und `univ` ist die Menge aller Elemente in `A`.
**Du** ist das nicht einfach `A` selber?
**Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
**Du**: Unlogisch.
**Mengites**: Naja, Typen und Mengen sind halt zwei unterschiedliche Sachen und wenn ihr
über Mengen sprechen wollt, müssen alles Mengen sein.
**Du**: Na gut. Und wieso `x ∈ univ` und nicht `x : univ` wie bei Typen?
**Robo**: Jedes Element `(x : A)` hat entweder die Eigenschaft `x ∈ U` oder `x ∉ U` für eine
Menge `(U : Set A)`. (`\\in`, `\\nin`)
**Du**: Also das ist ja dann trivial. Hoffentlich sehen die das hier auch so…
"
Conclusion "**Mengitte**: Ja das stimmt schon. Dann wünsche ich euch viel Erfolg auf eurer Reise!"
server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
+13 -8
View File
@@ -13,17 +13,22 @@ Title "leere Menge"
Introduction
"
Gleich wie bei `univ` gibt es leere Mengen `∅` von verschiedenen Typen.
So ist `(∅ : Set ℕ)` in Lean nicht das gleiche wie `(∅ : Set ℤ)`. (`\\empty`)
Zudem hat die Verneinung `¬ (x ∈ A)` die Notation `x ∉ A` (`\\nin`), gleich wie bei `=` and `≠`.
Um zu zeigen, dass etwas nicht in der leeren Menge ist, kannst du wieder `tauto` verwenden.
Ihr zieht also durch die Gegend und redet mit den Leuten. Ein Junge rennt zu euch und fragt:
"
open Set
Statement not_mem_empty
"Kein Element ist in der leeren Menge enthalten." {A : Type _} (x : A) :
Statement not_mem_empty "" {A : Type} (x : A) :
x ∉ (∅ : Set A) := by
tauto
NewLemma mem_univ
Hint (A : Type) (x : A) : x ∉ (∅ : Set A) =>
"**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles tautologisches Zeugs...
**Robo**: Dann behaupte das doch. (`\\empty`)"
Conclusion "Der Junge rennt weiter.
**Du**: So wird das ganze schon angenehmer."
server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+6 -6
View File
@@ -28,18 +28,18 @@ namespace MySet
open Set
theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
trivial
-- theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
-- trivial
theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
tauto
-- theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
-- tauto
Statement subset_empty_iff
"." (A : Set ℕ) : A ⊆ univ := by
intro h hA
apply mem_univ -- or `trivial`.
trivial --apply mem_univ -- or `trivial`.
NewTactics intro trivial apply
NewTactic intro trivial apply
-- blocked: tauto simp
end MySet
server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+2 -2
View File
@@ -54,8 +54,8 @@ Statement subset_empty_iff
rcases a with ⟨h₁, h₂⟩
assumption
NewTactics constructor intro rw assumption rcases simp tauto trivial
NewTactic constructor intro rw assumption rcases simp tauto trivial
NewLemmas Subset.antisymm_iff empty_subset
NewLemma Subset.antisymm_iff empty_subset
end MySet
server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
+2 -2
View File
@@ -45,8 +45,8 @@ Statement eq_empty_iff_forall_not_mem
rw [←subset_empty_iff]
rfl -- This is quite a miracle :)
NewTactics constructor intro rw assumption rcases simp tauto trivial
NewTactic constructor intro rw assumption rcases simp tauto trivial
NewLemmas Subset.antisymm_iff empty_subset
NewLemma Subset.antisymm_iff empty_subset
end MySet

Some files were not shown because too many files have changed in this diff Show More