Julin S (Apr 09 2022 at 10:46): Julin S (Apr 09 2022 at 10:46):I was making a heterogenous list (hlist) in the line of what's mentioned in here.
Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist A B []
| hcons : forall (x : A) (ls : list A),
(B x) -> hlist A B ls -> hlist A B (x::ls).
Arguments hnil {A B}.
Arguments hcons {A B x ls}.
This type checked all right.
And I was able to make hlists as well.
Example hls1 : hlist Set (fun x => x) [nat; bool] :=
hcons 3 (hcons true hnil).
Then I tried making a function to index into the element of hlists and made an hidx function.
But that gave error.
Fixpoint hidx_helper {A : Type} (ls : list A) (idx : nat) : Type :=
match idx, ls with
| _, []%list => unit
| O, (x::xs)%list => A
| S n', (x::xs)%list => hidx_helper xs n'
end.
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper ls idx :=
match idx, hls with
| _, hnil _ _ => tt (* --------ERROR here--------- *)
| O, hcons _ _ _ _ x xs => x
| S n', hcons _ _ _ _ x xs => hidx n' xs
end.
(*
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
The term "tt" has type "unit" while it is expected to have type
"hidx_helper ?l@{l0:=[]} ?n@{i0:=0}".
*)
I guess the problem is that I can't let Coq know that hidx_helper [] 0 evaluates to unit?
Compute hidx_helper []%list 0.
(* = unit : Type *)
How can I set this right?
Julin S (Apr 09 2022 at 10:48):And could there be a way where the hidx_helper needn't have been separately defined?
As it's used just to find the type of hidx?
Gaëtan Gilbert (Apr 09 2022 at 10:54):I guess the problem is that I can't let Coq know that hidx_helper [] 0 evaluates to unit?
no, the problem is that it hasn't figured out that the return type is hidx_helper [] 0 so it can't evaluate it
try match idx , hls in hlist _ _ ls return hidx_helper ls idx with
Julin S (Apr 09 2022 at 11:25):Thanks. That fixed the first branch of that match.
But the second is also having trouble that I couldn't figure out.
It says:
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper (a :: l) 0".
Could this be a similar problem?
Gaëtan Gilbert (Apr 09 2022 at 11:26):the definition of the helper looks wrong to me, it uses only the length of the list but not its contents
Julin S (Apr 09 2022 at 11:49):Yeah, I hadn't realized it.
Julin S (Apr 09 2022 at 11:50):I changed it to:
Fixpoint hidx_helper (A : Type) (lslen idx : nat) : Type :=
match idx, lslen with
| _, O => unit
| O, _ => A
| S n', S lslen' => hidx_helper A lslen' n'
(*| S n', (x::xs)%list => hidx_helper xs n' *)
end.
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper A (length ls) idx :=
match idx, hls in (hlist _ _ ls) return
(hidx_helper A (length ls) idx) with
| _, hnil _ _ => tt
| O, hcons _ _ _ _ x xs => x (* Error here! *)
| S n', hcons _ _ _ _ x xs => hidx n' xs
end.
But got a similar error:
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper A (length ls) idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper A (length (a :: l)) 0".
it should be something like
Fixpoint hidx_helper {A : Type} (B:A->Type) (ls : list A) (idx : nat) {struct ls} : Type :=
match idx, ls with
| _, []%list => unit
| O, (x::xs)%list => B x
| S n', (x::xs)%list => hidx_helper B xs n'
end.
I used this helper like:
Fixpoint hidx {A: Type} {B: A -> Type} {ls: list A}
(idx : nat) (hls : hlist A B ls)
: hidx_helper (fun x=>Type) ls idx :=
match idx, hls in (hlist _ _ ls) return
(hidx_helper (fun x=>Type) ls idx) with
| _, @hnil _ _ => tt
| O, @hcons _ _ _ _ x xs => x
| S n', @hcons _ _ _ _ x xs => hidx n' xs
end.
But got error:
In environment
hidx : forall (A : Type) (B : A -> Type) (ls : list A) (idx : nat),
hlist A B ls -> hidx_helper (fun _ : A => Type) ls idx
A : Type
B : A -> Type
ls : list A
idx : nat
hls : hlist A B ls
a : A
l : list A
x : B a
xs : hlist A B l
The term "x" has type "B a" while it is expected to have type
"hidx_helper (fun _ : A => Type) (a :: l) 0".
I guess I'm using it wrong. How should it be used?
Gaëtan Gilbert (Apr 09 2022 at 12:02):use B not fun x=>Type
Julin S (Apr 09 2022 at 12:16):Thanks a lot. That works. Now let me spend some time understanding it. :smiley:
Notification Bot (Apr 09 2022 at 12:16):Julin S has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC