using section parameters

Stream: general

[Thorsten Altenkirch]

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]

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

[Henrik Böving]

ah now!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Or is that not what you are asking?

[Johan Commelin]

Sigma is already an implicit parameter, in your example

[Reid Barton]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

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

[Reid Barton]

Right, it doesn't work like that

[Thorsten Altenkirch]

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

[Reid Barton]

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

[Johan Commelin]

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]

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

[Reid Barton]

well right, you can do :this: as well

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Jeremy Avigad]

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]

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]

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

[Yakov Pechersky]

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