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]
Filippo A. E. Nuccio (Feb 22 2024 at 11:01):
I have two questions about letI
, one about its syntax and one about the docs. First of all, how can I use letI
in term mode? Suppose I have
import Mathlib
attribute [ -instance ] instInhabitedNat
def inHab : Inhabited ℕ := ⟨37⟩
example : Inhabited (ℕ × ℕ → ℕ) := by
letI := inHab
exact ⟨fun _ => default⟩
The exampe could be closed by infer_instance
, but I keep it in this way for the purpose of the question, since I would like to write it in term mode as
example : Inhabited (ℕ × ℕ → ℕ) where
default := ⟨fun _ => default⟩ -- it does not work of course
and I do not know how to pass the letI
.
Second question: the docs for letI
is "letI
behaves like let
, but inlines the value instead of producing a let_fun
term." I have always thought that the I
in letI
(and haveI
) were for "instance", but I now wonder whether they stand for "inline" and, more generally, if the doc is correct or if it should not contain a reference to the fact that it creates a local instance (perhaps this is what it is saying, but then it seems obscure).
Damiano Testa (Feb 22 2024 at 11:08):
Would this be good for you?
example : Inhabited (ℕ × ℕ → ℕ) :=
let _ := inHab
⟨fun _ => default⟩
Michael Stoll (Feb 22 2024 at 11:09):
AFAIU, the meaning of the "I" changed from Lean 3 to Lean 4.
Damiano Testa (Feb 22 2024 at 11:09):
I guess that it works also with where
syntax:
example : Inhabited (ℕ × ℕ → ℕ) where
default :=
let _ := inHab
fun _ => default
Damiano Testa (Feb 22 2024 at 11:10):
Also, yes, I
now stands for inline
, not anymore for instance
, I think.
Filippo A. E. Nuccio (Feb 22 2024 at 11:10):
And what does it mean?
Filippo A. E. Nuccio (Feb 22 2024 at 11:12):
BTW: Yes, your syntax works, but if the structure has more than one field, should I repeat the let _ :=
in each of them? If working in tactic mode, I could call let/letI
at the beginning, and it would be in scope for every proof of all fields.
Filippo A. E. Nuccio (Feb 22 2024 at 11:12):
Damiano Testa said:
Would this be good for you?
example : Inhabited (ℕ × ℕ → ℕ) := let _ := inHab ⟨fun _ => default⟩
Well, no, the whole point was to use where
(but your second answer is OK)
Damiano Testa (Feb 22 2024 at 11:16):
If you want to use where
with multi-field instances, I can offer this -- not sure if you like it:
class A where
x : Nat
y : Nat
attribute [local instance] inHab in
example : A where
x := default
y := default
Eric Wieser (Feb 22 2024 at 12:01):
Another option:
example : Inhabited (ℕ × ℕ → ℕ) :=
let _ := inHab
{ default := fun _ => default }
Eric Wieser (Feb 22 2024 at 12:02):
where
notation only works as a replacement for def foo := { ... }
not def foo := let x := y; { ... }
Filippo A. E. Nuccio (Feb 22 2024 at 12:02):
But in your snippet you have no {
Filippo A. E. Nuccio (Feb 22 2024 at 12:02):
I mean, not around let
Eric Wieser (Feb 22 2024 at 12:03):
Yes, that wouldn't make any sense
Filippo A. E. Nuccio (Feb 22 2024 at 12:03):
Ah, but you do not have where
Filippo A. E. Nuccio (Feb 22 2024 at 12:03):
I see!
Filippo A. E. Nuccio (Feb 22 2024 at 12:03):
And what is the theoretical advantage of allowing both :=
and where
?
Filippo A. E. Nuccio (Feb 22 2024 at 12:04):
I mean, from the point of view of designing lean syntax
Eric Wieser (Feb 22 2024 at 12:04):
Same as allowing both HMul.hMul
and *
; one looks nicer, but doesn't always work
Eric Wieser (Feb 22 2024 at 12:04):
(https://eric-wieser.github.io/lftcm-2023/#/defining-structures/1 has examples of all the way to make structure terms)
Filippo A. E. Nuccio (Feb 22 2024 at 12:04):
The one that "looks nicer" here is supposedly where
, right?
Eric Wieser (Feb 22 2024 at 12:05):
where
also lets you write someFun x y := x + y
instead of someFun := fun x y => x + y
Filippo A. E. Nuccio (Feb 22 2024 at 12:05):
This is nicer, agreed!
Filippo A. E. Nuccio (Feb 22 2024 at 12:08):
Just to explain why I insisted on where
: this is because it is the syntax the blue bulb in VSCode turns :=
to when asking for help, and I would like to have a way to say "thanks, what you suggest is OK, provided I pass you this instance".
Eric Wieser (Feb 22 2024 at 12:17):
If you write the let
first, then the blue bulb will insert {}
instead
Eric Wieser (Feb 22 2024 at 12:17):
That is, write let _ := inHab
then _
on the next line
Filippo A. E. Nuccio (Feb 22 2024 at 12:17):
Thanks!
Eric Wieser (Feb 22 2024 at 12:22):
I can't remember if I demoed that at the end of the recorded version of that talk (on youtube)
Last updated: May 02 2025 at 03:31 UTC