Basic Parameters troubles

Stream: new members

[Rémi Bottinelli]

Hey, I'm playing/trying to work out some code allowing to defining a path metric given enough structure on a set, and have trouble, as usual, making sense of parameters/variables.
Why is it that in edist_symm_le below, lean complains of an unknown identifier when I try to uncomment the sorryed line?

Thanks!

import data.real.ennreal
import topology.metric_space.emetric_space

noncomputable theory

open_locale classical ennreal

open emetric ennreal




section Path_Metric

parameters (α : Type*)
          (P : α → α → Type*)
          (L : Π {a b : α}, P a b → ennreal)
          (Lrefl : Π a : α, infi (@L a a) = (0 : ennreal))
          (Psymm : Π {a b : α}, P a b → P b a)
          (Lsymm : Π a b : α, Π p : P a b, L (Psymm p) ≤ L p)
          (Ptran : Π {a b c : α}, P a b → P b c → P a c)
          (Ltran : Π a b c : α, Π p : P a b, Π q : P b c, L (Ptran p q) ≤ L p + L q)

def edist (a b : α) : ennreal := infi (@L a b)

lemma edist_refl (a : α) : edist a a = 0 := Lrefl a

lemma edist_symm_le (a b : α) : edist a b ≤ edist b a :=
begin
  apply @infi_mono' _ _ _ _(@L a b) (@L b a),
  sorry,--exact (@Lsymm a b p)
end

lemma edist_symm (a b : α) : edist a b = edist b a :=
has_le.le.antisymm (edist_symm_le a b) (edist_symm_le b a)

lemma edist_triangle (a b c : α) : edist a c ≤ edist a b + edist b c :=
begin
  suffices : ∀ ε > 0, edist a c ≤ edist a b + edist b c + ε, by {
    sorry,
  },
  rintros ε hε,
  have p : P a b, by sorry,
  have hp : L p ≤ edist a b + ε/2, by sorry,
  have q : P b c, by sorry,
  have hq : L q ≤ edist b c + ε/2, by sorry,
  let pq := Ptran p q,
  have : L pq ≤ edist a b + edist b c + ε, by sorry,
  exact infi_le_of_le this,
end

end Path_Metric

[Eric Wieser]

Generally speaking, thinkg work better if you don't use parameters

[Eric Wieser]

Although the reason exact (@Lsymm a b p) fails is because lean doesn't know you were intending to use Lsymm in your proof, so doesn't make it available to you

[Eric Wieser]

If you add include Lsymm before that lemma (and omit Lsymm after) then that should be resolved

[Eric Wieser]

It works for Lrefl a because lean will look inside term-mode proofs to see which variables/parameters you intended to use; but it can't look inside tactic-mode ones

[Rémi Bottinelli]

ah, yeah, I remember readding about this, thanks!

[Rémi Bottinelli]

How would you correct the code to not use parameters, then, if I may ask?

[Rémi Bottinelli]

I'm thinking such generic code would be useful to generalize constructions such as the path metric on graphs, or the length metric on metric spaces. Would it be worth pursuing?

[Alex J. Best]

If you replace parameters with variables, you can then supply all of alpha, P L Lrefl, Psymm, ... each time.
This is a bit unwieldy, so you might be best off packing all these things into a structure, which is much easier to pass around