help proving antisymm

Stream: general

[Bernd Losert]

I have the following code:

import tactic
import order.filter.ultrafilter
import order.filter.partial

variable a : Type*

class convergence_space (a : Type*) :=
(conv : filter a -> a -> Prop)

open convergence_space

namespace convergence_space

instance : has_le (convergence_space a) := {
  le := fun p q, forall {l : filter a} {x : a}, @conv a q l x -> @conv a p l x
}

theorem conv_le_antisymm : forall (p q : convergence_space a), p <= q -> q <= p -> p = q := begin
  intros p q h h',
  ext l x,
  exact iff.intro (h l x, h' l x),
end

Unfortunately, lean complains with:

error: no applicable extensionality rule found for convergence_space

I think I need to unfold the definitions of h and h', but I'm not sure how to do so.

[Heather Macbeth]

If you tag the structure with @[ext], it should auto-generate the ext lemmas.

@[ext] structure convergence_space (a : Type*) :=
(conv : filter a → a → Prop)

#check convergence_space.ext
#check convergence_space.ext_iff

[Bernd Losert]

Ah, nice. Didn't know about that attribute. I added it, but now I get a type mismatch error in conv_le_antisymm.

[Heather Macbeth]

@Bernd Losert Your syntax is a bit off with iff.intro.

theorem conv_le_antisymm : forall (p q : convergence_space a), p <= q -> q <= p -> p = q := begin
  intros p q h h',
  ext l x,
  exact iff.intro h' h,
end

[Bernd Losert]

Ah, that works. I was confused because in another thread I asked about how to use ext and there it was like this:

theorem foo : ∀ (p q : a -> a -> Prop), (∀ x y, p x y -> q x y) → (∀ x y, q x y -> p x y) → p = q :=
begin
  intros p q hpq hqp,
  ext x y,
  exact ⟨hpq x y, hqp x y⟩,
end

[Heather Macbeth]

@Bernd Losert By the way, instead of proving some antisymmetry lemma directly, you probably want to put a partial order structure on convergence_space a, and then it will be accessible as docs#le_antisymm, while also hooking your result in to all the other lemmas about partial orders.

instance : partial_order (convergence_space a) :=
{ le_refl := _,
  le_trans := _,
  le_antisymm := λ p q h h', by { ext, exact iff.intro h' h },
  .. convergence_space.has_le a }

[Bernd Losert]

Actually, that's what I'm doing. I just wrote it out as a lemma to demonstrate my issue.

[Bernd Losert]

When I use your suggested instance, I get this error:

function expected at
  convergence_space.has_le
term has type
  has_le (convergence_space ?m_1)

[Bernd Losert]

Ah, it's because of a in has_le a.

[Yakov Pechersky]

Bernd, iff is an inductive type that produces a Prop. It has one single constructor, iff.intro. So either you say iff.intro h' h, or you say ⟨h', h⟩ because those chevrons are constructor notation (when used in this location). Whether or not you include l and x depends on the type of argument you made them be. In your definition on le you made them implicit, which is why you only need h' and h.

[Bernd Losert]

Makes sense.