How to write Definitions without arguments in Coq?

Question

I have the following Inductive type defined in Coq.

Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity). 
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y  nil) ..).

The natlist is basically a list of natural numbers (similar to lists in Python). I am trying to find the union of two natlist using the definition below.

Definition union_of_lists : natlist -> natlist -> natlist

i.e Eval simpl in (union_of_lists [1,2,3] [1,4,1]) should return [1,2,3,1,4,1]

I have the following doubts.

• Since there are no arguments to this definition, how do I actually get the inputs and handle them?
• What does the definition union_of_lists return exactly? Is it just a natlist?

Any help or hints are highly appreciated.

Answer 1

Guys, I found the answer myself :) What I did was, I wrote a separate Fixpoint function 'append' and then assigned it to the definition of union_of_lists.

Fixpoint append(l1 l2 : natlist) : natlist := match l1 with | nil => l2 | (h :: t) => h :: app t l2 end.

and then

Definition union_of_lists : natlist -> natlist -> natlist := append.

Eval simpl in (append [1,2,3] [1,2,3]) returned [1,2,3,1,2,3]

The definition 'union_of_lists' returns a function which takes natlist as an argument and returns another function of type natlist -> natlist (i.e function taking a natlist argument and returning a natlist).

This definition of union_of_lists resembles functions in Functional Programming which can either return a function or a value.