Showing a strict relation is incomplete.

Stream: new members

[Greg Leo]

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:

section

parameters {A : Type} {R : A → A → Prop}

/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x

/- Defininig Complete Relations -/
def incomplete (R : A → A → Prop) : Prop :=
∃ x y, ¬ (R x y ∨ R y x)

def rational (R : A → A → Prop) : Prop :=
complete R ∧ reflexive R ∧ transitive R

/- R is a relexive, complete, transitive relation -/
parameter (rationalR : rational R)

/- Defininig S the Strict Preference Relation-/
def S (a b : A) : Prop := R a b ∧ ¬ R b a

/-###################################-/
/- Properties of the Strict Relation-/
/-#################################-/

/- Include the preference relations properties in proofs. -/
include rationalR

/- 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

/- The Strict Relation is Incomplete -/
theorem incompS : incomplete S :=
begin
assume x,       /-Now I'm lost -/

end

end

[Eric Wieser]

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

[Notification Bot]

Greg Leo has marked this topic as resolved.

[Notification Bot]

Greg Leo has marked this topic as unresolved.

[Greg Leo]

Thanks. That looks nicer.

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Consider A = empty

[Greg Leo]

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

[Greg Leo]

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

[Greg Leo]

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



end

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

But the statement looks true either way now

[Greg Leo]

Ok, I have changed it to your way. I will have to read about that.

[Greg Leo]

I have:

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

[Greg Leo]

still having trouble introducing that x to the context.

[Greg Leo]

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

[Eric Wieser]

Probably you want to use tactic#inhabit

[Greg Leo]

Thank you!

[Greg Leo]

I have so much to learn.

[Eric Wieser]

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]

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

[Ratmir Mugattarov]

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]

Thanks for the tip @Patrick Johnson

[Greg Leo]

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]

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]

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

[Greg Leo]

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

[Greg Leo]

I’ll paste in the full thing shortly

[Greg Leo]

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

[Patrick Johnson]

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]

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

[Greg Leo]

Let me see about updateing mathlib.

[Greg Leo]

Ok, upgraded my leanproject to latest mthlib

[Greg Leo]

Ok, here's the state of my file.

import tactic

section

parameters {A : Type} {R : A → A → Prop}

/- Defininig Complete Relations -/
def complete (R : A → A → Prop) : Prop :=
∀ x y, R x y ∨ R y x

/- Defininig Complete Relations -/
def incomplete (R : A → A → Prop) : Prop :=
∃ x y, ¬ (R x y ∨ R y x)

def rational (R : A → A → Prop) : Prop :=
complete R ∧ reflexive R ∧ transitive R

/- R is a relexive, complete, transitive relation -/
parameter (rationalR : rational R)

/- Defininig S the Strict Preference Relation-/
def S (a b : A) : Prop := R a b ∧ ¬ R b a

/-###################################-/
/- Properties of the Strict Relation-/
/-#################################-/

/- Include the preference relations properties in proofs. -/
include rationalR

/- 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

/- The Strict Relation is Incomplete -/
theorem incompS [nonempty A]: incomplete S :=
begin
inhabit A,
refine ⟨default, default, _⟩,
simp [S],
end



end

[Greg Leo]

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]

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]

Indeed, it shows an old version.

[Greg Leo]

3 35 1

[Greg Leo]

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

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

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

stable (default)

[Greg Leo]

That's my elan output

[Greg Leo]

Ok I see. I need to change the active toolchain

[Greg Leo]

Manually updated that in the .toml

[Greg Leo]

having some import issues now

[Greg Leo]

import tactic gets me

invalid import: tacti
could not resolve import: tacti

[Greg Leo]

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

[Greg Leo]

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

[Greg Leo]

leanproject upgrade-mathlib seemed to clear that up