Can I define functions of this type?

Stream: new members

[Justin Pearson]

I need to reason about partially defined functions. I'm using sub
types to represent domains. I can quite happily pass
around proofs that you have elements in the subtype to show that the
function applications make sense.

I have a structure representing families of partial assignments indexed by a
Type S. The thing that makes this harder/more interesting is that
the codomain of assign depends on the type S and the function
carrier that maps elements of S into some type.

Essentially it looks like this :-

variable V : Type
variable S : Type
variable carrier : S → Type

structure assignment   :=
  (domain : set (V × S) )
  (assign  (s:S) :    {v : V    // (v,s) ∈ domain } →  (carrier s) )

Abstractly it seems to do the job that I want and I can even produce
some of the proofs that I need, but I was trying to do some testing
and work on some concrete instances when I got stuck. My question is
this, using Lean can I actually define concrete functions (using
def) of type (assign (s:S) : {v : V // (v,s) ∈ domain } → (carrier s) )?

I suppose the real question is: Is there a better way of doing this?

[Eric Wieser]

def assign (s:S) (v : {v : V // (v,s) ∈ domain }) : carrier
s := sorry

is such a function

[Eric Wieser]

Of course if carrier s = empty and domain = set.univ then the sorry is impossible to fill out, but in a concrete case you would presumably be thinking of a particular compatible pair of domain and carrier

[Justin Pearson]

Even when V and S are inductive types with a finite number of elements, I'm at a lose on how to define more useful functions that the sorry case. I just don't understand enough of lean's syntax to define a specific function.

[Horatiu Cheval]

I am no expert, but as far as I understand the standard wisdom regarding design is that in many cases it is better to not use hypotheses on arguments (e.g. in the form of subtypes) in the types of functions, but rather defining functions to be total and return some junk values on wrong arguments and only require the hypotheses in lemmas about the functions. For example, division by zero is defined in Lean, and the divisor is only required to be nonzero in lemmas

[Horatiu Cheval]

Another alternative is using option valued functions to represent partial functions

[Horatiu Cheval]

That may or may not work for you, I think in any case it would be worth it to give some more specific examples of what kind of partial functions you want to express

[Reid Barton]

docs#part is intended for this kind of use. So def assignment := Π (s : S), V → part (carrier s).

[Reid Barton]

docs#option is also possible, but if you are happy to pass proofs of definedness around then you will probably prefer part.

[Justin Pearson]

Cool. It seems to do what I want. I'll take a look at the documentation. There even seems to be some theorems about going back and forward to option types. I might even be able to define concrete functions when I need them.

[Eric Wieser]

I think it would help if you had a concrete function in mind

[Justin Pearson]

I understand how option types give you partial functions. I've been writing Haskell code for more years than I care to remember. I was trying to avoid using option types, and instead carry around a proof that the values are in your domain. In terms of option types, I wanted to carry around a proof that you are not going to produce none values to avoid lifting. Abstractly it all seems to work, and it turns out that I'm reinventing part.

The computer scientist part of me, is not happy with my lean code just type checking. I wanted to do some concrete instantiations and use #reduce to see what is going on. My question is partly syntactical. Suppose that I have two finite types

inductive S
 | s
 | t

inductive V
 | x
 | y
 | z

Suppose I want to turn the partial function :

def o_assign : S →  V → option ℕ
 | S.s V.x := some 1
 | S.s V.y := some 2
 | S.t V.z := some 2
 | _   _   := none

into an instance of my above scheme :

def  domain : set (V × S)  := { ( V.x , S.s) , (V.y , S.s) , (V.z , S.t)   }
def  assign (s : S) : {v : V    // (v,s) ∈ domain }  → ℕ := sorry

Syntactically how do I write the function assign? The documentation for part is a bit brief, but if I turned each subtype into an instance of part set (V \times S) how would I write this?

On reflection it might be easier to use option types. Instead of carrying around a proof that your elements come from your domain, I will have to have extra proof cases that when you get things of type none it was because you applied it to values not in your domain. I suppose that's what monads are for. Even so, being stubborn and I I would like to know how to use part in the future, I would still like to understand what is going on.

[Eric Wieser]

I'd expect you can use something like:

def assign (s:S) (v : {v : V // (v,s) ∈ domain }) : ℕ
| S.s ⟨V.x, _⟩ := 1
| S.s ⟨V.y, _⟩ := 2
| S.t ⟨V.z, _⟩ := 2
| _ _ := false.elim sorry

Although you might have to add more than one false.elim case:

def assign (s:S) (v : {v : V // (v,s) ∈ domain }) : ℕ
| S.s ⟨V.x, _⟩ := 1
| S.s ⟨V.y, _⟩ := 2
| S.s ⟨V.z, h⟩ := false.elim sorry
| S.t ⟨V.x, h⟩ := false.elim sorry
| S.t ⟨V.y, h⟩ := false.elim sorry
| S.t ⟨V.z, _⟩ := 2

[Eric Wieser]

That is; the equation compiler may or may not be smart enough to eliminate the impossible cases for you, so it's up to you to do so

[Eric Wieser]

Having said that, this defines a provably equal function:

def assign (s:S) (v : {v : V // (v,s) ∈ domain }) : ℕ
| S.s ⟨V.x, _⟩ := 1
| S.s ⟨V.y, _⟩ := 2
| S.t ⟨V.z, _⟩ := 2
| _ _ := 37