Abstracting types in constructors

Stream: new members

[Ruben Lapauw]

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

[Eric Wieser]

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

[Ruben Lapauw]

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

[Eric Wieser]

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

[Ruben Lapauw]

(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.

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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".

[Ruben Lapauw]

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'?

[Ruben Lapauw]

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

[Kevin Buzzard]

Outside the section try #check @ntx

[Ruben Lapauw]

And inside or outside for @nty.

Thank you both!