CODEWITHSUNDEEP
lean
LyX2394
LyX2394

Reputation: 131

How to remove a universal quantifier in Lean?

I am working with two binary relations: g_o and pw_o, and I've defined pw_o below:

constants {A : Type} (g_o : A → A → Prop)

def pw_o (x y : A) : Prop := ∀ w : A, (g_o w x → g_o w y) ∧ (g_o y w → g_o x w)

I need to prove the following:

theorem prelim: ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=

I start with these tactics:

begin

   intros,

   cases a with h1 h2,

end

And I have this:

x y z : A,
h1 : g_o x y,
h2 : pw_o y z
⊢ g_o x z

Since pw_o is defined with a universal quantifier, I'd like to substitute w with x, then I would have (g_o x y → g_o x z) ∧ (g_o z x → g_o y x). After isolating the first conjunct with the "cases" tactic, I can use modus ponens on that first conjunct and h1.

How can I tell Lean to replace w in the definition of pw_o with x and replace x and y in the definition of pw_o with y and z, respectively?

Upvotes: 0

Views: 456

Answers (1)

matt
matt

Reputation: 5614

Elimination of the universal quantifier is basically just application, so to substitute w, with x just apply x to the instance h2 of pw_o y z.

theorem prelim': ∀ x y z : A, g_o x y ∧ pw_o y z → g_o x z :=
begin

   intros,

   cases a with h1 h2,
   cases h2 x with h3 _,
   sorry
end

Upvotes: 1

Related Questions