## Stream: general

### Topic: using section parameters

#### Thorsten Altenkirch (Mar 18 2022 at 13:02):

I am starting to formalize some automata theory. First issue: I would like to use the alphabet (Sigma - how to use the greek letter?) as an implicit parameter. First I defined

section dfa
parameters {Sigma : Type}

structure dfa  : Type 1 :=
(Q : Type)
(init : Q)
(final : Q → Prop)
(δ : Q → Sigma → Q)
open dfa

def word : Type := list Sigma
def lang : Type := word → Prop

def δ_star (A : dfa) : A.Q → word → A.Q
| q [] := q
| q (x :: w) := δ_star (A.δ q x) w
end dfa


and this works fine but then I though I better factor this out:

section basics
parameter {Sigma : Type}

@[reducible]
def word : Type := list Sigma

@[reducible]
def lang : Type := word → Prop

end basics

section dfa
parameters {Sigma : Type}

structure dfa  : Type 1 :=
(Q : Type)
(init : Q)
(final : Q → Prop)
(δ : Q → Sigma → Q)

open dfa

def δ_star (A : dfa) : A.Q → word → A.Q
| q [] := q
| q (x :: w) := δ_star (A.δ q x) w

end dfa


and I get an error:

type mismatch at application
δ_star (A.δ q x) w
term
w
has type
list Sigma
but is expected to have type
word


So what is the recommended way to do this?

#### Henrik Böving (Mar 18 2022 at 13:03):

Did you write something in that box? It's just white empty for me

ah now!

#### Johan Commelin (Mar 18 2022 at 13:05):

@Thorsten Altenkirch I think Σ is claimed by the foundations of DTT...

#### Johan Commelin (Mar 18 2022 at 13:05):

So you'll have to use some unicode variant of it.

#### Johan Commelin (Mar 18 2022 at 13:05):

Or is that not what you are asking?

#### Johan Commelin (Mar 18 2022 at 13:05):

Sigma is already an implicit parameter, in your example

#### Reid Barton (Mar 18 2022 at 13:06):

I think using parameters with implicit variables doesn't make a lot of sense, better to just use variables

#### Johan Commelin (Mar 18 2022 at 13:07):

Parameters are local to sections. Once the section is closed, the argument starts behaving like a regular variable instead of a parameter.

#### Thorsten Altenkirch (Mar 18 2022 at 13:08):

Ok, I guess I am more thinking of something like a module parameter.

#### Reid Barton (Mar 18 2022 at 13:08):

Right, it doesn't work like that

#### Thorsten Altenkirch (Mar 18 2022 at 13:08):

Is there such a thing? Sigma is used by all the definitions in a section.

#### Reid Barton (Mar 18 2022 at 13:10):

No, we just rely on unification where possible, or write the type explicitly where not (as here)

#### Johan Commelin (Mar 18 2022 at 13:10):

I suppose you could do something like

section outer_scope_container_module

parameter {Sigma : Type} -- even better, make it explicit: (Sigma : Type)

section subsection_one

blabla

end subsection_one

section hi_Im_section_two

more blabla

end hi_Im_section_two

end outer_scope_container_module


#### Johan Commelin (Mar 18 2022 at 13:10):

But frankly, I would just use variables. It's the right thing 99% of the time.

#### Reid Barton (Mar 18 2022 at 13:10):

well right, you can do :this: as well

#### Reid Barton (Mar 18 2022 at 13:11):

In that case though it might be better to make it explicit, so that from outside the outer section (or whole module) you can specify it

#### Johan Commelin (Mar 18 2022 at 13:11):

jmc@atarrimbo:~/data/math/mathlib$rg variable | wc -l 14190 jmc@atarrimbo:~/data/math/mathlib$ rg parameter | wc -l
311


#### Reid Barton (Mar 18 2022 at 13:11):

It will be suppressed from what you write inside the section either way

#### Reid Barton (Mar 18 2022 at 13:14):

I'd say parameters is best used when you have a bunch of implementation details that you don't intend to expose that share the same context (e.g. a fixed alphabet). It's not a good approximation of Agda/ML modules. (Or really an approximation at all.)

#### Thorsten Altenkirch (Mar 18 2022 at 13:14):

Ok I can't use Sigma as an implicit variable, but making is explicit really gets very ugly as in

def dfa_lang (A : dfa Sigma) : lang Sigma
:= λ w , A.final (δ_star Sigma A A.init w)


#### Thorsten Altenkirch (Mar 18 2022 at 13:15):

I am not sure wether nested sections would work because I may want to use basics from different places.

#### Jeremy Avigad (Mar 18 2022 at 13:20):

One trick is to make up a type class with all the parameters you need. Here's an explanation I recently sent to someone:

import data.nat.prime
import tactic

class my_local_data :=
(a b c d : ℕ) (deq : d = a^2 + b) (cgez : 0 ≤ c)

section
variable [my_local_data]
open my_local_data

-- In this section, you can refer to a, b, c, d, deq, and cgez.
-- Lean needs to find an instance of my_local_data.
-- It just uses the anonymous version declared above.

def foo := a + c + 3

theorem bar : 2 ≤ foo :=
by {rw foo, linarith [cgez] }

theorem baz : 4 ≤ 2 * foo :=
begin
transitivity 2 * 2,
{ norm_num },
rw mul_le_mul_left,
exact bar,
norm_num,
end

end

-- Outside the section, all the theorems depend on the structure.

#check @foo
#check @bar
#check @baz

-- You can then state an explicit version manually.

theorem my_great_theorem {a b c d : ℕ} (deq : d = a^2 + b) (cgez : 0 ≤ c) :
4 ≤ 2 * (a + c + 3) :=
@baz ⟨a, b, c, d, deq, cgez⟩


#### Reid Barton (Mar 18 2022 at 13:21):

Thorsten Altenkirch said:

Ok I can't use Sigma as an implicit variable, but making is explicit really gets very ugly as in

def dfa_lang (A : dfa Sigma) : lang Sigma
:= λ w , A.final (δ_star Sigma A A.init w)


I would make Sigma explicit in types and implicit in functions, as if you were programming in Haskell. You can do this by declaring variables (Sigma : Type) at first and then redeclaring variables {Sigma} (without a type) later to switch the implicitness as needed.

#### Reid Barton (Mar 18 2022 at 13:27):

Of course it would look a bit nicer if you could use a unicode Sigma as well

#### Yakov Pechersky (Mar 18 2022 at 22:34):

There's always French quotes for escaping the Sigma...

Last updated: Aug 03 2023 at 10:10 UTC