Stream: Coq users

Topic: Appending two hlists


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Julin S (Apr 11 2022 at 05:05):

Thanks, that made it right.


Last updated: Feb 04 2023 at 21:02 UTC