I’m getting some hard-to-decipher errors regarding type checking on some Coq code that I’m generating. Specifically, I have a dependently-typed function that reads a list from a store and returns it - if the list does not exist in the store, it returns an empty unit list.
This function was easy enough to write in a proof environment, but I’m now running into issues in my auto-generated code. Specifically, after a store is written to in a conditional expression, trying to read a list out of the new store with my dependently-typed function fails. Here’s a MWE, where the last three functions were auto-generated:
Require Import String.
Require Import ZArith.
Require Import List.
Import ListNotations.
Open Scope string_scope.
Inductive value := None | Int (z : Z) | List (T : Set) (l : list T).
Definition store : Type := string -> value.
Definition fresh_store : store := fun _ => None.
Definition update s k v : store :=
fun x => if String.eqb x k then v else s x.
Definition get_int (s : store) (id : string) : Z :=
match s id with
| Int z => z
| _ => 0
end.
Definition get_list :
forall (s : store) id,
match s id with
| List T _ => list T
| _ => list unit
end.
intros. destruct (s id); try (exact l); exact [].
Defined.
Definition max_idx {T: Type} (l : list T) := Nat.sub (List.length l) 1.
Definition test := update fresh_store "l" (List nat [1;2;3]).
Compute get_list test "l".
(* = [1; 2; 3]
: match test "l" with
| List T _ => list T
| _ => list unit
end*)
Compute max_idx (get_list test "l").
(* = 2
: nat*)
(*
Error: In environment
s : store
poison := false : bool
s0 : store
poison0 : bool
The term "get_list s0 "x"" has type
"match s0 "x"%string with
| List T _ => list T
| _ => list unit
end" while it is expected to have type
"list ?T@{s0:=s; s:=s0; poison:=poison0}".
*)
Definition culprit_function (s: store) :=
let poison : bool := false in
let (s,poison) :=
(if (negb poison) then
(update s "x" (List nat [1;2;3]),poison)
else
(s,true)) in
max_idx (get_list s "x").
(*
Error: Cannot infer the return type of pattern-matching on
"if negb poison
then
(update s "x" (List nat [1; 2; 3]), poison)
else (s, true)".
*)
Definition culprit_function_simpler (s: store) :=
let poison : bool := false in
let (s,poison) :=
(if (negb poison) then
(update s "x" (List nat [1;2;3]),poison)
else
(s,true)) in
get_list s "x".
(* Compiles fine! *)
Definition non_culprit (s: store) :=
let poison : bool := false in
let (s,poison) :=
(if (negb poison) then
(update s "x" (List nat [1;2;3]),poison)
else
(s,true)) in
get_int s "x".
We can see that retrieving an Int is no problem, but the call to get_list raises an error regarding the type of the output of get_list when it’s passed into another function, and another error regarding pattern-matching type inference when just the output of get_list is returned.
This is my first real foray into dependent typing, so I’m at a loss for why Coq can’t automatically infer that the output of get_list is a list whose type should clearly be fine to pass into max_idx, or why it can’t tell that both branches of the conditional statement return a store * bool. I can’t even seem to coerce type inference with let (s, poison) : store * bool := ... because I get a syntax error regarding :.
I’m also looking into passing in a proof that the output of the store is a List:
Definition get_list' {T : Set} {l : list T} (s : store) id (pf : s id = List T l) :=
l.
Definition test := update fresh_store "l" (List nat [1;2;3]).
Compute get_list' test "l" eq_refl. (* [1;2;3] *)
Compute max_idx (get_list' test "l" eq_refl). (* 2 *)
But I’m running into similarly-counterintuitive type-inference errors.
All this to say: what can I do next to be able to auto-generate code that can call dependent-typed functions and be able to use their output?