rename message to hint
This commit is contained in:
Alexander Bentkamp
@@ -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<string>()
|
||||
const [goals, setGoals] = useState<any[]>(null)
|
||||
const [completed, setCompleted] = useState<boolean>(false)
|
||||
const [diagnostics, setDiagnostics] = useState<any[]>(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<any[]>(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 (<div>
|
||||
<TacticState goals={goals} diagnostics={diagnostics} completed={completed}
|
||||
globalDiagnostics={globalDiagnostics}></TacticState>
|
||||
</div>)
|
||||
}
|
||||
|
||||
export default Infoview
|
||||
|
||||
const useEditorUri = (editor: monaco.editor.IStandaloneCodeEditor) => {
|
||||
const [uri, setUri] = useState<string>(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}
|
||||
}
|
||||
@@ -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';
|
||||
|
||||
@@ -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 (
|
||||
<Box sx={{ pl: 2 }}>
|
||||
{hasObject && <Box><Typography>Objects</Typography>
|
||||
<List>
|
||||
{goal.objects.map((item, index) =>
|
||||
<ListItem key={index}>
|
||||
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
|
||||
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
|
||||
</ListItem>)}
|
||||
</List></Box>}
|
||||
{hasAssumption && <Box><Typography>Assumptions</Typography>
|
||||
<List>
|
||||
{goal.assumptions.map((item, index) => <ListItem key={index}><Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
|
||||
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography></ListItem>)}
|
||||
</List></Box>}
|
||||
<Typography>Prove:</Typography>
|
||||
<Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
|
||||
{openMessages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><Markdown>{message.message}</Markdown></Alert>)}
|
||||
{hasHints &&
|
||||
<FormControlLabel
|
||||
control={<Switch checked={showHints} onChange={handleHintsChange} />}
|
||||
label="More Help?"
|
||||
/>}
|
||||
{hints.map((hint, index) => <Collapse key={index} in={showHints}><Alert severity="info" sx={{ mt: 1 }}><Markdown>{hint.message}</Markdown></Alert></Collapse>)}
|
||||
</Box>)
|
||||
}
|
||||
|
||||
/* 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 (
|
||||
<Accordion>
|
||||
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
|
||||
<Typography color="primary" sx={{ ml: 0 }}>⊢ {goal.goal}</Typography>
|
||||
</AccordionSummary>
|
||||
<AccordionDetails sx={{ backgroundColor: "aliceblue" }}>
|
||||
{hasObject &&
|
||||
<Box>
|
||||
<Typography>Objects</Typography>
|
||||
<List>
|
||||
{goal.objects.map((item, index) =>
|
||||
<ListItem key={index}>
|
||||
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
|
||||
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
|
||||
</ListItem>)}
|
||||
</List>
|
||||
</Box>}
|
||||
{hasAssumption &&
|
||||
<Box>
|
||||
<Typography>Assumptions</Typography>
|
||||
<List>
|
||||
{goal.assumptions.map((item, index) =>
|
||||
<ListItem key={index}>
|
||||
<Typography color="primary" sx={{ mr: 1 }}>{item.userName}</Typography> :
|
||||
<Typography color="secondary" sx={{ ml: 1 }}>{item.type}</Typography>
|
||||
</ListItem>)}
|
||||
</List>
|
||||
</Box>}
|
||||
<Typography>Prove:</Typography>
|
||||
<Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
|
||||
</AccordionDetails>
|
||||
</Accordion>)
|
||||
}
|
||||
|
||||
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 (
|
||||
<Box sx={{ height: "100%" }}>
|
||||
{completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
|
||||
{hasGoal &&
|
||||
<Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
|
||||
<Typography variant="h5">Main Goal
|
||||
(at <FontAwesomeIcon icon={faArrowPointer}></FontAwesomeIcon>)
|
||||
</Typography>
|
||||
<Goal goal={goals[0]} />
|
||||
</Paper>}
|
||||
{isLoading && <CircularProgress />}
|
||||
{!(hasGoal || completed || isLoading) &&
|
||||
<Typography variant="h6">
|
||||
No goals
|
||||
(at <FontAwesomeIcon icon={faArrowPointer}></FontAwesomeIcon>)
|
||||
</Typography>}
|
||||
{hasError &&
|
||||
<Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}>
|
||||
<Typography variant="h5" sx={{ mb: 2 }}>Lean says</Typography>
|
||||
{diagnostics.map(({severity, message}, index) =>
|
||||
<Alert key={index} severity={{1: "error", 2:"warning", 3:"info", 4:"success"}[severity]} sx={{ mt: 1 }}>{message}</Alert>
|
||||
// TODO: When does Lean give severity=4? Had colour `gray` before. Make custom theme for that
|
||||
)}
|
||||
</Paper>}
|
||||
{hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
|
||||
<Typography variant="h5" sx={{ mb: 2 }}>Further Goals</Typography>
|
||||
{goals.slice(1).map((goal, index) => <Paper><OtherGoal key={index} goal={goal} /></Paper>)}
|
||||
</Paper>}
|
||||
</Box>
|
||||
)
|
||||
}
|
||||
|
||||
export default TacticState
|
||||
@@ -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) => <div>{m.message}</div>)
|
||||
const hints = goal.hints.map((m) => <div>{m.text}</div>)
|
||||
|
||||
if (goal.goal.userName) {
|
||||
return <details open className={cn}>
|
||||
|
||||
@@ -121,7 +121,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
|
||||
{goals && <Goals filter={{ reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }} key='goals' goals={goals} />}
|
||||
</LocationsContext.Provider>
|
||||
<FilteredGoals headerChildren='Expected type' key='term-goal'
|
||||
goals={termGoal !== undefined ? {goals: [{goal:termGoal, messages: []}]} : undefined} />
|
||||
goals={termGoal !== undefined ? {goals: [{goal:termGoal, hints: []}]} : undefined} />
|
||||
{userWidgets.map(widget =>
|
||||
<details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
|
||||
<summary className='mv2 pointer'>{widget.name}</summary>
|
||||
|
||||
@@ -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 {
|
||||
|
||||
@@ -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
|
||||
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 {
|
||||
goal := g,
|
||||
intros := decls.size,
|
||||
message := 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.
|
||||
-/
|
||||
/-- 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,
|
||||
spoiler := true,
|
||||
message := msg.getString }}
|
||||
text := msg.getString }}
|
||||
|
||||
/--
|
||||
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'" 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 hints := level.hints.push {
|
||||
goal := g,
|
||||
intros := decls.size,
|
||||
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.
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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`.\"
|
||||
|
||||
|
||||
@@ -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 :
|
||||
|
||||
@@ -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`."
|
||||
|
||||
|
||||
|
||||
@@ -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) =>
|
||||
""
|
||||
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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 ...`"
|
||||
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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."
|
||||
|
||||
|
||||
@@ -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."
|
||||
|
||||
|
||||
@@ -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."
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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..."
|
||||
|
||||
|
||||
|
||||
@@ -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."
|
||||
|
||||
@@ -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."
|
||||
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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..."
|
||||
|
||||
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
|
||||
"`left` oder `right`?"
|
||||
|
||||
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B) (hA : A) : B ∨ (C ∧ A) =>
|
||||
"`left` oder `right`?"
|
||||
|
||||
Hint (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) =>
|
||||
"`left` oder `right`?"
|
||||
|
||||
Message (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
|
||||
|
||||
@@ -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 : ℕ) → `"
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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..."
|
||||
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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 ""
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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 : ℕ) → `"
|
||||
|
||||
|
||||
@@ -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 ""
|
||||
|
||||
|
||||
@@ -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\"."
|
||||
|
||||
@@ -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."
|
||||
|
||||
|
||||
|
||||
@@ -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 ""
|
||||
|
||||
@@ -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."
|
||||
|
||||
|
||||
@@ -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)`).
|
||||
|
||||
|
||||
@@ -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)`).
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user