letI etc

Stream: general

[Kevin Buzzard]

Q) Why does refl fail to finish the proof of Spv.refl in the code below?

I am about to write a bunch of API for a type Spv and I am going to have to get the hang of letI, exactI etc. I feel like my understanding of type class inference is now better than it was, and that I could do with a clearer picture of what is going on. Here's some documented minimised fully working code. Writing it has made me understand stuff better but I don't see why refl fails below.

import order.bounded_lattice -- for with_bot

universes u₀ u₁

-- what I need from with_bot
example (Γ : Type u₁) [partial_order Γ] : preorder (with_bot Γ) :=
by apply_instance

def valuation (R : Type u₀) (Γ : Type u₁) [partial_order Γ] :=
R → with_bot Γ

definition Spv (R : Type u₀) :=
{ineq : R → R → Prop // ∃ {Γ : Type u₀} [h : partial_order Γ],
 by exactI ∃ (v : valuation R Γ), ∀ r s : R, v r ≤ v s ↔ ineq r s}

lemma Spv.refl (R : Type u₀) (v : Spv R) : reflexive v.1 := λ r,
begin
  rcases v.2 with ⟨Γ, hΓ, v0, h⟩,
  -- hΓ : partial_order Γ
  -- but presumably type class inference doesn't know this yet.
  letI := hΓ,
  -- now it does
  rw ←h,
  -- v0 r : with_bot Γ
  -- ⊢ v0 r ≤ v0 r, and this ≤ is coming direct from hΓ and the
  -- instance in the example above.

  /-
  refl, -- fails!

  invalid apply tactic, failed to unify
  v0 r ≤ v0 r
with
  ∀ [_inst_1 : preorder ?m_1] (a : ?m_1), a ≤ a
  -/
  exact le_refl _, -- works
end

-- version without with_bot

def valuation' (R : Type u₀) (Γ : Type u₁) [partial_order Γ] :=
R → Γ

definition Spv' (R : Type u₀) :=
{ineq : R → R → Prop // ∃ {Γ : Type u₀} [h : partial_order Γ],
 by exactI ∃ (v : valuation' R Γ), ∀ r s : R, v r ≤ v s ↔ ineq r s}

lemma Spv'.refl (R : Type u₀) (v : Spv' R) : reflexive v.1 := λ r,
begin
  rcases v.2 with ⟨Γ, hΓ, v0, h⟩,
  -- Don't even need letI
  rw ←h, -- refl must now have worked
end

So there are two variants of a reflexivity proof. Let me talk through the code.

In the definition of Spv there is an inequality v r ≤ v s which, to make sense, relies on finding a preorder on with_bot Γ. The by exactI must be doing this. But it seems to me that what must be happening in practice is that the term generated by the definition of Spv must be plugging the partial order on with_bot Γ directly in, rather than saying "oh, we will deal with this using type class inference". Maybe this is how fully elaborated terms always work -- this is just dawning on me now as I write, I guess.

So in practice I am going to be writing a bunch of letI := hΓ's in my code I think. In the proof of Spv.refl, I do this.

But why does refl fail to finish the proof of Spv.refl?

Type class inference isn't finding the pre-order on with_bot Γ, even though I thought I inserted the partial order on Γ as early as I could.

[Kevin Buzzard]

lemma Spv.refl (R : Type u₀) (v : Spv R) : reflexive v.1 := λ r,
begin
  rcases v.2 with ⟨Γ, hΓ, v0, h⟩,
  rw ←h,
  exactI le_refl _, -- works
end

exactI also works. What does exactI do? I understand letI and haveI.

[Kevin Buzzard]

Independent issue:

attribute [refl] Spv.refl
/-
invalid binary relation declaration, relation 'reflexive' must have two explicit parameters
-/

??

[Reid Barton]

Do you know about resetI? resetI means "make everything in the context available for type class resolution". Of course things "to the left of the colon" were already available, so the point is to add things bound by a lambda, or by rcases, etc.--in particular your hΓ, I'm guessing.
exactI is resetI followed by exact.

[Kevin Buzzard]

import order.bounded_lattice -- for with_bot

universes u₀ u₁

-- what I need from with_bot
example (Γ : Type u₁) [partial_order Γ] : preorder (with_bot Γ) :=
by apply_instance

def valuation (R : Type u₀) (Γ : Type u₁) [partial_order Γ] :=
R → with_bot Γ

definition Spv (R : Type u₀) :=
{ineq : R → R → Prop // ∃ {Γ : Type u₀} [h : partial_order Γ],
 by exactI ∃ (v : valuation R Γ), ∀ r s : R, v r ≤ v s ↔ ineq r s}

lemma Spv.refl (R : Type u₀) (v : Spv R) : reflexive v.1 := λ r,
begin
  rcases v.2 with ⟨Γ, hΓ, v0, h⟩,
  resetI,
  rw ←h,
  letI : preorder (with_bot Γ) := by apply_instance,
  resetI,
  show (v0 r : with_bot Γ) ≤ v0 r,
  refl, -- fails
  /-
  invalid apply tactic, failed to unify
  v0 r ≤ v0 r
with
  ∀ [_inst_1 : preorder ?m_1] (a : ?m_1), a ≤ a
state:
R : Type u₀,
v : Spv R,
r : R,
Γ : Type u₀,
hΓ : partial_order Γ,
v0 : valuation R Γ,
h : ∀ (r s : R), v0 r ≤ v0 s ↔ v.val r s,
_inst : preorder (with_bot Γ) := partial_order.to_preorder (with_bot Γ)
⊢ v0 r ≤ v0 r
  -/
  sorry
end

[Kevin Buzzard]

It just seems to be an issue with refl. exact le_refl _ works fine.

[Mario Carneiro]

The issue with attribute [refl] Spv.refl is that the type of Spv.refl isn't asserting reflexivity of anything, it's proving reflexive bla. Lean is expecting a proof of my_rel bla x x

[Mario Carneiro]

I think if you just unfold reflexive in the statement lean will accept it... but then the relation you are proving reflexive is subtype.val which is a bit weird

[Mario Carneiro]

You should probably hide the implementation details of Spv by using something other than .1 to extract the relation from an Spv

[Mario Carneiro]

like define Spv.rel : Spv R -> R -> R -> Prop := subtype.val and then you can prove Spv.refl : Spv.rel v x x and mark it @[refl]