## Stream: maths

### Topic: proposition manipulation

#### Nicholas McConnell (Feb 23 2020 at 04:55):

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 (Feb 23 2020 at 05:15):

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 (Feb 23 2020 at 08:05):

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 (Feb 23 2020 at 17:27):

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 (Feb 23 2020 at 17:40):

rofl I stand corrected

#### Patrick Massot (Feb 23 2020 at 17:56):

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

#### Nicholas McConnell (Feb 24 2020 at 02:38):

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 (Feb 24 2020 at 02:39):

or.intro_left?

#### Mario Carneiro (Feb 24 2020 at 02:40):

or just or.inl

#### Nicholas McConnell (Feb 24 2020 at 02:40):

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

#### Mario Carneiro (Feb 24 2020 at 02:40):

or left

#### Bryan Gin-ge Chen (Feb 24 2020 at 02:40):

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

#### Mario Carneiro (Feb 24 2020 at 02:42):

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 (Feb 24 2020 at 02:49):

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 (Feb 24 2020 at 02:53):

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

#### Nicholas McConnell (Feb 24 2020 at 02:54):

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 (Feb 24 2020 at 02:54):

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

#### Mario Carneiro (Feb 24 2020 at 02:55):

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

#### Mario Carneiro (Feb 24 2020 at 02:56):

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

#### Nicholas McConnell (Feb 24 2020 at 02:57):

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

#### Mario Carneiro (Feb 24 2020 at 02:58):

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 (Feb 24 2020 at 02:59):

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

#### Nicholas McConnell (Feb 24 2020 at 03:00):

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 (Feb 24 2020 at 03:03):

don't use have to introduce functions, use let

Okay...

#### Mario Carneiro (Feb 24 2020 at 03:04):

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 (Feb 24 2020 at 03:04):

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

#### Nicholas McConnell (Feb 24 2020 at 03:04):

Hmm... what are their names?

#### Mario Carneiro (Feb 24 2020 at 03:05):

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

#### Mario Carneiro (Feb 24 2020 at 03:06):

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

Alright...

#### Nicholas McConnell (Feb 24 2020 at 03:09):

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 (Feb 24 2020 at 03:09):

use set instead of let

Oh okay

#### Mario Carneiro (Feb 24 2020 at 03:09):

you don't need let for theorems like dx

#### Mario Carneiro (Feb 24 2020 at 03:09):

just d

#### Mario Carneiro (Feb 24 2020 at 03:10):

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

#### Nicholas McConnell (Feb 24 2020 at 03:10):

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

#### Mario Carneiro (Feb 24 2020 at 03:11):

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

#### Mario Carneiro (Feb 24 2020 at 03:11):

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

Ah okay thanks

#### Mario Carneiro (Feb 24 2020 at 03:11):

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

#### Mario Carneiro (Feb 24 2020 at 03:13):

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

#### Mario Carneiro (Feb 24 2020 at 03:14):

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 (Feb 24 2020 at 03:19):

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 (Feb 24 2020 at 03:21):

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 (Feb 24 2020 at 03:40):

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


context!

#### Nicholas McConnell (Feb 24 2020 at 03:42):

I think I gave all the statements needed?

MWE?

#### Mario Carneiro (Feb 24 2020 at 03:43):

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

#### Mario Carneiro (Feb 24 2020 at 03:44):

notice that my code post above starts with import and stuff

Last updated: May 18 2021 at 08:14 UTC