natural number game

Stream: new members

[RexWang]

Hey guys! I'm new to the lean-community and hope this is the right way to ask questions.

I'm starting to learn Lean by the excellent tutorial natural_number_game, and I would like to do it locally since the website doesn't keep my progress sometimes.

Also, I find a GitHub-repo for the game, but fails to import the library in my machine. I'm wondering if there is a way to do it properly.


Thanks in advance!

[Alex J. Best]

You need to use the "Open folder" option in vscode to open the folder "natural_number_game".

Also its easier to keep things organised if you make a new thread for your question in future :smile:

[RexWang]

Alex J. Best 发言道：

You need to use the "Open folder" option in vscode to open the folder "natural_number_game".

Also its easier to keep things organised if you make a new thread for your question in future :)

Thanks a lot! I just noticed the post tags on Zulip.

[Notification Bot]

3 messages were moved here from #new members > Contributing to mathlib by Johan Commelin.

[Notification Bot]

RexWang has marked this topic as resolved.

[Notification Bot]

RexWang has marked this topic as unresolved.

[RexWang]

The last question in the Advanced Proposition world has left me confused.

contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q)

The hint suggests using a black box strategy cc. But in the previous six worlds, a pattern of axioms + reasoning was used, which makes this step difficult for me to accept. Is there a handwritten solution to this problem?

---

If I understand correctly, the tactic exfalso and by_cases are equivalent to introducing the following axioms to express the principle of contradiction:

false → P
Q → P ∨ (P → false)

Is it possible to reason about this problem based on these axioms, or by introducing more axioms, rather than using the cc strategy?

[Mario Carneiro]

(by_cases is actually equivalent to just P ∨ (P → false), a theorem available under the name em for excluded middle)

[Mario Carneiro]

Yes you can prove it with just em and basic logic. Hint: do cases on Q

[RexWang]

Mario Carneiro 发言道：

Yes you can prove it with just em and basic logic. Hint: do cases on Q

Thank you very much! Here might be a proof(incomplete).

lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
begin
  intros f p, -- skip to claim an element of Q
  by_cases q: Q, -- divide into two goals: Q is true or false
  -- if Q is true than P → Q is trivial
  exact q,
  -- if Q is not true, i.e. ∃ q ∈ ¬Q
  -- we work on the left side of the prop. P → Q
  have np := f(q), -- fq : ¬P
  -- get an element of ¬P, so ¬P is true
  -- it remains to prove ¬P ∧ P → Q
  have pnp : P ∧ ¬P, -- we first construct ¬P ∧ P
    split,
    exact p,
    exact np,
  -- a lemma before, we know that ¬P ∧ P → false
  apply contra P,
  exact pnp,
end

But I got stuck at the last step: how can I apply the lemma to reduce the question? Thanks again for the suggestion!

-- previous lemma
lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q
begin
-- use axiom false → any, by exfalso
rw not_iff_imp_false,
intro h,
cases h with p np,
have f : false := np(p),
exfalso,
apply f,
end

[Mario Carneiro]

Note that if np : ¬P and p : P then np p : false

[Mario Carneiro]

so exfalso should close the gap

[Notification Bot]

This topic was moved here from #Lean for teaching > natural number game by Heather Macbeth.