Julin S (Apr 11 2022 at 04:51): Julin S (Apr 11 2022 at 04:51):I made a heterogenous list (hlist) like:
Require Import List.
Import ListNotations.
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).
I didn't make any argument implicit yet.
I can make hlists like:
Example hls1 : hlist Set (fun x => x) [nat; bool] :=
hcons Set (fun x=>x) nat [bool] 3
(hcons Set (fun x=>x) bool [] true (hnil _ _)).
Example hls2 : hlist Set (fun x => x) [bool; nat; bool] :=
hcons Set (fun x=>x) bool[nat;bool] false
(hcons Set (fun x=>x) nat [bool] 3
(hcons Set (fun x=>x) bool [] true (hnil _ _))).
Then I tried making a function to append to hlists and did:
Fixpoint happ {A:Type} {B:A->Type} {ls1 ls2: list A}
(hls1 : hlist A B ls1) (hls2: hlist A B ls2) :
hlist A B (ls1++ls2)%list :=
match hls1 in (hlist _ _ ls1) return
hlist A B (ls1++ls2)%list with
| hnil _ _ => hls2
| hcons _ _ _ _ y ys =>
hcons A B _ (tail (ls1++ls2)) y (happ ys hls2)
(*| hcons _ _ _ _ y ys => hcons A B (head ls1) (tail (ls1++ls2)) y (happ ys hls2) *)
end.
But that's giving error:
In environment
happ : forall (A : Type) (B : A -> Type) (ls1 ls2 : list A),
hlist A B ls1 -> hlist A B ls2 -> hlist A B (ls1 ++ ls2)
A : Type
B : A -> Type
ls1 : list A
ls2 : list A
hls1 : hlist A B ls1
hls2 : hlist A B ls2
a : A
l : list A
y : B a
ys : hlist A B l
The term "happ A B l ls2 ys hls2" has type "hlist A B (l ++ ls2)"
while it is expected to have type "hlist A B (List.tl (ls1 ++
ls2))".
I'm guessing that I was not able to let coq figure out that the (l ++ ls2) is
same as the (List.tl (ls1 ++ ls2)).
Had a similar problem earlier which was fixed (with help from here) by using
return in match statement. Can this also be fixed similarly?
Li-yao (Apr 11 2022 at 04:57):Put _ instead of tail (ls1 ++ ls2).
Or get the tail of ls1 from the hcons pattern (which the error message names l).
Julin S (Apr 11 2022 at 05:05):Thanks, that made it right.
Last updated: Oct 13 2024 at 01:02 UTC