proposition manipulation

Stream: maths

[Nicholas McConnell]

2 goals
p q : Prop,
f : ¬(p ∧ q)
⊢ ¬p ∨ ¬q

In an attempt to prove De Morgan's laws in logic, I got here. But I'm not sure how to continue. f is a negation so I can't use "split", and "by_cases p1 : p ∧ q" doesn't work because p ∧ q appears to have "undecidable type"

[Bryan Gin-ge Chen]

You need to use classical.prop_decidable (if you're importing mathlib, you can also write open_locale classical near the start of your file):

local attribute [instance] classical.prop_decidable

example (p q : Prop) (f : ¬(p ∧ q))
: ¬p ∨ ¬q :=
begin
  by_cases hp : p,
  { by_cases hq : q,
    { exact (f ⟨hp, hq⟩).elim, },
    exact or.inr hq, },
  { exact or.inl hp, },
end

[Kevin Buzzard]

All the intro, split, apply, cases stuff will only solve goals in constructive logic, which is weaker than classical logic. A random statement which is true in classical logic has like a 50% chance of being true constructively and if it isn't then you can just do a case split on whether something is true or false, which is exactly the law of the excluded middle

[Bryan Gin-ge Chen]

A random statement which is true in classical logic has like a 50% chance of being true constructively

I got curious about this and did a little digging. Here's one paper on the topic: "In the full propositional logic, 5/8 of classical tautologies are intuitionistically valid" by Genitrini and Kozik.

[Kevin Buzzard]

rofl I stand corrected

[Patrick Massot]

We are discussing statistics and you were within 40% of the correct answer, there is no problem at all.

[Nicholas McConnell]

Is there a Lean command (such as or.assoc for a∨(b∨c)=(a∨b)∨c) to get the addition law, p implies p∨q?

[Alex J. Best]

or.intro_left?

[Mario Carneiro]

or just or.inl

[Nicholas McConnell]

Thanks. Bear with me, there are tons of commands I don't know

[Mario Carneiro]

or left

[Bryan Gin-ge Chen]

If you're in tactic mode, left will change a goal like p∨q to p.

[Mario Carneiro]

Technically, or.inl isn't a command, it's a theorem. There are tens of thousands of them and probably no one knows the whole list so you shouldn't be ashamed to not know one. It is good to know how to find them though

[Nicholas McConnell]

And just out of curiosity, are there Lean lemmas of this form?

lemma not_all_eq_ex_not (t : Type) (p : t → Prop) :
  ¬(∀(x:t), p(x)) ↔ ∃(x:t), ¬p(x) :=
begin
sorry
end

lemma not_ex_eq_all_not (t : Type) (p : t → Prop) :
  ¬(∃(x:t), p(x)) ↔ ∀(x:t), ¬p(x) :=
begin
sorry
end

Because I think they'd be useful to prove the well-ordering principle:

lemma WOP (pr : ℕ → Prop) (he : ∃(x:ℕ),(pr(x))) :
  ∃(m:ℕ),(pr(m) ∧ ∀(n:ℕ),(pr(n) → n ≥ m)) :=
begin
sorry
end

[Bryan Gin-ge Chen]

Those are not_forall and not_exists in mathlib's logic.basic, respectively.

[Nicholas McConnell]

Okay, thanks. I already wrote my own De Morgan's Laws lemmas for finite conjunctions and disjunctions (with some of your help), so I wonder if Lean has them builtin

[Mario Carneiro]

and what you are calling the well ordering principle is nat.find and its lemmas

[Mario Carneiro]

We usually represent finite conjunctions by iterating and, and there are de morgan's laws for them, also in logic.basic

[Mario Carneiro]

In fact, you should just browse through the file to get an idea of what to expect

[Nicholas McConnell]

Okay, maybe I'll put my useless lemmas in another file XD

[Mario Carneiro]

Generally, you will get a feel for what "should be in mathlib", which is to say, it either already exists and so you should find it, or it doesn't exist and you should PR it

[Mario Carneiro]

any logical manipulation involving 3 or fewer variables should already be proven

[Nicholas McConnell]

Anyway, I tried using nat.find:

lemma bezout (a p : ℕ) (hp : prime p) (ha : ¬(divides p a)) :
  ∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1 hp2,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh := LCex a p p_pos,
have dm := nat.find(dh),
-- ...
end

and now the hypotheses state dm is a natural number, but I don't see any assertion that it satisfies dh's condition or any assertion that nothing smaller does:

1 goal
a p : ℕ,
ha : ¬divides p a,
hp1 : 1 < p,
hp2 : ∀ (k : ℕ), divides k p → k = 1 ∨ k = p,
zero_lt_one : 0 < 1,
p_pos : 0 < p,
dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d,
dm : ℕ
⊢ ∃ (x y : ℤ), x * ↑a + y * ↑p = 1

[Mario Carneiro]

don't use have to introduce functions, use let

[Nicholas McConnell]

Okay...

[Mario Carneiro]

There is a definition called nat.find, a theorem saying that P (nat.find h) holds, and another theorem saying that nothing smaller than nat.find h satisfies P

[Mario Carneiro]

it's not in the context, it's just a global theorem about nat.find

[Nicholas McConnell]

Hmm... what are their names?

[Mario Carneiro]

nat.find_spec maybe? grep / find in files is your friend

[Mario Carneiro]

nat.find_spec says nat.find satisfies P, and nat.find_min or nat.find_min' say that nothing smaller does

[Nicholas McConnell]

Alright...

[Nicholas McConnell]

d : ℕ := nat.find dh,
dx : 0 < nat.find dh ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑(nat.find dh) := nat.find_spec dh
⊢ ∃ (x y : ℤ), x * ↑a + y * ↑p = 1

Is there a way to replace "nat.find dh" with "d" throughout, given this? rw doesn't work

[Mario Carneiro]

use set instead of let

[Nicholas McConnell]

Oh okay

[Mario Carneiro]

you don't need let for theorems like dx

[Mario Carneiro]

just d

[Mario Carneiro]

because you want to retain the knowledge of what it is defined to be so you can assert additional facts about it

[Nicholas McConnell]

Okay, done that but "rw d at dx" still doesn't work

[Mario Carneiro]

set should replace any instances of the let body in the current goal with the variable

[Mario Carneiro]

dsimp can be used to unfold a let but not to re-fold one

[Nicholas McConnell]

Ah okay thanks

[Mario Carneiro]

I think set has an option to give you an equality as well, which can be used with rw

[Mario Carneiro]

What I would probably do in this case is just state the theorem the way you want it to be stated

[Mario Carneiro]

import data.nat.prime
open nat
open_locale classical

lemma bezout (a p : ℕ) (hp : prime p) (ha : ¬(p ∣ a)) :
  ∃(x:ℤ), (∃(y:ℤ), (x*a + y*p = 1)) :=
begin
rw prime at hp,
cases hp with hp1 hp2,
have zero_lt_one := nat.lt_succ_self 0,
have p_pos := lt_trans zero_lt_one hp1,
have dh : ∃ (d : ℕ), 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := sorry,
let d := nat.find(dh),
have dx : 0 < d ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d := nat.find_spec dh
have dm : ∀ d', (0 < d' ∧ ∃ (x y : ℤ), x * ↑a + y * ↑p = ↑d') → d ≤ d' := λ d', nat.find_min' dh,
-- ...
end

[Bryan Gin-ge Chen]

As an additional stylistic point, specifying the expected types in your have statements makes proofs much easier to read. It also helps if you have to fix the code later on e.g. if you change other parts of the code or if mathlib changes.

[Mario Carneiro]

or if, for instance, you post a code snippet lacking the context to interpret a line like have dh := LCex a p p_pos,. I reverse engineered the statement from your later post about the goal

[Nicholas McConnell]

How can I prove this goal? (norm_cast doesn't work or at least not so easily, because x_ex and y_ex are integers which have great chances of being negative)

hq1 : a = d * q + r,
hy : x_ex * ↑(d * q + r) + y_ex * ↑p = ↑d
⊢ ↑(d * q + r) - x_ex * ↑q * ↑(d * q + r) - y_ex * ↑q * ↑p = ↑r

[Mario Carneiro]

context!

[Nicholas McConnell]

I think I gave all the statements needed?

[Mario Carneiro]

ask your question as a MWE

[Nicholas McConnell]

MWE?

[Mario Carneiro]

a minimum working example, i.e. a self contained file with the beginning of a proof

[Mario Carneiro]

notice that my code post above starts with import and stuff