Eliminating forall in hypothesis and applying.

Stream: new members

[Greg Leo]

I am working through some simple examples for dealing with real-valued functions in lean. I have two questions.

First, In the following example, how can I apply the introduced variables to eliminate the forall in the hypothesis rep?

Second, once that is eliminated, how can I rewrite, for example, R x y to be f x >= f y using that rep hypothesis?

MWE

import tactic
import data.real.basic
open classical set function

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

def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧  R y z) → R x z


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

theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
sorry,
},


end

end

[Kevin Buzzard]

Doesn't the parameter give you two Rin the definition of complete? I would encourae you to not use parameters; they are not used at all in mathlib for example.

[Greg Leo]

That's right. I'm not sure where I picked up this habit, but someone else mentioned it to me as well.

[Kevin Buzzard]

Replace parameters with variables would be the first thing I'd do with your code.

[Greg Leo]

Ok, this gets those parameters replaced with variables. I will have to read more about the distinction, but I found it here: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html

import tactic
import data.real.basic
open classical set function

section

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

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

def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧  R y z) → R x z

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

theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
sorry,
},


end

end

[Greg Leo]

Hey! That fixed it!

[Greg Leo]

import tactic
import data.real.basic
open classical set function

section

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

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

def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧  R y z) → R x z

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

theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h,
rename [h_w f, h_h rep],
rw [complete],
intro x,
intro y,
have rep2 : f x ≥ f y ↔ R x y, from rep x y,



},


end

end

[Greg Leo]

Let's see if I can make some progress. By the way, @Kevin Buzzard your videos are amazing! I love how fluent you are in Lean. It is inspiring. I find myself emulating the way you talk in the videos when I work with my RA in lean.

[Kevin Buzzard]

If you don't like the name h_w (and who would!) then you can do cases h with f rep

[Greg Leo]

That is better. Making some progress here.

import tactic
import data.real.basic
open classical set function

section

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

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

def rtransitive (R : A → A → Prop) : Prop :=
∀ x y z, (R x y ∧  R y z) → R x z

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

theorem represents : (∃ f : A → ℝ, ∀ x , ∀ y, f x ≥ f y ↔ R x y) → complete R :=
begin
intro h,
{
cases h with f rep,
rw [complete],
intro x,
intro y,
have repxy : f x ≥ f y ↔ R x y, from rep x y,
have repyx : f y ≥ f x ↔ R y x, from rep y x,
cases repxy with fxfyRxy Rxyfxfy,
cases repyx with fyfxRyx Ryxfyfx,
sorry,

},


end

end

[Greg Leo]

Think I need to show fx >= fy or fy >= fx from completeness of >= on the reals.