|
|
import TestGame.Metadata
|
|
|
import Mathlib
|
|
|
|
|
|
Game "TestGame"
|
|
|
World "Function"
|
|
|
Level 4
|
|
|
|
|
|
Title ""
|
|
|
|
|
|
Introduction
|
|
|
"
|
|
|
Du kommst an eine Tür mit zwei Wächtern. Der eine hat ein Schild
|
|
|
|
|
|
```
|
|
|
def f : ℚ → ℚ := fun x ↦ 5 * x
|
|
|
```
|
|
|
|
|
|
der andere eines mit
|
|
|
|
|
|
```
|
|
|
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
|
|
|
```
|
|
|
|
|
|
Auf der Tür steht groß:
|
|
|
"
|
|
|
|
|
|
example (P : Prop) [Decidable P] (a b : ℕ) (h : P) : ite P a b = a := if_pos h
|
|
|
|
|
|
open Set
|
|
|
|
|
|
namespace LevelFunction4
|
|
|
|
|
|
def f : ℚ → ℚ := fun x ↦ 5 * x
|
|
|
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
|
|
|
|
|
|
|
|
|
-- #eval (f2 + f2) 2
|
|
|
|
|
|
-- #check range f2
|
|
|
|
|
|
Statement ""
|
|
|
: f ∘ g = g ∘ f := by
|
|
|
funext x
|
|
|
simp_rw [Function.comp_apply]
|
|
|
unfold g
|
|
|
by_cases 0 ≤ x
|
|
|
have h' : 0 ≤ f x
|
|
|
unfold f
|
|
|
linarith
|
|
|
rw [if_pos h', if_pos h]
|
|
|
unfold f
|
|
|
ring
|
|
|
have h' : ¬ (0 ≤ f x)
|
|
|
unfold f
|
|
|
linarith
|
|
|
rw [if_neg h, if_neg h']
|
|
|
unfold f
|
|
|
ring
|
|
|
|
|
|
NewTactics funext by_cases simp_rw linarith
|
|
|
|
|
|
NewLemmas not_le if_pos if_neg
|
|
|
|
|
|
|
|
|
Hint : f ∘ g = g ∘ f =>
|
|
|
"
|
|
|
**Robo**: Schau mal, die beiden haben zwei Funktionen, eine davon mit stückweiser Definition.
|
|
|
|
|
|
**Du**: Und ich soll zeigen, dass die beiden vertauschbar sind?
|
|
|
|
|
|
**Robo**: Genau, am besten wählst du mit `funext x` ein beliebiges Element aus, und zeigst das
|
|
|
dann für dieses.
|
|
|
"
|
|
|
|
|
|
-- TODO: These 5 hints should be mutually exclusive. i.e. they should not trigger
|
|
|
-- if a assumption is missing.
|
|
|
Hint (x : ℚ) : (f ∘ g) x = (g ∘ f) x =>
|
|
|
"
|
|
|
**Du**: Ah und jetzt kann ich erst einmal `(g ∘ f) {x}` zu `g (f {x})` umschreiben?
|
|
|
|
|
|
**Robo**: Mit `simp_rw` geht das übrigens schneller.
|
|
|
|
|
|
**Robo**: Und danach willst du eien Fallunterscheidung
|
|
|
machen, `by_cases h : 0 ≤ {x}`.
|
|
|
|
|
|
**Du**: Damit krieg ich die Fälle `0 ≤ {x}` und `{x} < 0`?
|
|
|
|
|
|
**Robo**: Genau! Oder präziser `0 ≤ {x}` und `¬(0 ≤ {x})`. Das ist nicht ganz das gleiche, und man
|
|
|
könnte mit dem Lemma `not_le` zwischen `¬(0 ≤ {x})` und `0 < {x}` wechseln.
|
|
|
"
|
|
|
|
|
|
Hint (x : ℚ) (h : 0 ≤ x) : f (g x) = g (f x) =>
|
|
|
"
|
|
|
**Robo**: Um das ausrechnen zu können, brauchst du nicht nur `0 ≤ x` sondern auch noch
|
|
|
eine Annahme `0 ≤ f x`.
|
|
|
"
|
|
|
|
|
|
Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = g (f x) =>
|
|
|
"
|
|
|
**Du**: Mit den beiden Annahmen habe ich ja jetzt `(if 0 ≤ x then _)` wobei `0 ≤ x` wahr ist,
|
|
|
kann ich das dann einfach vereinfachen?
|
|
|
|
|
|
**Robo**: Dafür must du zuerst die Definition von `g` öffnen, also `unfold`. Und dann mit
|
|
|
dem Lemma `if_pos {h}` das umschreiben.
|
|
|
"
|
|
|
|
|
|
Hint (x : ℚ) (h : ¬ 0 ≤ x) : f (g x) = g (f x) =>
|
|
|
"
|
|
|
**Du**: Ich sehe, das ist jetzt der zweite Fall, da brauch ich sicher wieder eine zweite Annahme
|
|
|
`¬(0 ≤ f x)`…
|
|
|
"
|
|
|
|
|
|
Hint (x : ℚ) (h : ¬ 0 ≤ x) (h₂ : ¬ 0 ≤ f x) : f (g x) = g (f x) =>
|
|
|
"
|
|
|
**Robo**: Jetzt ist der Zeitpunkt wo die Definition von `g` geöffnet sein sollte.
|
|
|
|
|
|
**Robo**: Wenn man ein If-Statement mit wahrer Prämisse mit `if_pos` vereinfacht, dann
|
|
|
braucht man für eine falsche Prämisse…
|
|
|
|
|
|
**Du**: `if_neg`?
|
|
|
"
|
|
|
-- END TODO
|
|
|
HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = g (f x) =>
|
|
|
"
|
|
|
**Robo**: Jetzt das Gleiche noch mit `if_pos {h₂}`.
|
|
|
"
|
|
|
|
|
|
HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = 2 * f x =>
|
|
|
"
|
|
|
**Robo**: Jetzt das Gleiche noch mit `if_pos {h}`.
|
|
|
"
|
|
|
|
|
|
Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = 2 * f x =>
|
|
|
"
|
|
|
**Robo**: Wenn du jetzt noch die Definition von `f` öffnest, dann kann `ring` den
|
|
|
Rest ausrechnen.
|
|
|
"
|
|
|
|
|
|
|
|
|
-- TODO: This are also showing in the case of the Hint below
|
|
|
-- Proof of `0 ≤ f x`.
|
|
|
Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
|
|
|
" **Robo**: Wenn du die Definition von `f` öffnest, dann hast du schon das wissen,
|
|
|
um das zu beweisen."
|
|
|
HiddenHint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
|
|
|
"**Du** *(in Gedanken)*: Was war das nochmals... Ungleichungen... `linarith`!"
|
|
|
|
|
|
HiddenHint (x : ℚ) (h : ¬0 ≤ x) : ¬ 0 ≤ f x =>
|
|
|
" **Robo**: Das ist das selbe wie vorhin…"
|
|
|
|
|
|
|
|
|
-- Hint for modifying `h` wrongly.
|
|
|
Hint (x : ℚ) (h : x < 0) : f (g x) = g (f x) =>
|
|
|
"
|
|
|
**Robo**: Das war nicht so ideal, hier brauchst du die Annahme in der Form `({h} : ¬ 0 ≤ {x})`!
|
|
|
"
|
|
|
|
|
|
-- TODO: In this case we get to see the Hints above
|
|
|
Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ x =>
|
|
|
"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
|
|
|
geschrieben hast."
|
|
|
|
|
|
Hint (x : ℚ) (h : 0 ≤ f x) : 0 ≤ f x =>
|
|
|
"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
|
|
|
geschrieben hast."
|
|
|
|
|
|
Hint (x : ℚ) (h : ¬ 0 ≤ x) : ¬ 0 ≤ x =>
|
|
|
"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
|
|
|
geschrieben hast."
|
|
|
|
|
|
Hint (x : ℚ) (h : ¬ 0 ≤ f x) : ¬ 0 ≤ f x =>
|
|
|
"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
|
|
|
geschrieben hast."
|
|
|
|
|
|
Conclusion
|
|
|
"Zufrieden tauschen die beiden Wächter ihren Platz und geben so dabei den
|
|
|
Durchgang frei."
|
|
|
|
|
|
end LevelFunction4
|