Proving that a variable is of a given type

Stream: general

[Robert Maxton]

Given some a: α, some set s: set α, and a definition β: {x // x ∈ s}, how might I go about proving that a: ↥β, given that a is in fact ∈ s?

[Sebastien Gouezel]

Are you looking for β.2?

[Johan Commelin]

@Robert Maxton You can not prove that a term t has type T. That's only something that the type checker can check for you.

[Johan Commelin]

Also, if you have β: {x // x ∈ s}, then typically a: ↥β doesn't make sense. Did you mean

β := {x // x ∈ s} -- with the `=` sign

[Johan Commelin]

In that case, I think your question is how to construct a term of type ↥β starting from a and a proof ha : a ∈ s .

[Robert Maxton]

yes, I did. And... uh, if the type checker gets it wrong? For example, in my case I have a proof already in my context that a ∈ s, and a proposition that begins ∀ (a : ↥s) that I'd like to use it with; but the 'native type' of a is some underlying set.

[Johan Commelin]

The answer is that ↥β is a structure, so you can build it in 3 ways:

1. Using the constructor function: subtype.mk a ha
2. Using record syntax:

{ val := a,
  property := ha }

3. Using the anonymous constructor: \<a, ha\>. (If you type \< in VScode, then it will automatically replace it by the correct fancy unicode bracket).

[Johan Commelin]

Version 3 is what most people use, but it is good to realise that it is just a fancy short-hand for the other 2 options.

[Robert Maxton]

invalid constructor ⟨...⟩, 'has_lift_t.lift' is not an inductive type

[Johan Commelin]

Could you please paste more code?

[Robert Maxton]

bleh, making an mwe of this is a bit of a mess. let's see what I can do...

[Johan Commelin]

Maybe paste the output of extract_goal

[Robert Maxton]

import algebra.ring.basic
import algebra.ring_quot
import ring_theory.ideal.basic
import tactic

universe u

open_locale classical


theorem mwe {R: Type u} [comm_ring R] {I: ideal R} (x:R) :
  (∀ (a:I), @is_unit R (ring.to_monoid R) (1 + a))
    → true :=
λ hdefI, begin
  have: 1 + x ∈ I, by sorry,
  have: is_unit(2 + x), by {
    rw ← one_add_one_eq_two,
    rw add_assoc,
  }
end

[Robert Maxton]

At this point I'd like to say apply hdefI or apply (hdefI (1 + x)), but I can't because 1+x is of type R, not ↥I

[Johan Commelin]

    apply hdefI ⟨1 + x, this⟩,

[Patrick Massot]

You're making your life complicated by using the subtype associated to I too much. Can't you write

theorem mwe {R: Type u} [comm_ring R] {I: ideal R} (x:R) :
  (∀ a : R, a ∈ I → is_unit (1 + a))
    → true :=
λ hdefI, begin
  have: 1 + x ∈ I, by sorry,
  have: is_unit(2 + x), by {
    rw ← one_add_one_eq_two,
    rw add_assoc,
    exact hdefI _ this,
  },

end

(it's hard to tell without seeing more context).

[Robert Maxton]

@Patrick Massot ... I probably could have, but at this point I'd have to rewrite much of my proof, so I'd rather not. Something to think about in the future, then.
@Johan Commelin Huh. Thanks, that does work. How is that different from apply hdefI (1+x), though? Or like, the latter complains that I haven't proved that I has has_one, but the constructor doesn't seem to care?

[Johan Commelin]

x has type R, and so 1 + x also has type R.

[Johan Commelin]

But you want something that lives in the ideal. How should lean know that 1 + x is in the ideal?

[Johan Commelin]

You have to tell it this

[Johan Commelin]

In other words, you have to package together the element 1 + x and a proof that it is in the ideal I.

[Johan Commelin]

That's exactly what those weird brackets do for you.

[Patrick Massot]

If you really want to keep it this way then you can at least replace (∀ (a:I), @is_unit R (ring.to_monoid R) (1 + a)) by (∀ (a:I), is_unit (1 + a : R))

[Robert Maxton]

... Ah. I had the same problem when I was setting up this proof in the first place, so I expanded out is_unit for lack of any better way to tell Lean that the sum was valid.

[Robert Maxton]

What's the precedence of : over +? Is that "1 + (a of type R)", or "(1+a) which is of type R"?

[Robert Maxton]

and to be honest, I was kind of expecting unification to handle that; or like, it honestly confuses me that unification doesn't automatically fill in constructions of that form, given how implicit type conversion usually works in languages with type classes

[Robert Maxton]

then again, I probably shouldn't be applying Scala instincts to Lean too much lol

[Johan Commelin]

It is (1 + a) : R.

[Johan Commelin]

Robert Maxton said:

and to be honest, I was kind of expecting unification to handle that; or like, it honestly confuses me that unification doesn't automatically fill in constructions of that form, given how implicit type conversion usually works in languages with type classes

I'm still not sure what you would like Lean to do. Should it look into the context of your tactic state and see if you already have a proof of 1 + x at hand?

[Johan Commelin]

What should it do if you don't have such a proof ready?

[Sebastian Ullrich]

Note that the syntax is not _ : _ but (_ : _), which should implicitly answer the precedence question

[Robert Maxton]

I'm still not sure what you would like Lean to do. Should it look into the context of your tactic state and see if you already have a proof of 1 + x at hand?

Well, yes, essentially. That's the whole point of the proofs-as-types system, no? Since a proof would be of type 1+x ∈ I, all it would have to do is check if there's any variables of that type in the context. If there isn't, then it can complain that it failed to unify; but it seems weird that it can find 'an instance of a typeclass' but not 'an proof-instance of this Prop'.

[Johan Commelin]

Because typeclass search and unification are two different things.

[Patrick Massot]

Also note that the tactic state widget is very helpful to answer your precedence questions quickly and exactly in the case you care about. Simply move your mouse cursor above various symbols in the tactic state to see how they are grouped.

[Johan Commelin]

Robert Maxton said:

but it seems weird that it can find 'an instance of a typeclass' but not 'an proof-instance of this Prop'.

well, typeclass inference and unification are two very different things.

[Johan Commelin]

And you always have to balance speed vs automation

[Johan Commelin]

It's a trade-off

[Johan Commelin]

In this case, the idea is that writing \<a, ha\> is worth the hassle, compared to making lean try to figure things out itself.

[Johan Commelin]

Sure, in this case it needs to check x \mem I. But in general it could be any proposition that you are using to build a subtype.

[Patrick Massot]

Robert, in principle you could imagine a different elaborator which tries to do what you want. But as Johan wrote, it would make things more complicated for very few use cases. You would much more often need to switch to the explicit thing we have now.

[Robert Maxton]

Right, but no matter what proposition p it is, the subtype would be defined as {x \\ p x}, so it could always attempt to find a variable of type p x. And yeah, I guess mentally I conflate the two because I usually think of 'the algorithm that fills underscores' as 'unification'.

[Robert Maxton]

And I guess. Mostly my issue is that it's not very discoverable/the error isn't very legible, and AFAIK there isn't much about subtypes in any of the existing tutorials/documentation >.>

[Johan Commelin]

Robert Maxton said:

so it could always attempt to find a variable of type p x.

My claim is that this could potentially be pretty expensive.

[Robert Maxton]

That + 'other languages already do the automatic casting' is my motive here lol

[Johan Commelin]

We do automatic casting from the subtype {x // p x} to X. But not the other way round.

[Robert Maxton]

Fair. I haven't actually looked at lean's code/similar inference engine code myself, so I wouldn't know.

[Johan Commelin]

One direction doesn't need Lean to search for proofs, the other does.

[Johan Commelin]

We have automatic casting from nat to int to rat to real to complex, etc...

[Johan Commelin]

But you wouldn't want to have an automatic cast from int to nat that starts search for 0 \le n proofs

[Robert Maxton]

Though actually, how could it get expensive? After all, the number of variables in the context is presumably a fairly small number, and the types all have to be pre-computed for the interactive help function to work anyway

[Robert Maxton]

I'm not expecting it to automatically compose proofs together to try and build the right term, just to see if any of the existing variables already have the right type

[Robert Maxton]

or like, this seems solvable by greping on the existing interactive context output lol

[Johan Commelin]

It would be nice if we can make

example (X : Type) (s : set X) (x : X) (hx : x ∈ s) : true :=
begin
  lift x to s,
end

work

[Johan Commelin]

Robert Maxton said:

Though actually, how could it get expensive? After all, the number of variables in the context is presumably a fairly small number, and the types all have to be pre-computed for the interactive help function to work anyway

Because checking that two types are definitionally equal can get expensive.

[Robert Maxton]

Ah. Thus the use of the constructor so that you only have to do it for a single variable.

[Robert Maxton]

I suppose that makes some sense, though I'm still confused about what the interactive context is doing different...

[Johan Commelin]

What do you think of something like

instance foobar (R : Type*) [comm_ring R] (I : ideal R) : can_lift R I :=
{ coe := coe,
  cond := λ x, x ∈ I,
  prf := λ x hx, ⟨⟨x, hx⟩, rfl⟩ }

theorem mwe {R: Type u} [comm_ring R] {I: ideal R} (x:R) :
  (∀ (a:I), is_unit (1 + a : R)) → true :=
λ hdefI,
begin
  lift 1 + x to ↥I with y,
  have: is_unit(2 + x),
  { rw [← one_add_one_eq_two, add_assoc, ← h],
    apply hdefI y },
end

[Johan Commelin]

Robert Maxton said:

I suppose that makes some sense, though I'm still confused about what the interactive context is doing different...

The interactive context will show you hx : p x. If you have a goal q x, and you run assumption, then lean will try to see if hx has type q x. It will not syntactically compare p x and q x and stop if they differ.

[Johan Commelin]

In stead, it will try to see whether p x and q x are definitionally equal. This is a process that usually is very fast, but it can be quite expensive.

[Robert Maxton]

Actually, defining a has_lift like that would be valuable, yeah. Among other reasons it'd be entirely reasonable to include that in ring_theory.ideal.basic as a utility helper function, so it'd achieve the same effect of basically not having to worry about it anymore.

[Johan Commelin]

Yup, but can_lift is a relative "newcomer". So there are still a lot of gaps in the library where we should add instances.

[Robert Maxton]

and I see. So it's a sort of precedent problem, where we generally say that we operate up to definitional equality, but sometimes we have to revert to literal syntactic equality instead.

[Robert Maxton]

what's the distinction between can_lift and has_lift? I think I've seen the latter in the libraries already

[Johan Commelin]

Also, it doesn't work without the crazy up-arrow before the I, in lift 1 + x to ↥I with y. That's bad, I think. So we should fix that first.

[Johan Commelin]

@Floris van Doorn Any idea on how to do that :point_up:

[Johan Commelin]

Robert Maxton said:

what's the distinction between can_lift and has_lift? I think I've seen the latter in the libraries already

has_lift is about automatic coercions. Those will always be functions defined on all terms. can_lift is trying to help with the opposite battle. When you have a function X -> Y and a term y : Y, you can lift it to X if a certain predicate is full-filled.

[Johan Commelin]

E.g., you can lift a n : int to nat if you know 0 \le n.

[Johan Commelin]

In my opinion has_lift is bad terminology from the point of view of what's common terminology in maths. But is was there from the start, and it seems to be a common name in computer science.

[Johan Commelin]

So now we have a lot of things that are called lift, and sometimes they do opposite things :head_bandage:

[Robert Maxton]

ah, I see. Yes, that is exactly the sort of thing I'm looking for

[Robert Maxton]

and pft. Yeah, I actually usually see that as coercion or casting rather than lifting (unless it's strictly a supertype, which I think would roughly map to the usual math terminology), but I'm hardly a CS specialist.

[Johan Commelin]

I don't know about supertypes. But in maths, lifting is usually something that takes some effort.
E.g., you have

      Y
      |
   f  v
X --> Z

then you can ask whether the function f lifts to a function from X to Y.

[Patrick Massot]

I wonder whether the possibility of fixing this in Lean4 is still open.

[Sebastian Ullrich]

Which part, the naming?

[Sebastian Ullrich]

Note that there is no has_lift equivalent in the Lean 4 stdlib at all right now; after all, there is nothing special about it in contrast to has_coe (now Coe).

[Eric Wieser]

What was the original intent behind the separation of has_lift and has_coe?

[Kevin Buzzard]

@Sebastian Ullrich is there still quotient.lift? This is usually called quotient.descent in maths I guess. The quotient is smaller than the big set so lives under it.

[Sebastian Ullrich]

@Kevin Buzzard It is still there as Quot.lift. Interesting point of view; from a CS standpoint one would say that the quotient type is "structurally bigger", i.e. has one more type constructor, I'd guess. Like lifting monadic values into bigger monads (where no-one wants to think about cardinality).

[Kevin Buzzard]

My impression was that we had lost this argument some time ago wrt quotients.

[Kevin Buzzard]

It's the way we draw things on the blackboard

[Sebastian Ullrich]

I wasn't even aware there was an argument

[Kevin Buzzard]

All the mathematical language -- the bigger set "covers" the smaller one, points in the quotient "lift" to points in the bigger set etc -- are set up this way.

[Reid Barton]

Kevin, quotient.lift is just a lift in the opposite category of types and functions, what's the problem? :upside_down:

[Johan Commelin]

Maybe we should call it oplift then?

[Reid Barton]

In the category theory library I think we already use lift/desc as an opposite pair, so... yeah

[Floris van Doorn]

@Johan Commelin said:

Also, it doesn't work without the crazy up-arrow before the I, in lift 1 + x to ↥I with y. That's bad, I think. So we should fix that first.

I just saw this again when going through my starred messages. It is fixed in #7598

[Johan Commelin]

Thanks a lot Floris!