Natural Number Game in Verso

8. ≀ WorldπŸ”—

In this world we define a ≀ b and prove standard facts about it, such as "if a ≀ b and b ≀ c then a ≀ c."

The definition of a ≀ b is "there exists a number c such that b = a + c. " So we're going to have to learn a tactic to prove "exists" theorems, and another one to use "exists" hypotheses.

Click on "Start" to proceed.

8.1.Β Level 1: The use tacticπŸ”—

a ≀ b is notation for βˆƒ c, b = a + c. This "backwards E" means "there exists". So a ≀ b means that there exists a number c such that b = a + c. This definition works because there are no negative numbers in this game.

To prove an "exists" statement, use the use tactic. Let's see an example.

If x is a number, then x \le x.

New: use

Summary

The use tactic makes progress with goals which claim something exists. If the goal claims that some x exists with some property, and you know that x = 37 will work, then use 37 will make progress.

Because a ≀ b is notation for "there exists c such that b = a + c", you can make progress on goals of the form a ≀ b by useing the number which is morally b - a (i.e. use b - a)

Any of the following examples is possible assuming the type of the argument passed to the use function is accurate:

  • use 37

  • use a

  • use a * a + 1

New: ≀

a ≀ b is notation for βˆƒ c, b = a + c.

Because this game doesn't have negative numbers, this definition is mathematically valid.

This means that if you have a goal of the form a ≀ b you can make progress with the use tactic, and if you have a hypothesis h : a ≀ b, you can make progress with cases h with c hc.

theorem le_refl (x : β„•) : x ≀ x
Tactics
Theorems
Symbols

8.2.Β Level 2: 0 ≀ xπŸ”—

To solve this level, you need to use a number c such that x = 0 + c.

If x is a number, then 0 \le x.

theorem zero_le (x : β„•) : 0 ≀ x
Tactics
Theorems
Symbols

8.3.Β Level 3: x ≀ succ xπŸ”—

If you use the wrong number, you get stuck with a goal you can't prove. What number will you use here?

If x is a number, then x \le \operatorname{succ}(x).

theorem le_succ_self (x : β„•) : x ≀ succ x
Tactics
Theorems
Symbols

8.4.Β Level 4: x ≀ y and y ≀ z implies x ≀ zπŸ”—

In this level, we see inequalities as hypotheses. We have not seen this before. The cases tactic can be used to take hxy apart.

If x \leq y and y \leq z, then x \leq z.

theorem le_trans (x y z : β„•) (hxy : x ≀ y) (hyz : y ≀ z) : x ≀ z
Tactics
Theorems
Symbols

8.5.Β Level 5: x ≀ 0 β†’ x = 0πŸ”—

It's "intuitively obvious" that there are no numbers less than zero, but to prove it you will need a result which you showed in advanced addition world.

If x \leq 0, then x=0.

theorem le_zero (x : β„•) (hx : x ≀ 0) : x = 0
Tactics
Theorems
Symbols

8.6.Β Level 6: x ≀ y and y ≀ x implies x = yπŸ”—

This level asks you to prove antisymmetry of \leq. In other words, if x \leq y and y \leq x then x = y. It's the trickiest one so far. Good luck!

If x \leq y and y \leq x, then x = y.

theorem le_antisymm (x y : β„•) (hxy : x ≀ y) (hyx : y ≀ x) : x = y
Tactics
Theorems
Symbols

8.7.Β Level 7: Dealing with orπŸ”—

Totality of ≀ is the boss level of this world, and it's coming up next. It says that if a and b are naturals then either a ≀ b or b ≀ a. But we haven't talked about or at all. Here's a run-through.

  1. The notation for "or" is ∨. You won't need to type it, but you can type it with \or.

  2. If you have an "or" statement in the goal, then two tactics make progress: left and right. But don't choose a direction unless your hypotheses guarantee that it's the correct one.

  3. If you have an "or" statement as a hypothesis h, then cases h with h1 h2 will create two goals, one where you went left, and the other where you went right.

If x=37 or y=42, then y=42 or x=37.

New: left

Summary

The left tactic changes a goal of P ∨ Q into a goal of P. Use it when your hypotheses guarantee that the reason that P ∨ Q is true is because in fact P is true.

Internally this tactic is just applying a theorem saying that P \implies P \lor Q.

Note that this tactic can turn a solvable goal into an unsolvable one.

New: right

Summary

The right tactic changes a goal of P ∨ Q into a goal of Q. Use it when your hypotheses guarantee that the reason that P ∨ Q is true is because in fact Q is true.

Internally this tactic is just applying a theorem saying that Q \implies P \lor Q.

Note that this tactic can turn a solvable goal into an unsolvable one.

example (x y : β„•) (h : x = 37 ∨ y = 42) : y = 42 ∨ x = 37
Tactics
Theorems
Symbols

8.8.Β Level 8: x ≀ y or y ≀ xπŸ”—

This is I think the toughest level yet. Tips: if a is a number then cases a with b will split into cases a = 0 and a = succ b. And don't go left or right until your hypotheses guarantee that you can prove the resulting goal!

I've left hidden hints; if you need them, retry from the beginning and click on "Show more help!"

If x and y are numbers, then either x \leq y or y \leq x.

theorem le_total (x y : β„•) : x ≀ y ∨ y ≀ x
Tactics
Theorems
Symbols

8.9.Β Level 9: succ x ≀ succ y β†’ x ≀ yπŸ”—

We've proved that x ≀ 0 implies x = 0. The last two levels in this world will prove which numbers are ≀ 1 and ≀ 2. This lemma will be helpful for them.

If \operatorname{succ}(x) \leq \operatorname{succ}(y) then x \leq y.

theorem succ_le_succ (x y : β„•) (hx : succ x ≀ succ y) : x ≀ y
Tactics
Theorems
Symbols

8.10.Β Level 10: x ≀ 1πŸ”—

We've seen le_zero, the proof that if x ≀ 0 then x = 0. Now we'll prove that if x ≀ 1 then x = 0 or x = 1.

If x \leq 1 then either x = 0 or x = 1.

theorem le_one (x : β„•) (hx : x ≀ 1) : x = 0 ∨ x = 1
Tactics
Theorems
Symbols

8.11.Β Level 11: le_twoπŸ”—

We'll need this lemma to prove that two is prime!

You'll need to know that ∨ is right associative. This means that x = 0 ∨ x = 1 ∨ x = 2 actually means x = 0 ∨ (x = 1 ∨ x = 2). This affects how left and right work.

If x \leq 2 then x = 0 or 1 or 2.

theorem le_two (x : β„•) (hx : x ≀ 2) : x = 0 ∨ x = 1 ∨ x = 2
Tactics
Theorems
Symbols