179 lines
4.5 KiB
Coq
179 lines
4.5 KiB
Coq
(* coq-ext-lib *)
|
|
|
|
(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
|
|
(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.Member.html *)
|
|
From ExtLib Require Import HList.
|
|
From ExtLib Require Import Member.
|
|
|
|
Require Import Program.
|
|
|
|
|
|
Fail Program Fixpoint foo {A:Type} (A_beq: A -> A -> bool)
|
|
(a:A): forall (l:list A), member a l := fun l =>
|
|
match l with
|
|
| nil => _
|
|
| cons x xs =>
|
|
if A_beq x a then MZ _ _
|
|
else foo A_beq a xs
|
|
end.
|
|
|
|
|
|
(*
|
|
s ∈ l1 -> s ∈ l1++l2
|
|
*)
|
|
Fixpoint memberappL {A:Type} {l1:list A} {a:A}
|
|
(l2:list A) (m: member a l1): member a (l1++l2).
|
|
Proof.
|
|
refine (
|
|
match m with
|
|
| MZ _ _ => MZ _ _
|
|
| MN _ mn => MN _ (memberappL _ _ _ _ _)
|
|
end).
|
|
assumption.
|
|
Defined.
|
|
|
|
(*
|
|
s ∈ l2 -> s ∈ l1++l2
|
|
*)
|
|
Fixpoint memberappR {A:Type} {l1:list A} {a:A}
|
|
(l2:list A) (m: member a l2): member a (l1++l2).
|
|
Proof.
|
|
refine (
|
|
match l1 with
|
|
| nil => m
|
|
| cons _ xs => MN _ (memberappR _ xs _ _ m)
|
|
end).
|
|
Defined.
|
|
|
|
Module HListNotations.
|
|
Declare Scope hlist_scope.
|
|
Delimit Scope hlist_scope with hlist.
|
|
|
|
Notation "« »" := Hnil : hlist_scope.
|
|
Notation "« x »" := (Hcons x Hnil) : hlist_scope.
|
|
Notation "« x ; .. ; y »" := (Hcons x .. (Hcons y Hnil) ..) : hlist_scope.
|
|
Infix "++" := hlist_app: hlist_scope.
|
|
End HListNotations.
|
|
|
|
|
|
Require Import String List.
|
|
Open Scope string.
|
|
|
|
Import ListNotations.
|
|
Import HListNotations.
|
|
Open Scope hlist.
|
|
|
|
Check «3; true» : hlist (fun x:Set=>x) [nat; bool].
|
|
(* « 3; true » : hlist (fun x : Set => x) [nat; bool] *)
|
|
|
|
Example eg1 := «3» : hlist (fun x:Set=>x) [nat].
|
|
Example eg2 := «2; true»: hlist (fun x:Set=>x) [nat; bool].
|
|
Example eg3 := «(0,3)» : hlist (fun x:Set=>(x*nat)%type) [nat].
|
|
Example eg4 := «2; true; "h"; (2,3)»: hlist (fun x:Set=>x) [nat; bool; string; (nat*nat)%type].
|
|
|
|
Example eg5 := [0; 1].
|
|
Print member.
|
|
Check MN _ (MZ _ _): member 1 eg5.
|
|
Fail Check [MZ _ _: member 0 eg5; MN _ (MZ _ _)].
|
|
Example mm5 := «MZ _ _; MN _ (MZ _ _)»: hlist (fun t => t) [member 0 eg5; member 1 eg5].
|
|
Check mm5.
|
|
Example mm5' := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l => (fun x => member x l)) eg5) [0; 1].
|
|
Example mm5'2 := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l x => member x l) eg5) [0; 1].
|
|
Example mm5'3 := «MZ _ _; MN _ (MZ _ _)»: hlist ((fun l x => member x l) eg5) eg5.
|
|
|
|
|
|
Section Foo.
|
|
Context {A T:Type}.
|
|
Variables (l:list A).
|
|
Fail Variable f: forall (l:list A) (x:B), member x l.
|
|
|
|
Variable f': list T -> T -> Type.
|
|
Variable f: forall (ts:list T) (x:T), member x ts.
|
|
Variable ts: list T.
|
|
Variable a: A.
|
|
|
|
Fixpoint foo (hls: hlist (f l) ts) (a: A)
|
|
|
|
foo (hl: hlist (f l) [member x l]): hlist (f l) [member x (l++[a])
|
|
|
|
End Foo.
|
|
|
|
|
|
|
|
|
|
Check «» : hlist (fun x:Set=>x) [].
|
|
(* « » : hlist (fun x : Set => x) [] *)
|
|
|
|
Check « "hi" » : hlist (fun x:Set=>x) [string].
|
|
(* « "hi" » : hlist (fun x : Set => x) [string] *)
|
|
|
|
Check «(0,3); (1,true)» : hlist (fun x:Set=>(nat*x)%type) [nat; bool].
|
|
(* « (0, 3); (1, true) » *)
|
|
|
|
Compute hlist_hd eg1.
|
|
(* = 3 : nat *)
|
|
Compute hlist_hd eg3.
|
|
(* = (0, 3) : nat * nat *)
|
|
|
|
Compute hlist_tl eg1.
|
|
(* = « » : hlist (fun x : Set => x) [] *)
|
|
Compute hlist_tl eg2.
|
|
(* = « true » : hlist (fun x : Set => x) [bool] *)
|
|
|
|
Compute eg1 ++ eg2 ++ eg2.
|
|
(* = « 3; 2; true; 2; true » *)
|
|
|
|
Compute hlist_tl (eg1 ++ eg2 ++ eg2).
|
|
(* = « 2; true; 2; true » *)
|
|
|
|
|
|
(* [Member.member] is like the proof relevant version of [List.In] *)
|
|
(* Kinda like the relation between [sumbool] and [bool] *)
|
|
Print member.
|
|
|
|
(** Indexing *)
|
|
Compute hlist_get (MZ _ _) eg2.
|
|
(* = 2 : nat *)
|
|
Compute hlist_get (MN _ (MZ _ _)) eg2.
|
|
(* = true : bool *)
|
|
Compute hlist_get (MN _ (MN _ (MZ _ _))) eg4.
|
|
(* = "h" : string *)
|
|
Compute hlist_get (MN _ (MN _ (MN _ (MZ _ _)))) eg4.
|
|
(* = (2, 3) : nat * nat *)
|
|
|
|
(** Getting nth element *)
|
|
Compute hlist_nth eg4 2.
|
|
(* = "h"
|
|
: match nth_error [nat; bool; string; (nat * nat)%type] 2 with
|
|
| Some t => t
|
|
| None => unit
|
|
end
|
|
*)
|
|
|
|
Compute nth_error[nat; bool; string; (nat * nat)%type] 2.
|
|
(* = Some string : option Set *)
|
|
|
|
Unset Printing Notations.
|
|
|
|
(** Converting list to hlist ?? *)
|
|
Compute hlist_gen _ [1].
|
|
(* = Hcons (?f 1) Hnil
|
|
: hlist ?F (cons 1 nil) *)
|
|
|
|
Compute hlist_gen (fun x=>x) [1].
|
|
(* = Hcons 1 Hnil
|
|
: hlist (fun _ : nat => nat) (cons 1 nil) *)
|
|
|
|
|
|
Infix "∈" := member (at level 50).
|
|
|
|
|
|
|
|
Compute memberappL (cons 2 nil) (MZ 3 (cons 3 nil)).
|
|
Fail Compute memberappR (cons 2 nil) (MZ _ (cons 3 nil)).
|
|
|
|
(** Converting hlist to list ?? *)
|
|
(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
|
|
Fail Check hlist_erase eg1.
|
|
|