diff --git a/client/src/components/Infoview.tsx b/client/src/components/Infoview.tsx deleted file mode 100644 index a1d8d2c..0000000 --- a/client/src/components/Infoview.tsx +++ /dev/null @@ -1,152 +0,0 @@ -import * as React from 'react'; -import { useEffect, useState, useRef } from 'react'; -import { EditorApi } from '@leanprover/infoview-api' -import { LeanClient } from 'lean4web/client/src/editor/leanclient'; -import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import * as ls from 'vscode-languageserver-protocol' -import TacticState from './TacticState'; -import { useLeanClient } from '../connection'; -import { useAppDispatch } from '../hooks'; -import { levelCompleted, selectCompleted } from '../state/progress'; - -// TODO: move into Lean 4 web -function toLanguageServerPosition (pos: monaco.Position): ls.Position { - return {line : pos.lineNumber - 1, character: pos.column - 1} -} - -function Infoview({ worldId, levelId, editor, editorApi } : {worldId: string, levelId: number, editor: monaco.editor.IStandaloneCodeEditor, editorApi: EditorApi}) { - const dispatch = useAppDispatch() - const [rpcSession, setRpcSession] = useState() - const [goals, setGoals] = useState(null) - const [completed, setCompleted] = useState(false) - const [diagnostics, setDiagnostics] = useState(undefined) - - /* `globalDiagnostics` is a work-around to show something when the proof is complete - but had previous subgoals with `sorry` or errors. - - It is displayed whenever there are no goals and no (error)-messages present and the proof - isn't complete. */ - const [globalDiagnostics, setGlobalDiagnostics] = useState(undefined) - - const {uri} = useEditorUri(editor) - const {leanClient, leanClientStarted} = useLeanClient() - - const fetchInteractiveGoals = () => { - if (editor && rpcSession && editor.getPosition()) { - const pos = toLanguageServerPosition(editor.getPosition()) - - leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getGoals", - "params":{"textDocument":{uri}, "position": pos}, - "sessionId":rpcSession, - "textDocument":{uri}, - "position": pos - }).then((res) => { - setGoals(res ? res.goals : null) - console.log(goals) - }).catch((err) => { - console.error(err) - }) - - leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics", - "params":{"textDocument":{uri}, "lineRange": {start: pos.line, end: pos.line + 1}}, - "sessionId":rpcSession, - "textDocument":{uri}, - "position": pos - }).then((res) => { - - /* Workaround to not display the error `unsolved goals` */ - if (res) {res = res.filter(x => x.message.trim() !== 'unsolved goals')} - - setDiagnostics(res ? res : undefined) - console.log(res) - }).catch((err) => { - console.error(err) - }) - - } - } - - const checkCompleted = () => { - if (editor && rpcSession && editor.getPosition()) { - const pos = toLanguageServerPosition(editor.getPosition()) - // Get all diagnostics independent of cursor position - leanClient.sendRequest("$/lean/rpc/call", {"method":"Game.getDiagnostics", - "params":{"textDocument":{uri},}, - "sessionId":rpcSession, - "textDocument":{uri}, - "position": pos - }).then((res) => { - // Check that there are no errors and no warnings - const completed = !res.some(({severity}) => severity <= 2) - if (completed) { - dispatch(levelCompleted({world: worldId, level: levelId})) - } - setCompleted(completed) - setGlobalDiagnostics(res) - }).catch((err) => { - console.error(err) - }) - } - } - - useEffect(() => { - if (editor) { - fetchInteractiveGoals() - checkCompleted() - } - }, [editor, uri, rpcSession]); - - useEffect(() => { - if (editorApi && leanClientStarted && uri) { - editorApi.closeRpcSession(rpcSession) - setRpcSession(undefined) - console.log(uri) - editorApi.createRpcSession(uri).then((rpcSession) => { - setRpcSession(rpcSession) - }) - } - }, [editorApi, uri]); - - useEffect(() => { - if (editor) { - const t = editor.onDidChangeCursorPosition(async (ev) => { - fetchInteractiveGoals() - }) - return () => { t.dispose() } - } - }, [editor, rpcSession]) - - useEffect(() => { - const t = leanClient.didChange(async (ev) => { - fetchInteractiveGoals() - checkCompleted() - }) - return () => { t.dispose() } - }, [editor, leanClient, rpcSession]) - - return (
- -
) -} - -export default Infoview - -const useEditorUri = (editor: monaco.editor.IStandaloneCodeEditor) => { - const [uri, setUri] = useState(undefined) - - useEffect(() => { - if (editor) { - const t = editor.onDidChangeModel((ev) => { - if (ev.newModelUrl) { - setUri(ev.newModelUrl.toString()) - } else { - setUri(undefined) - } - }) - return () => {t.dispose()} - } - }, [editor]) - - return {uri} -} diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 43939c6..5031dc9 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -20,7 +20,6 @@ import 'lean4web/client/src/editor/infoview.css' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import './level.css' import { ConnectionContext, useLeanClient } from '../connection'; -import Infoview from './Infoview'; import { useParams } from 'react-router-dom'; import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; import { codeEdited, selectCode } from '../state/progress'; diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx deleted file mode 100644 index b51b7ae..0000000 --- a/client/src/components/TacticState.tsx +++ /dev/null @@ -1,142 +0,0 @@ -import * as React from 'react'; -import '@fontsource/roboto/300.css'; -import '@fontsource/roboto/400.css'; -import '@fontsource/roboto/500.css'; -import '@fontsource/roboto/700.css'; - -import List from '@mui/material/List'; -import ListItem from '@mui/material/ListItem'; -import { Paper, Box, Typography, Alert, FormControlLabel, FormGroup, Switch, Collapse, CircularProgress } from '@mui/material'; -import { Accordion, AccordionSummary, AccordionDetails, Divider } from '@mui/material'; -import ExpandMoreIcon from '@mui/icons-material/ExpandMore'; - -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faArrowPointer } from '@fortawesome/free-solid-svg-icons' -import Markdown from './Markdown'; - -// TODO: Dead variables (x✝) are not displayed correctly. - -function Goal({ goal }) { - - const [showHints, setShowHints] = React.useState(false); - - const handleHintsChange = () => { - setShowHints((prev) => !prev); - }; - - const hasObject = typeof goal.objects === "object" && goal.objects.length > 0 - const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0 - const openMessages = typeof goal.messages === "object" ? goal.messages.filter((msg) => ! msg.spoiler) : [] - const hints = typeof goal.messages === "object" ? goal.messages.filter((msg) => msg.spoiler) : [] - const hasHints = hints.length > 0 - return ( - - {hasObject && Objects - - {goal.objects.map((item, index) => - - {item.userName} : - {item.type} - )} - } - {hasAssumption && Assumptions - - {goal.assumptions.map((item, index) => {item.userName} : - {item.type})} - } - Prove: - {goal.goal} - {openMessages.map((message) => {message.message})} - {hasHints && - } - label="More Help?" - />} - {hints.map((hint, index) => {hint.message})} - ) -} - -/* Function to display a goal that is not the main goal. */ -function OtherGoal({ goal }) { - - const hasObject = typeof goal.objects === "object" && goal.objects.length > 0 - const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0 - - return ( - - }> - ⊢ {goal.goal} - - - {hasObject && - - Objects - - {goal.objects.map((item, index) => - - {item.userName} : - {item.type} - )} - - } - {hasAssumption && - - Assumptions - - {goal.assumptions.map((item, index) => - - {item.userName} : - {item.type} - )} - - } - Prove: - {goal.goal} - - ) -} - -function TacticState({ goals, diagnostics, completed, globalDiagnostics }) { - const isLoading = goals === null - const hasGoal = goals !== null && goals.length > 0 - const hasManyGoal = hasGoal && goals.length > 1 - - if (!(hasGoal || completed) && globalDiagnostics) { - diagnostics = [{"severity" : 4, "message": "Showing global messages:"}, ...globalDiagnostics] - } - - const hasError = typeof diagnostics === "object" && diagnostics.length > 0 - - return ( - - {completed && Level completed ! 🎉} - {hasGoal && - - Main Goal - (at ) - - - } - {isLoading && } - {!(hasGoal || completed || isLoading) && - - No goals - (at ) - } - {hasError && - - Lean says - {diagnostics.map(({severity, message}, index) => - {message} - // TODO: When does Lean give severity=4? Had colour `gray` before. Make custom theme for that - )} - } - {hasManyGoal && - Further Goals - {goals.slice(1).map((goal, index) => )} - } - - ) -} - -export default TacticState diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 1a290bf..27ffad7 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -143,7 +143,7 @@ export const Goal = React.memo((props: GoalProps) => { if (props.goal.goal.isRemoved) cn += 'b--removed ' // TODO: make this prettier - const hints = goal.messages.map((m) =>
{m.message}
) + const hints = goal.hints.map((m) =>
{m.text}
) if (goal.goal.userName) { return
diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 8899f82..a7ca772 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -121,7 +121,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { {goals && } + goals={termGoal !== undefined ? {goals: [{goal:termGoal, hints: []}]} : undefined} /> {userWidgets.map(widget =>
{widget.name} diff --git a/client/src/components/infoview/rpcApi.ts b/client/src/components/infoview/rpcApi.ts index f07cece..016b6c0 100644 --- a/client/src/components/infoview/rpcApi.ts +++ b/client/src/components/infoview/rpcApi.ts @@ -1,13 +1,13 @@ import { InteractiveGoals, InteractiveGoal } from '@leanprover/infoview-api'; -export interface GameMessage { - message: string; - spoiler: boolean; +export interface GameHint { + text: string; + hidden: boolean; } export interface GameInteractiveGoal { goal: InteractiveGoal; - messages: GameMessage[]; + hints: GameHint[]; } export interface GameInteractiveGoals { diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index dcc398e..27a8181 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -123,7 +123,7 @@ elab "Path" s:Parser.path : command => do end metadata -/-! ## Messages -/ +/-! ## Hints -/ open Lean Meta Elab Command Term @@ -144,38 +144,37 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term | (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail))) | [] => return s -/-- Declare a message. This version doesn't prevent the unused linter variable from running. -/ -local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do +/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/ +local elab "Hint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList let g ← liftTermElabM do (return ← elabTermAndSynthesize g none) - modifyCurLevel fun level => pure {level with messages := level.messages.push { + modifyCurLevel fun level => pure {level with hints := level.hints.push { goal := g, intros := decls.size, - message := msg.getString }} + text := msg.getString }} /-- Declare a hint. This version doesn't prevent the unused linter variable from running. -The difference between hints/messages is that hints should be hidden by default, while -messages are visible. +A hidden hint is only displayed if explicitly requested by the user. -/ -local elab "Hint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do +local elab "HiddenHint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList let g ← liftTermElabM do (return ← elabTermAndSynthesize g none) - modifyCurLevel fun level => pure {level with messages := level.messages.push { + modifyCurLevel fun level => pure {level with hints := level.hints.push { goal := g, intros := decls.size, - spoiler := true, - message := msg.getString }} + hidden := true, + text := msg.getString }} -/-- Declare a message in reaction to a given tactic state in the current level. -/ -macro "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do - `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg) - /-- Declare a hint in reaction to a given tactic state in the current level. -/ macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do `(set_option linter.unusedVariables false in Hint' $decls* : $goal => $msg) +/-- Declare a hidden hint in reaction to a given tactic state in the current level. -/ +macro "HiddenHint" decls:mydecl* ":" goal:term "=>" msg:str : command => do + `(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg) + /-! ## Tactics -/ /-- Declare a documentation entry for some tactic. diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 1f755a0..c4e97c6 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -8,20 +8,20 @@ defined in this file. open Lean -/-! ## Messages -/ +/-! ## Hints -/ /-- -A message to be displayed to the user as instruction/hint. +A hint to help the user with a specific goal state Fields (TODO) - spoiler: If true, then message should be hidden by default + hidden: If true, then hint should be hidden by default -/ -structure GoalMessageEntry where +structure GoalHintEntry where goal : Expr intros : Nat - message : String - spoiler : Bool := false + text : String + hidden : Bool := false deriving Repr /-! ## Tactic documentation -/ @@ -200,7 +200,7 @@ structure GameLevel where conclusion: String := default tactics: Array TacticDocEntry := default lemmas: Array LemmaDocEntry := default - messages: Array GoalMessageEntry := default + hints: Array GoalHintEntry := default goal : TSyntax `Lean.Parser.Command.declSig := default descrText: String := default descrFormat : String := default diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index 791ef7f..06b265f 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -10,57 +10,13 @@ open Meta /-! ## GameGoal -/ -structure GameLocalDecl where - userName : Name - type : String +structure GameHint where + text : String + hidden : Bool deriving FromJson, ToJson -structure GameMessage where - message : String - spoiler : Bool -deriving FromJson, ToJson - -structure GameGoal where - objects : List GameLocalDecl - assumptions : List GameLocalDecl - goal : String - messages : Array GameMessage -deriving FromJson, ToJson - - -def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array GameMessage) : MetaM GameGoal := do -match (← getMCtx).findDecl? goal with -| none => throwError "unknown goal" -| some mvarDecl => do - -- toGameGoalAux below will sort local declarations from the context of goal into data and assumptions, - -- discarding auxilliary declarations - let rec toGameGoalAux : List (Option LocalDecl) → MetaM (List LocalDecl × List LocalDecl) - | (some decl)::t => withLCtx mvarDecl.lctx mvarDecl.localInstances do - let (o, a) ← toGameGoalAux t - if decl.isAuxDecl then - return (o, a) - if (← inferType decl.type).isProp then - return (o, decl::a) - else - return (decl::o, a) - | none:: t => toGameGoalAux t - | [] => return ([], []) - withLCtx mvarDecl.lctx mvarDecl.localInstances do - let (objects, assumptions) ← toGameGoalAux mvarDecl.lctx.decls.toList - let objects ← objects.mapM fun decl => do - return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) } - let assumptions ← assumptions.mapM fun decl => do - return { userName := decl.userName, type := toString (← Meta.ppExpr decl.type) } - return {objects := objects, assumptions := assumptions, goal := toString (← Meta.ppExpr mvarDecl.type), messages } - namespace GameServer -/-- `Game.getGoals` client<-server reply. -/ -structure PlainGoal where - /-- The pretty-printed goals, empty if all accomplished. -/ - goals : Array GameGoal - deriving FromJson, ToJson - -- TODO: Find a better way to pass on the file name? def levelIdFromFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String) : m LevelId := do let fileParts := fileName.splitOn "/" @@ -99,26 +55,26 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := return true open Meta in -/-- Find all messages whose trigger matches the current goal -/ -def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameMessage) := do +/-- Find all hints whose trigger matches the current goal -/ +def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array GameHint) := do goal.withContext do let level ← getLevelByFileName doc.meta.mkInputContext.fileName - let messages ← level.messages.filterMapM fun message => do - let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros + let hints ← level.hints.filterMapM fun hint => do + let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros -- TODO: Protext mvars in the type of `goal` to be instantiated? - if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions + if ← isDefEq hintGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions then let lctx ← getLCtx -- Local context of the `goal` if ← matchDecls declMvars lctx.getFVars then - return some { message := message.message, spoiler := message.spoiler } + return some { text := hint.text, hidden := hint.hidden } else return none else return none - return messages + return hints structure GameInteractiveGoal where goal : InteractiveGoal - messages: Array GameMessage + hints: Array GameHint deriving RpcEncodable structure GameInteractiveGoals where @@ -148,8 +104,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore let goals ← ci.runMetaM {} do goals.mapM fun goal => do - let messages ← findMessages goal doc - return {goal := ← Widget.goalToInteractive goal, messages} + let hints ← findHints goal doc + return {goal := ← Widget.goalToInteractive goal, hints} -- compute the goal diff -- let goals ← ciAfter.runMetaM {} (do -- try diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean index 5c350b9..467ffee 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean @@ -42,11 +42,11 @@ Statement assumption contradiction -Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. " -Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => " Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\" diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean index 6b977d9..29e586e 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean @@ -42,11 +42,11 @@ Statement apply h assumption -Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. " -Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => " Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\" In Lean : diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean index d88106c..3b4551b 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean @@ -39,14 +39,14 @@ muss." assumption -Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) : ¬ A => +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`." -Message (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => +Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => "Jetzt kannst du mit `suffices` oder `have` Fortschritt machen." -Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => +HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => "Zum Beispiel `suffices hb : B`." diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean index 0c41219..c4d44df 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean @@ -40,7 +40,7 @@ Statement not_imp_not -- TODO: Forbidden Tactics: apply, rw -- TODO: forbidden Lemma: not_not -Hint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) => +HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) => "" diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean index 94f0ae7..ed3f32d 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean @@ -43,22 +43,22 @@ Statement rw [not_odd] apply even_square -Hint (n : ℕ) (h : Odd (n ^ 2)) : Odd n => +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`!" -Message (n : ℕ) : Odd (n ^ 2) → Odd n => +Hint (n : ℕ) : Odd (n ^ 2) → Odd n => "Mit `contrapose` kann man die Implikation zu `¬ (Not n) → ¬ (Odd n^2)` umkehren." -Message (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`." +Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`." -Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden." +HiddenHint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden." -Message (n : ℕ) : Even n → ¬Odd (n ^ 2) => +Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) => "rw [not_odd] muss hier zweimal angewendet werden." -Message (n : ℕ) : Even n → Even (n ^ 2) => +Hint (n : ℕ) : Even n → Even (n ^ 2) => "Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek." Tactics contrapose rw apply diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean index bc7f5db..20dc4ac 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean @@ -40,10 +40,10 @@ Statement apply even_square assumption -Hint (n : ℕ) (h : Odd (n^2)) : Odd n => +HiddenHint (n : ℕ) (h : Odd (n^2)) : Odd n => "Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten." -Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False => +Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False => " Am sinnvollsten ist es, hier einen Widerspruch zu `Odd (n^2)` zu suchen. Dafür kannst du @@ -54,20 +54,20 @@ contradiction benützen. " -Hint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False => +HiddenHint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False => "Hier brauchst du nur `contradiction`." -Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) => +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." -Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) => +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." -Message (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => +Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => "Diese Aussage hast du bereits als Lemma bewiesen." -Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => +HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => "Probiers mit `apply ...`" diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean index 5ef9e51..d5735cf 100644 --- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean +++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean @@ -31,10 +31,10 @@ Statement assumption assumption -Hint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) => +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." -Message (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) => +Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) => "Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden." Tactics intro constructor assumption diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean index 8838cf4..e76d7eb 100644 --- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean +++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean @@ -36,7 +36,7 @@ dass $B$ wahr ist." revert ha assumption -Hint (A : Prop) (B : Prop) (ha : A) (h : A → B): B => +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." Tactics revert assumption diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean index 73c4a2b..7727721 100644 --- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean @@ -25,10 +25,10 @@ Statement apply g assumption -Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B => +HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B => "Mit `apply g` kannst du die Implikation `g` anwenden." -Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A => +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." diff --git a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean index cd49a9b..7d18abc 100644 --- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean @@ -22,13 +22,13 @@ Statement apply f assumption -Hint (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C => +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." -Message (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C => +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." -Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C => +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." diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean index 4bb684e..155127c 100644 --- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean @@ -28,22 +28,22 @@ Statement apply f assumption -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) +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." -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) +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." -Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) +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." -Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) +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." diff --git a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean index b845c60..54b93c8 100644 --- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean @@ -25,10 +25,10 @@ Statement assumption assumption -Hint (A : Prop) (B : Prop) : A ↔ B => +HiddenHint (A : Prop) (B : Prop) : A ↔ B => "Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen." -Hint (A : Prop) (B : Prop) (h : A → B) : A → B => +HiddenHint (A : Prop) (B : Prop) (h : A → B) : A → B => "Such mal in den Annahmen." Conclusion diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean index 81d44e3..93d67bd 100644 --- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean +++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean @@ -36,38 +36,38 @@ Statement rw [←h₂] assumption -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C => +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₁]`." -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : A ↔ C => +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₁]`." -Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D => +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)" -Hint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B => +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`. -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ C) : B ↔ C => +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?" -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : B ↔ D) : B ↔ C => +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?" -Message (A : Prop) (B : Prop) (h : B ↔ A) : A ↔ B => +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.)" -Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : D ↔ A) : B ↔ C => +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..." -Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : A ↔ D) : B ↔ C => +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..." diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean index bc566d9..d0cabaf 100644 --- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean @@ -30,13 +30,13 @@ Statement apply h.mp assumption -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C => "Fange wie immer mit `intro` an." -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C => +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." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B => +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." diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean index 48b95e1..41f7c4f 100644 --- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean @@ -25,10 +25,10 @@ Statement rcases h assumption -Hint (A : Prop) (B : Prop) : (A ↔ B) → A → B => +HiddenHint (A : Prop) (B : Prop) : (A ↔ B) → A → B => "Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist." -Hint (A : Prop) (B : Prop) (h : A ↔ B) : A → B => +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." diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean index da84543..4b57f5c 100644 --- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean @@ -40,10 +40,10 @@ Statement intro assumption -Hint (A : Prop) : ¬A ∨ A => +HiddenHint (A : Prop) : ¬A ∨ A => "Das Lemma wendest du mit `apply not_or_of_imp` an." -Hint (A : Prop) : A → A => +HiddenHint (A : Prop) : A → A => "Wie immer, `intro` ist dein Freund." Conclusion diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean index 5bfdb3e..6569583 100644 --- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean +++ b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean @@ -52,28 +52,28 @@ Statement imp_iff_not_or contradiction assumption -Hint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B => +HiddenHint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B => "Eine Äquivalenz im Goal geht man immer mit `constructor` an." -Hint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B => +HiddenHint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B => "Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet." -Hint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B => +HiddenHint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B => "Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet." -Hint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) => +HiddenHint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) => "Eine Implikation geht man fast immer mit `intro h` an." -Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => +HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => "Nochmals `intro`." -Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => +HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => "Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen." -Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B => +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." -Hint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B => +HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B => "Findest du einen Widerspruch?" Tactics rfl assumption trivial left right constructor rcases diff --git a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean index b1798e7..17930a8 100644 --- a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean +++ b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean @@ -35,36 +35,36 @@ Statement and_or_imp assumption assumption -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) => "Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`." -- If starting with `left`. -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : B => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : B => "Da kommst du nicht mehr weiter..." -- If starting with `right`. -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : (C ∧ A) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) : (C ∧ A) => "Da kommst du nicht mehr weiter..." -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) => "`left` oder `right`?" -Hint (A : Prop) (B : Prop) (C : Prop) (h : B) (hA : A) : B ∨ (C ∧ A) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B) (hA : A) : B ∨ (C ∧ A) => "`left` oder `right`?" -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) => "Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B => "Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C => "Sackgasse." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A => "Hmmm..." -Message (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A => "Ein UND im Goal kann mit `constructor` aufgeteilt werden." Tactics left right assumption constructor rcases diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean index a2a8c77..b0f6232 100644 --- a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean +++ b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean @@ -54,7 +54,7 @@ Statement -Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) => +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 : ℕ) → `" diff --git a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean index 6304881..31c3006 100644 --- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean +++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean @@ -29,7 +29,7 @@ Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring -Hint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 => +HiddenHint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 => "`ring` übernimmt den ganzen Spaß." Conclusion diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean index de26cf0..22ee139 100644 --- a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean @@ -28,39 +28,39 @@ Zeige dass $b = c$." rw [←h₂] assumption -Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c => +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₁]`." -Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = c => +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₁]`." -Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d => +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)" -Hint (a : ℕ) (b : ℕ) (h : a = b) : a = b => +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`. -Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = c) : b = c => +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?" -Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : b = d) : b = c => +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?" -Message (a : ℕ) (b : ℕ) (h : b = a) : a = b => +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.)" -Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c => +Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c => "das ist nicht der optimale Weg..." -Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c => +Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c => "das ist nicht der optimale Weg..." diff --git a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean index e540543..2395208 100644 --- a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean @@ -28,10 +28,10 @@ Zeige dass $b + b ^ 2 = b + 1$." rw [h] at g assumption -Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 => +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." -Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 => +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 diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean index 85ae5f3..42460c2 100644 --- a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean +++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean @@ -22,10 +22,10 @@ Statement rw [h] ring -Message (x : ℕ) (y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y => +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." -Message (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y => +Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y => "Jetzt kann `ring` übernehmen." Conclusion "" diff --git a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean index e8851a6..8bbcd67 100644 --- a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean +++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean @@ -42,29 +42,29 @@ Statement even_square rw [hx] ring -Message (n : ℕ) (h : Even n) : Even (n ^ 2) => +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." -Message (n : ℕ) (h : ∃ r, n = 2 * r) : ∃ r, n ^ 2 = 2 * r => +Hint (n : ℕ) (h : ∃ r, n = 2 * r) : ∃ r, n ^ 2 = 2 * 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." -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = 2 * r => +Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = 2 * r => "Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass die Aussage erfüllen soll." -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r => +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." -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => +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..." -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => +Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => "Die Taktik `ring` löst solche Gleichungen." Tactics unfold rcases use rw ring diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean index 444151c..9d6af52 100644 --- a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean +++ b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean @@ -43,7 +43,7 @@ Statement rw [hy] ring -Message (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even (n + 1) => +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 : ℕ) → `" diff --git a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean index 8eb1d59..306dd9e 100644 --- a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean +++ b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean @@ -35,30 +35,30 @@ Statement unfold Even use n -Message : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) => +Hint : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) => "`push_neg` schiebt die Negierung an den Quantoren vorbei." -Message (n : ℕ) : (∃ k, ¬Odd (n + k)) => +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." -Hint (n : ℕ) : ¬Odd (n + n) => +HiddenHint (n : ℕ) : ¬Odd (n + n) => "Du kennst ein Lemma um mit `¬odd` umzugehen." --- Hint (n : ℕ) (k : ℕ) : ¬odd (n + k) => +-- HiddenHint (n : ℕ) (k : ℕ) : ¬odd (n + k) => -- "Du kennst ein Lemma um mit `¬odd` umzugehen." -Hint (n : ℕ) : Even (n + n) => +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." --- Hint (n : ℕ) (k : ℕ) : even (n + k) => +-- HiddenHint (n : ℕ) (k : ℕ) : even (n + k) => -- "`unfold even` hilft hier weiter." -Message (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`." +Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`." Conclusion "" diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 2db30d2..3e82469 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -31,10 +31,10 @@ Statement "Zeige $ 42 = 42 $." : 42 = 42 := by rfl --- Message : 42 = 42 => +-- Hint : 42 = 42 => -- "Die Taktik `rfl` beweist ein Goal der Form `X = X`." -Hint : 42 = 42 => +HiddenHint : 42 = 42 => "Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile." Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"." diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index 9927e91..0bb2704 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -26,7 +26,7 @@ Statement (n : ℕ) (h : 1 < n) : 1 < n := by assumption -Hint (n : ℕ) (h : 1 < n) : 1 < n => +HiddenHint (n : ℕ) (h : 1 < n) : 1 < n => "`assumption` sucht nach einer Annahme, die dem Goal entspricht." diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index b7edbfe..9ffd29d 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -22,7 +22,7 @@ Zeige, dass $A$ wahr ist." (A : Prop) (hA : A) : A := by assumption -Hint (A : Prop) (hA : A) : A => +HiddenHint (A : Prop) (hA : A) : A => "Auch hier kann `assumption` den Beweis von `A` finden." Conclusion "" diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 7dfecdd..34cd0ac 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -23,7 +23,7 @@ Zeige, dass daraus $A$ folgt." (A : Prop) (h : False) : A := by contradiction -Hint (A : Prop) (h : False) : A => +HiddenHint (A : Prop) (h : False) : A => "Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen, unabhängig davon, was das Goal ist." diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index f11ec9c..3fe50d0 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -26,10 +26,10 @@ Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by assumption assumption -Hint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => +HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => "`constructor` zerlegt die Struktur in Einzelteile." -Hint (A : Prop) (hA : A) : A => +HiddenHint (A : Prop) (hA : A) : A => "Du hast einen Beweis dafür in den *Annahmen*." Tactics constructor assumption @@ -51,24 +51,24 @@ Tactics constructor assumption -- intro -- assumption --- Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => +-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => -- "`↔` oder `∧` im Goal kann man mit `constructor` zerlegen." --- Message (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => +-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => -- "Hier würdest du mit `intro` die Implikation angehen. -- (Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf -- das UND in der Implikationsannahme)" -- -- if they don't use `intro ⟨_, _⟩`. --- Message (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => +-- Hint (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => -- "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen." --- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => +-- HiddenHint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => -- "Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?" -- -- Rückrichtung --- Message (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => -- "Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$ -- Da hilft `intro`. @@ -78,16 +78,16 @@ Tactics constructor assumption -- -- if they don't use `intro ⟨_, _⟩`. --- Message (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => -- "Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen." --- Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => +-- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => -- "Wieder in Einzelteile zerlegen..." --- Message (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => -- "Immer das gleiche ... noch mehr zerlegen." --- -- Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => +-- -- Hint (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => -- -- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen, -- -- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`). diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 6688905..461217f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -26,11 +26,11 @@ Statement "Benutze `rcases` um das UND in `(h : A ∧ (B ∧ C))` zu zerlegen un rcases h with ⟨_, ⟨g , _⟩⟩ assumption -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => "Du kannst mit `rcases` auch verschachtelt mehrere Strukturen in einem Schritt zerlegen: `rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`." -Hint (A : Prop) (hA : A) : A => +HiddenHint (A : Prop) (hA : A) : A => "Du hast einen Beweis dafür in den *Annahmen*." Tactics constructor assumption @@ -52,24 +52,24 @@ Tactics constructor assumption -- intro -- assumption --- Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => +-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => -- "`↔` oder `∧` im Goal kann man mit `constructor` zerlegen." --- Message (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => +-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => -- "Hier würdest du mit `intro` die Implikation angehen. -- (Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf -- das UND in der Implikationsannahme)" -- -- if they don't use `intro ⟨_, _⟩`. --- Message (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => +-- Hint (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => -- "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen." --- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => +-- HiddenHint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => -- "Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?" -- -- Rückrichtung --- Message (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => -- "Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$ -- Da hilft `intro`. @@ -79,16 +79,16 @@ Tactics constructor assumption -- -- if they don't use `intro ⟨_, _⟩`. --- Message (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => -- "Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen." --- Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => +-- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => -- "Wieder in Einzelteile zerlegen..." --- Message (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => +-- Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => -- "Immer das gleiche ... noch mehr zerlegen." --- -- Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => +-- -- Hint (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => -- -- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen, -- -- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`). diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index e088bbb..59a4e53 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -24,10 +24,10 @@ Statement left assumption -Hint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) => +HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) => "Entscheide dich, `right` oder `left`?" -Message (A : Prop) (B : Prop) (hA : A) : ¬ B => +Hint (A : Prop) (B : Prop) (hA : A) : ¬ B => "Sackgasse. Probier's nochmals." Tactics left right assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index 3e3e04a..8bbb033 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -38,10 +38,10 @@ Statement rcases h with ⟨h₁, h₂⟩ assumption -Hint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A => +HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A => "Als erstes kannst du das ODER in den Annahmen mit `rcases h with h | h` zerlegen." -Message (A : Prop) (B : Prop) (h : A ∧ B) : A => +Hint (A : Prop) (B : Prop) (h : A ∧ B) : A => "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen." Tactics assumption rcases diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index 7fc3e10..d0342bf 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -95,31 +95,31 @@ $(A \\lor B) \\land (A \\lor C)$ wahr ist." right assumption -Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => "Das `∧` im Goal kann mit `constructor` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." -Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) => +HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." --- TODO: Message nur Anhand der Annahmen? +-- TODO: Hint nur Anhand der Annahmen? -Hint (A : Prop) (B : Prop) : A ∨ B => +HiddenHint (A : Prop) (B : Prop) : A ∨ B => "`left` oder `right`?" Tactics left right assumption constructor rcases rfl contradiction trivial