## Stream: new members

### Topic: Showing a strict relation is incomplete.

#### Greg Leo (May 05 2022 at 20:16):

Hello all, I am trying to learn lean by working on some binary relations.

I have defined a strict relation like this:
def S (a b : A) : Prop := R a b ∧ ¬ R b a

I was able to prove that S is irreflexive.

/- The Strict Relation is Irreflexive -/
theorem irreflS : irreflexive S :=
begin
assume x, --add object x to the context
assume sxx : S x x, --assume the opposite to derive a contradsiction
have nrxx : ¬ R x x, from and.right sxx, --get the ¬ x≿x from the definition of ≻
have rxx : R x x, from and.left sxx, --get the x≿x from the definition of ≻
show false, from nrxx rxx, --show the contradiction
end


I am having trouble starting on proving that the relation is incomplete, which I have defined this way:

def incomplete (R : A → A → Prop) : Prop :=
∃ x y, ¬ (R x y ∨ R y x)


I want to prove this by showing that ¬ S x x but I can't seem to introduce x. Is my issue that I have not defined what set these relations are on so that there might not be such an x?

Here is my complete code:

#### Eric Wieser (May 05 2022 at 20:18):

(note you can use triple #backticks for multiline code)

#### Notification Bot (May 05 2022 at 20:20):

Greg Leo has marked this topic as resolved.

#### Notification Bot (May 05 2022 at 20:20):

Greg Leo has marked this topic as unresolved.

#### Greg Leo (May 05 2022 at 20:21):

Thanks. That looks nicer.

#### Eric Wieser (May 05 2022 at 20:23):

Are you trying to prove incomplete S? It helps if you phrase your question to include the statement you don't know how to prove

#### Greg Leo (May 05 2022 at 20:24):

Yes. I have added my full code to the first message to show where I am. incomplete S is where I can't get started.

#### Eric Wieser (May 05 2022 at 20:25):

   works in spoilers too (but you have to use  spoiler  with four backticks not three; and you have to use  lean  explicitly)

#### Eric Wieser (May 05 2022 at 20:26):

I think your problem is going to be that the statement is false

#### Eric Wieser (May 05 2022 at 20:26):

Consider A = empty

#### Greg Leo (May 05 2022 at 20:27):

Yes, that's sort of what I was suspecting.

#### Greg Leo (May 05 2022 at 20:28):

Ok, I think I was able to restate the theorem.

#### Greg Leo (May 05 2022 at 20:29):

theorem incompS : nonempty A → incomplete S :=
begin
assume x,

end


#### Eric Wieser (May 05 2022 at 20:30):

That would be better written as theorem incompS [nonempty A] : incomplete S

#### Eric Wieser (May 05 2022 at 20:31):

Which tells lean to find a proof that A is nonempty automatically

#### Eric Wieser (May 05 2022 at 20:31):

But the statement looks true either way now

#### Greg Leo (May 05 2022 at 20:39):

I have:

A: Type
R: A → A → Prop
rationalR: rational R
_inst_1: nonempty A
⊢ incomplete S


#### Greg Leo (May 05 2022 at 20:39):

still having trouble introducing that x to the context.

#### Greg Leo (May 05 2022 at 20:40):

Getting now "assume tactic failed, Pi/let expression expected" when I assume x

#### Eric Wieser (May 05 2022 at 20:44):

Probably you want to use tactic#inhabit

Thank you!

#### Greg Leo (May 05 2022 at 21:21):

I have so much to learn.

#### Eric Wieser (May 05 2022 at 21:24):

Your approach with assume x would have worked if you just used A instead of nonempty A, which contains the same content mathematically; it's just less convenient as a lemma

#### Patrick Johnson (May 06 2022 at 03:27):

theorem incompS [nonempty A] : incomplete S :=
begin
inhabit A,
use [default, default],
simp [S],
end


#### Ratmir Mugattarov (May 06 2022 at 08:02):

Hello everyone, I am new to LEAN.
Does anybody know if there are any papers on verification of LEAN itself?
I mean can prove that code of LEAN is correct?
Thank you for any directions

#### Greg Leo (May 06 2022 at 12:35):

Thanks for the tip @Patrick Johnson

#### Greg Leo (May 06 2022 at 13:13):

I tried exactly that:

theorem incompS [nonempty A]: incomplete S :=
begin
inhabit A,
use [default, default],
simp [S],
end


I get this:

failed to instantiate goal with default
state:
A : Type,
R : A → A → Prop,
rationalR : rational R,
_inst_1 : nonempty A,
inst : inhabited A
⊢ incomplete S


#### Patrick Johnson (May 06 2022 at 14:07):

Have you changed the definition of incomplete in the meantime? What error do you get if you replace use [default, default] with refine ⟨default, default, _⟩ ?

#### Yaël Dillies (May 06 2022 at 14:15):

Or maybe refine ⟨⟨default, default, _⟩⟩ ?

#### Greg Leo (May 06 2022 at 14:40):

In both cases a bunch of “invalid expression”, “invalid begin-end expression , expected”

#### Greg Leo (May 06 2022 at 14:41):

I’ll paste in the full thing shortly

#### Greg Leo (May 06 2022 at 14:41):

I haven’t changed the definition. Still the same one from the code in my original post.

#### Patrick Johnson (May 06 2022 at 14:49):

Maybe you are missing import tactic at the beginning of the file (although inhabit would fail in that case). What is your Lean and mathlib version?

#### Greg Leo (May 06 2022 at 15:14):

Have import tactic. Just used elan to update from 3.35.1 to 3.42.1

#### Greg Leo (May 06 2022 at 15:15):

Let me see about updateing mathlib.

#### Greg Leo (May 06 2022 at 15:22):

Ok, upgraded my leanproject to latest mthlib

#### Greg Leo (May 06 2022 at 15:26):

Ok, here's the state of my file.

#### Greg Leo (May 06 2022 at 15:27):

My error:

type mismatch at application
Exists.intro default
term
default
has type
Π (α : Sort ?) [self : inhabited α], α : Sort (imax (?+1) (max 1 ?) ?)
but is expected to have type
A : Type
state:
A : Type,
R : A → A → Prop,
rationalR : rational R,
_inst_1 : nonempty A,
inst : inhabited A
⊢ incomplete S


#### Patrick Johnson (May 06 2022 at 16:36):

Seems like you're still using an outdated version of Lean. The parameter of inhabited.default was changed to implicit in version 3.37, but you still have it explicit. What does #reduce lean.version show?

#### Greg Leo (May 06 2022 at 16:46):

Indeed, it shows an old version.

3 35 1

#### Greg Leo (May 06 2022 at 16:47):

installed toolchains
--------------------

stable (default)
leanprover-community/lean:3.35.1
leanprover-community/lean:3.42.1

active toolchain
----------------

stable (default)


#### Greg Leo (May 06 2022 at 16:47):

That's my elan output

#### Greg Leo (May 06 2022 at 16:50):

Ok I see. I need to change the active toolchain

#### Greg Leo (May 06 2022 at 16:53):

Manually updated that in the .toml

#### Greg Leo (May 06 2022 at 17:03):

having some import issues now

#### Greg Leo (May 06 2022 at 17:04):

import tactic gets me

invalid import: tacti
could not resolve import: tacti


#### Greg Leo (May 06 2022 at 17:04):

import tactic.basic gets me a load of imported file '...' uses sorry

#### Greg Leo (May 06 2022 at 17:08):

Using import tactic and then restarted vs code. Now my infoview is just showing Loading...

#### Greg Leo (May 06 2022 at 17:17):

leanproject upgrade-mathlib seemed to clear that up

Last updated: Dec 20 2023 at 11:08 UTC