Say I have the following type typ representing bool or nat:
Inductive typ : Type := TB | TN.
I also have a function to extract an actual function type from a list of typs and a result type:
Fixpoint get_types (s: seq typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
| TN => nat -> get_types xs result_type
| TB => bool -> get_types xs result_type
end
end.
Example get_types_works : get_types (TB :: TN :: nil) nat = bool -> nat -> nat.
Proof. by []. Qed.
Now, I have another function that takes as input a list s of typs and a function of type get_types s:
Fixpoint app (s: seq typ) (constructor: get_types s nat) : nat :=
match s with
| nil => 2 (* Not properly handling empty list case for now *)
| TB :: nil => constructor true
| TN :: nil => constructor 2
| TB :: xs => app xs (constructor true)
| TN :: xs => app xs (constructor 2)
end.
Defining the above function fails at the line | TB :: nil => constructor true with:
Illegal application (Non-functional construction):
The expression "constructor" of type "get_types s nat" cannot be applied to the term
"true" : "bool"
Given we know here that the type of get_types s nat should be bool -> nat, as the value of s is TB :: nil, I'm wondering if there's a way we can make Coq aware of this so that the above function can be defined?
If not, is this a limitation of Coq or would the same apply to other dependently typed languages?
Edit: For context, this is not the original problem I'm trying to solve; it's a condensed version to show the issue I was having with the type system. In the actual version, rather than hard-coding 2 and true, the typ-like datastructure also carries indices of data to parse from a memory slice, and validation functions. The aim for app is a function that takes a list of such typs, a slice, and a constructor for a record containing such types, then constructs an instance of that record from the indices of the types to parse, or returns None if any of the validations fail.
Yet two other ways of defining app.
The first one uses tactics, and relies on induction instead of Fixpoint.
Definition app (s: seq typ) (constructor: get_types s nat) : nat.
Proof.
induction s as [|t xs].
- exact 2.
- destruct xs.
+ destruct t.
* exact (constructor true).
* exact (constructor 2).
+ destruct t.
* exact (IHxs (constructor true)).
* exact (IHxs (constructor 2)).
Defined.
The second one uses Gallina and complexed pattern-matchings.
Fixpoint app (s: seq typ) : get_types s nat -> nat :=
match s return get_types s nat -> nat with
| nil => fun _ => 2
| x :: xs =>
match xs as xs0 return xs = xs0 -> get_types (x::xs0) nat -> nat with
| nil => fun _ => match x return get_types (x::nil) nat -> nat with
| TB => fun c => c true
| TN => fun c => c 2
end
| _ => fun e => match e in _ = xs1 return get_types (x::xs1) nat -> nat with
| eq_refl =>
match x return get_types (x::xs) nat -> nat with
| TB => fun c => app xs (c true)
| TN => fun c => app xs (c 2)
end
end
end eq_refl
end.
When destructing xs, we remember an equality between the original xs and what it is destructed in. We do not need this equality in the nil branch and discards it with fun _. In the other branch, we pattern-match on the proof of equality (match e), which corresponds to a rewriting using this equality. Inside the eq_refl branch, we can use the original xs and thus make recursive calls allowed by the termination checker. Outside the pattern-match, we return the right type expected by the pattern-matching on xs. The last thing to do is to provide a proof of the equality of xs and xs0, but it is trivially eq_refl.