Zulip Chat Archive

Stream: new members

Topic: Abstracting types in constructors


view this post on Zulip Ruben Lapauw (Jan 13 2021 at 23:47):

I want to abstract a complex type by introducing a "newtype". How can I pass the implicit variables implicitly?

variables {x:nat}

structure nt: Type := (data: fin x)

--Works
structure foo := (v : list (@nt x))

--Error:
--  don't know how to synthesize placeholder
--  context:
--  x x : ℕ
--  ⊢ ℕ
structure foo := (v : list nt)

Edit: smaller MWE

view this post on Zulip Eric Wieser (Jan 13 2021 at 23:51):

What are you expecting the last line to do? How would lean know to pass x to @nt and not 37?

view this post on Zulip Ruben Lapauw (Jan 13 2021 at 23:53):

The same way lean knows x is available when proving theorems? I don't need to specify most type-variables in those proofs.

view this post on Zulip Eric Wieser (Jan 14 2021 at 00:07):

Can you give an example of the case you're thinking of that does work, so that I can explain the difference?

view this post on Zulip Ruben Lapauw (Jan 14 2021 at 00:12):

(from https://github.com/leanprover-community/tutorials/blob/0a0de42dd339de62b1e781745fd128afba4d1df8/src/solutions/00_first_proofs.lean#L146)

lemma inf_lt {A : set } {x : } (hx : x is_an_inf_of A) :
   y, x < y   a  A, a < y :=

is used like this:
(https://github.com/leanprover-community/tutorials/blob/0a0de42dd339de62b1e781745fd128afba4d1df8/src/solutions/00_first_proofs.lean#L398)

      apply inf_lt h,

in which A and x are implicit.

view this post on Zulip Eric Wieser (Jan 14 2021 at 00:13):

Right, that's because h contains x and A as part of its type

view this post on Zulip Eric Wieser (Jan 14 2021 at 00:14):

If you know the type of h, then lean has only one possibly choice for those implicit variables - so it makes that choice

view this post on Zulip Eric Wieser (Jan 14 2021 at 00:17):

Having said that, you can probably get what you want with parameters {x : nat} which I think tells lean "treat x as a constant in the current section".

view this post on Zulip Ruben Lapauw (Jan 14 2021 at 00:20):

yeah, thats exactly what I want!

But continuing with the problem:
Thus if I had:

variable {x :nat}
structure nt {y: nat} (x=y) : Type := (data: fin x)

then

structur foo := (v: list (nt ($$$)))     -- With $$$ a proof that x=x

would work? Since in this proof there is a variable which is then unified with the unknown 'x'?

view this post on Zulip Ruben Lapauw (Jan 14 2021 at 00:32):

Curiouser and curiouser: with parameters the second example works, but not the first. This I can somewhat understand. However their type makes me very confused. How can I see their full type?

section s
parameters {x:nat}
variable {y: nat}

structure ntx: Type := (data: fin x)
structure nty: Type := (data: fin y)

#check ntx -- ntx : Type
#check nty -- nty : Type
end s

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 00:42):

Outside the section try #check @ntx

view this post on Zulip Ruben Lapauw (Jan 14 2021 at 00:45):

And inside or outside for @nty.

Thank you both!


Last updated: May 06 2021 at 22:13 UTC