Parametrized modules in Lean?

Stream: lean4

[Andrey Yao]

I am relatively new to Lean, but I have some prior experience using the Coq proof assistant. I am trying to work with variables (both implicit and explicit) in Lean in the following code snippet:

import Mathlib.Data.Finite.Basic
import Mathlib.Data.List.Basic
import Mathlib.Logic.Function.Defs
import Mathlib.Data.Set.Finite

/-- A vector is a list with extra length information enforced -/
structure Vect {n : Nat} (A : Type) where
  lst : List A
  len : lst.length = n

def Vect.map {A B : Type} (f : A -> B) (V : @Vect n A) : @Vect n B :=
  { lst := List.map f V.lst,
    len := Eq.subst V.len (List.length_map V.lst f) }

def Vect.mem {A : Type} (V : @Vect n A) (a : A) : Prop := List.Mem a V.lst

structure Schema where
  relSym : Type
  arities : relSym -> Nat

variable (S : Schema)
variable {outs : Nat}
variable {V V1 V2 : Type}
variable (vars : Set V) (vars1 : Set V1) (vars2 : Set V2)

structure Atom where
  R : S.relSym
  var_vec : @Vect (S.arities R) vars

structure CQ where
  head : @Vect outs vars
  body : List (Atom S vars)

def Atom.map (f : vars1 -> vars2) (A : Atom S vars1) : Atom S vars2 :=
{ R := A.R, var_vec := Vect.map f A.var_vec }

class homomorphism (q1 : @CQ S outs V1 vars1) (q2 : @CQ S outs V2 vars2) where
  f : vars1 -> vars2
  body_cond : List.Forall (fun (A : Atom S vars1) => q2.body.Mem (Atom.map S vars1 vars2 f A)) q1.body
  head_cond : q2.head = Vect.map f q1.head

As you can see, since I am using many variables, I have to manually put in a LOT of explicit variable instantiation to the types, for example at @CQ S outs V1 vars1. This can't be the expected way to structure my code, right? I know that in Coq you can use a "parametrized module" where the module takes these variables as arguments, and you can just use them freely in the module body. Is there a way to achieve something similar in Lean?

[Joël Riou]

Could you edit your code so as to add a list of imports which makes the code work?
Otherwise, the only simplification that I personaly see is that in the definition of CQ, vars refers to V, so that in the subsequent uses, you should not have to specify V1 and vars1, but only vars1. I would also make outs an explicit variable. Then the syntax CQ S outs vars1 could be used.

[Andrey Yao]

Sorry, hopefully it compiles now
Those are good suggestions. I was just wondering how people handle the number of variables in more complex codebases? It seems like there is extensive use of typeclasses, so I am assuming a lot of these variables are encapsulated in typeclass instances?

[Johan Commelin]

Yep, or custom structures that bundle a set of variables together

[Andrey Yao]

Thanks to you both!