# Zulip Chat Archive

## 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`

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

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

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

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`

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

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

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

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

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

context!

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

I think I gave all the statements needed?

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

ask your question as a MWE

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

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