# Zulip Chat Archive

## Stream: general

### Topic: letI etc

#### Kevin Buzzard (Mar 05 2019 at 09:17):

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 (Mar 05 2019 at 09:19):

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 (Mar 05 2019 at 09:29):

Independent issue:

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

??

#### Reid Barton (Mar 05 2019 at 17:56):

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 (Mar 05 2019 at 18:05):

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 (Mar 05 2019 at 18:13):

It just seems to be an issue with `refl`

. `exact le_refl _`

works fine.

#### Mario Carneiro (Mar 05 2019 at 18:42):

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 (Mar 05 2019 at 18:43):

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 (Mar 05 2019 at 18:44):

You should probably hide the implementation details of `Spv`

by using something other than `.1`

to extract the relation from an Spv

#### Mario Carneiro (Mar 05 2019 at 18:45):

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]`

Last updated: Dec 20 2023 at 11:08 UTC