zunction · April 24, 2020 08:56 · zunction · Apr 24, 2020
diff --git a/new.v b/new.v
 From mathcomp Require Import all_ssreflect.

 From void Require Import void.
 From deriving Require Import deriving.

 Require Import Coq.Strings.String.
 Open Scope string_scope.

 (* Deriving the type structures of string *)
 Canonical string_indType := Eval hnf in IndType _ _ [indMixin for string_rect].
 Canonical string_eqType := Eval hnf in EqType string [derive eqMixin for string].
 Canonical string_choiceType := Eval hnf in ChoiceType string [derive choiceMixin for string].
 Canonical string_countType := Eval hnf in CountType string [derive countMixin for string].

 Inductive uri : Type := Build_uri (s : string).
 Definition defaultU := Build_uri "default".

 (* Deriving the type structures of uri *)
 Definition uri_indMixin := Eval hnf in [indMixin for uri_rect].
 Canonical uri_indType := Eval hnf in IndType _ _ uri_indMixin.
 Canonical uri_eqType := Eval hnf in EqType uri [derive eqMixin for uri].
 Canonical uri_choiceType := Eval hnf in ChoiceType uri [derive choiceMixin for uri].
 Canonical uri_countType := Eval hnf in CountType uri [derive countMixin for uri].

 Notation vertexT := uri.
 Notation edgeT := (uri * uri * uri)%type.
 Definition default_edgeU := (defaultU,defaultU,defaultU).

 Section Query.

 Variable V : seq vertexT.
 Variable E : seq edgeT.

 Definition query_pred := seq edgeT -> pred vertexT.

 (* we use && to connect the two fields together to enable boolean predicate subtyping *)
 Record query_type (qp: query_pred) := Answer { query_uri :> uri ; query_uriP : query_uri \in (filter (qp E) V) }.

 (* 
 Record query_type (qp: query_pred) := Answer { query_uri :> uri ; query_uriP : query_uri \in _ : (query_uri \in V) && ((E, query_uri) \in qp)}.
 *)

 (* Building the instances of subType, eqType for query_type *)
 Canonical queryt_subType (qp:query_pred) := Eval hnf in [subType for query_uri qp].
 Definition queryt_eqMixin (qp:query_pred) := Eval hnf in [eqMixin of (query_type qp) by <:].
 Canonical queryt_eqType (qp:query_pred) := Eval hnf in EqType (query_type qp) (queryt_eqMixin qp).
 Definition queryt_choiceMixin (qp:query_pred) := Eval hnf in [choiceMixin of (query_type qp) by <:].
 Canonical queryt_choiceType (qp:query_pred) := Eval hnf in ChoiceType (query_type qp) (queryt_choiceMixin qp).
 Definition queryt_countMixin (qp:query_pred) := Eval hnf in [countMixin of (query_type qp) by <:].
 Canonical queryt_countType (qp:query_pred) := Eval hnf in CountType (query_type qp) (queryt_countMixin qp).

 Definition queryt_enum (qp:query_pred) : seq (query_type qp) := undup (pmap insub (filter (qp E) V)). 

 Lemma mem_queryt_enum (qp:query_pred) (x : query_type qp) : x \in (queryt_enum qp).
 Proof. by rewrite mem_undup mem_pmap -valK map_f ?query_uriP. Qed.

 Fact queryt_axiom (qp:query_pred) : Finite.axiom (queryt_enum qp).
 Proof. exact: Finite.uniq_enumP (undup_uniq _) (mem_queryt_enum qp). Qed.

 Definition queryt_finMixin (qp:query_pred) := Finite.Mixin (queryt_countMixin qp) (queryt_axiom qp).
 Canonical queryt_finType (qp:query_pred) := Eval hnf in FinType (query_type qp) (queryt_finMixin qp). 

 End Query.

 (* Building the uris for some strings *)
 Definition personU := Build_uri "person".
 Definition birthcertU := Build_uri "birthcert".

 Definition barackU := Build_uri "barack".
 Definition michelleU := Build_uri "michelle".
 Definition maliaU := Build_uri "malia".
 Definition sashaU := Build_uri "sasha".

 Definition bc_maliaU := Build_uri "birthcert_malia".
 Definition bc_sashaU := Build_uri "birthcert_sasha".

 Definition hasTypeU := Build_uri "hasType".
 Definition hasPersonU := Build_uri "hasPerson".
 Definition hasFatherU := Build_uri "hasFather".

 Definition vertexL := [:: personU; birthcertU; barackU; michelleU; maliaU; sashaU; 
                          bc_maliaU; bc_sashaU;
                          hasTypeU; hasPersonU; hasFatherU].

 Definition edgeL := [:: (barackU,hasTypeU,personU); (michelleU,hasTypeU,personU);
                       (maliaU,hasTypeU,personU); (sashaU,hasTypeU,personU);
                       (bc_maliaU,hasTypeU,birthcertU); (bc_sashaU,hasTypeU,birthcertU);
                       (bc_maliaU,hasPersonU,maliaU); (bc_sashaU,hasPersonU,sashaU);
                       (bc_maliaU,hasFatherU,barackU); (bc_sashaU,hasFatherU,barackU)].

 (* Specification of a predicate to determine the type of a uri *)

 (* makePred1 is a predicate on the subject, useful for checking membership of terms to a type *)
 Definition makePred1 rel obj : query_pred := fun E x => (x, rel, obj) \in E.

 Definition personP := makePred1 hasTypeU personU.
 Definition birthcertP := makePred1 hasTypeU birthcertU.
 Definition defaultP := makePred1 hasTypeU defaultU.

 Compute barackU \in personP edgeL.
 Compute bc_maliaU \in birthcertP edgeL.
 Compute barackU \in birthcertP edgeL.

 Section TripleDict.

 Variable A : eqType.
 Implicit Type (s r : A).
 Implicit Type (vl : seq A).
 Notation B := (A*A*A)%type.
 Variable (e : B).
 Implicit Type (el : seq B).

 (* 
  Generalized definition of query_pred 
  Definition gen_query_pred := seq B -> pred A.
 *)

 (* Predicate on edge for given subject and relation *)
 Definition sub_rel s r (triple : B) := (triple.1 == (s,r)). 

 (* Returns a triple containing the given subject and relation. nth ensures only the first triple is returned.  *)
 Definition sub_rel2triple s r el := nth e el (find (sub_rel s r) el). 

 (*
 Definition getObj s r : qp := fun el => fun x => (sub_rel2triple s r el) == (s, r, x).

 Lemma FindObj s r vl el : has (sub_rel s r) el -> (sub_rel2triple s r el).2 \in vl
                             -> (sub_rel2triple s r el).2 \in [seq x <- vl | getObj s r el x].
 Proof. pose H := has (sub_rel s r) el.
 have lem1 : H -> (sub_rel2triple s r el).1 == (s,r). { apply/nth_find. }
 move=> h m. move: (lem1 h)=> p.
 by rewrite mem_filter m /getObj -(eqP p) -surjective_pairing eq_refl.
 Qed.
 *)

 (* Lemma that finds the answer from the query *)
 Lemma FindAns s r vl el : has (sub_rel s r) el -> (sub_rel2triple s r el).2 \in vl
                         -> (sub_rel2triple s r el).2 \in [seq x <- vl | (s, r, x) \in el].
 Proof.
  pose H := has (sub_rel s r) el.
  have lem1 : H -> (sub_rel2triple s r el).1 == (s,r). { apply/nth_find. }
  have lem2 : H -> (find (sub_rel s r) el) < size el. { by rewrite -has_find. } 
  move => h m; move: (lem1 h) => p; move: (lem2 h) => q.
 (*  rewrite mem_filter. rewrite m. rewrite -{1}(eqP p). rewrite -surjective_pairing. rewrite mem_nth. *)
  by rewrite mem_filter m -{1}(eqP p) -surjective_pairing mem_nth.
  Qed.  

 Definition swap_triple x : B := match x with (s, r, o) => (o, r, s) end.

 End TripleDict.

 (*==============================================================================================================*)

 (* Simplify notation for swapping triples in sequences *)
 Definition swap { T : eqType } s := map (swap_triple T) s.

 (* makePred2 predicate on object is compatible with FindAns *)
 Definition makePred2 rel sub : query_pred := fun E x => (sub, rel, x) \in E.

 (** 
    Note: Any way of having a single predicate? FindAns is defined in the current way as 
    sub_rel is easier defined to check subject, relation compared to object, relation.
    Thus makePred2 is used to construct predicates for querying.
 **)

 (* query_pred for edges of (bc_maliaU, hasPersonU, _) form *)
 Check makePred2 hasPersonU bc_maliaU. 

 (* With (swap edgeL) we can check if bc_sashaU is one such vertex *)
 Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_sashaU.

 (* Query/Type to find all term related to bc_maliaU by hasPersonU *)
 Check query_type vertexL edgeL (makePred2 hasPersonU bc_maliaU).

 (**
   Objective: 
   Compute (makePred2 rel sub el) x == true <=> x : query_type (makePred2 rel sub el)
 **)

 Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_sashaU == true.
 Compute bc_sashaU \in (makePred2 hasFatherU barackU (swap edgeL)).
 Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

 Theorem barack_BC : query_type vertexL (swap edgeL) (makePred2 hasFatherU barackU).
 Proof. by apply/Answer/(FindAns _ default_edgeU _ _ _ _). Defined.

 Compute (makePred2 hasFatherU barackU (swap edgeL)) barack_BC == true.

 Compute bc_maliaU == barack_BC.

 (* This expression is of type Set which is at the wrong level. *)
 (* now I think this is at the right level for us to do the query-as-types *)
 Check query_type vertexL edgeL (makePred2 hasFatherU barackU) : Set. 

 (**
   This goal of
                 e : personP x == true  <==> x : personT 
   ... (thinking)
 **)

 (* Filtering is used to find all birthcerts with hasFatherU relation to barackU *)
 Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

 (* Examples of querying with query_type *)
 Theorem bc_malia_Person : query_type vertexL edgeL (makePred2 hasPersonU bc_maliaU).
 Proof. apply: Answer. rewrite/makePred2. apply: (FindAns _ default_edgeU _ _ _ _); done.
 Defined.
 Compute maliaU == bc_malia_Person.
  
 Theorem bc_sasha_Person : query_type vertexL edgeL (makePred2 hasPersonU bc_sashaU).
 Proof. by apply/Answer/(FindAns _ default_edgeU _ _ _ _). Defined.

 Ltac answer := by apply/Answer/(FindAns _ default_edgeU _ _ _ _).

 Theorem malia_BC : query_type vertexL (swap edgeL) (makePred2 hasPersonU maliaU).
 Proof. answer. Defined.

 Compute bc_maliaU == malia_BC.


 (*==============================================================================================================*)
 (* Continue from here *)

 (**
                 e : personP x == true  <==> x : personT 
 **)
 (* Filtering to return possible answers *)
 Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

 (* pred vertexT *)
 Check (makePred2 hasFatherU barackU (swap edgeL)).

 (* Using as a predicate *)
 Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_maliaU.

 (* Using the predicate, construct a type : Set. Specifically this is the type of birth certs with barack father *)
 Check query_type vertexL edgeL (makePred2 hasFatherU barackU) : Type.

 (** Attempt reflection for query_type with constructor memT (membership true), cannot formulate memF
    as it is of type Set and there is no negation for it. **)

 Inductive qtreflect (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (b : bool) :=
 | memT (x : query_type vl el qp)          (e : (qp el x) = true).

 Check memT.
 (* memT : forall (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (b : bool) (x : query_type vl el qp),
                  qp el x = true -> qtreflect qp vl el b *)
 Check ReflectT.
 Lemma try (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (x : query_type vl el qp) : (qp el x = true).
 Proof. case: x => a b. 




 (*==============================================================================================================*)


 (* query_type for the person type *)
 Definition personT := query_type vertexL edgeL personP.
 Definition testT := query_type vertexL (swap edgeL) (makePred2 hasPersonU maliaU).
  
 (* filtering allows us to list the uris of type person *)
 Compute filter (personP edgeL) vertexL.
 Compute filter (defaultP edgeL) vertexL.

 Check [eqType of testT].
 Check [choiceType of personT].
 Check [countType of personT].
 Check [finType of testT].

 Definition barack := Answer vertexL edgeL personP barackU erefl.
 Check (personP edgeL).
 Compute barackU \in (personP edgeL).

 Check barack : personT.
 Check nat_eqType. Check personT.
 Print nat_eqType.

 Compute barack == barack.
	From mathcomp Require Import all_ssreflect.

	From void Require Import void.
	From deriving Require Import deriving.

	Require Import Coq.Strings.String.
	Open Scope string_scope.

	(* Deriving the type structures of string *)
	Canonical string_indType := Eval hnf in IndType _ _ [indMixin for string_rect].
	Canonical string_eqType := Eval hnf in EqType string [derive eqMixin for string].
	Canonical string_choiceType := Eval hnf in ChoiceType string [derive choiceMixin for string].
	Canonical string_countType := Eval hnf in CountType string [derive countMixin for string].

	Inductive uri : Type := Build_uri (s : string).
	Definition defaultU := Build_uri "default".

	(* Deriving the type structures of uri *)
	Definition uri_indMixin := Eval hnf in [indMixin for uri_rect].
	Canonical uri_indType := Eval hnf in IndType _ _ uri_indMixin.
	Canonical uri_eqType := Eval hnf in EqType uri [derive eqMixin for uri].
	Canonical uri_choiceType := Eval hnf in ChoiceType uri [derive choiceMixin for uri].
	Canonical uri_countType := Eval hnf in CountType uri [derive countMixin for uri].

	Notation vertexT := uri.
	Notation edgeT := (uri * uri * uri)%type.
	Definition default_edgeU := (defaultU,defaultU,defaultU).

	Section Query.

	Variable V : seq vertexT.
	Variable E : seq edgeT.

	Definition query_pred := seq edgeT -> pred vertexT.

	(* we use && to connect the two fields together to enable boolean predicate subtyping *)
	Record query_type (qp: query_pred) := Answer { query_uri :> uri ; query_uriP : query_uri \in (filter (qp E) V) }.

	(*
	Record query_type (qp: query_pred) := Answer { query_uri :> uri ; query_uriP : query_uri \in _ : (query_uri \in V) && ((E, query_uri) \in qp)}.
	*)

	(* Building the instances of subType, eqType for query_type *)
	Canonical queryt_subType (qp:query_pred) := Eval hnf in [subType for query_uri qp].
	Definition queryt_eqMixin (qp:query_pred) := Eval hnf in [eqMixin of (query_type qp) by <:].
	Canonical queryt_eqType (qp:query_pred) := Eval hnf in EqType (query_type qp) (queryt_eqMixin qp).
	Definition queryt_choiceMixin (qp:query_pred) := Eval hnf in [choiceMixin of (query_type qp) by <:].
	Canonical queryt_choiceType (qp:query_pred) := Eval hnf in ChoiceType (query_type qp) (queryt_choiceMixin qp).
	Definition queryt_countMixin (qp:query_pred) := Eval hnf in [countMixin of (query_type qp) by <:].
	Canonical queryt_countType (qp:query_pred) := Eval hnf in CountType (query_type qp) (queryt_countMixin qp).

	Definition queryt_enum (qp:query_pred) : seq (query_type qp) := undup (pmap insub (filter (qp E) V)).

	Lemma mem_queryt_enum (qp:query_pred) (x : query_type qp) : x \in (queryt_enum qp).
	Proof. by rewrite mem_undup mem_pmap -valK map_f ?query_uriP. Qed.

	Fact queryt_axiom (qp:query_pred) : Finite.axiom (queryt_enum qp).
	Proof. exact: Finite.uniq_enumP (undup_uniq _) (mem_queryt_enum qp). Qed.

	Definition queryt_finMixin (qp:query_pred) := Finite.Mixin (queryt_countMixin qp) (queryt_axiom qp).
	Canonical queryt_finType (qp:query_pred) := Eval hnf in FinType (query_type qp) (queryt_finMixin qp).

	End Query.

	(* Building the uris for some strings *)
	Definition personU := Build_uri "person".
	Definition birthcertU := Build_uri "birthcert".

	Definition barackU := Build_uri "barack".
	Definition michelleU := Build_uri "michelle".
	Definition maliaU := Build_uri "malia".
	Definition sashaU := Build_uri "sasha".

	Definition bc_maliaU := Build_uri "birthcert_malia".
	Definition bc_sashaU := Build_uri "birthcert_sasha".

	Definition hasTypeU := Build_uri "hasType".
	Definition hasPersonU := Build_uri "hasPerson".
	Definition hasFatherU := Build_uri "hasFather".

	Definition vertexL := [:: personU; birthcertU; barackU; michelleU; maliaU; sashaU;
	bc_maliaU; bc_sashaU;
	hasTypeU; hasPersonU; hasFatherU].

	Definition edgeL := [:: (barackU,hasTypeU,personU); (michelleU,hasTypeU,personU);
	(maliaU,hasTypeU,personU); (sashaU,hasTypeU,personU);
	(bc_maliaU,hasTypeU,birthcertU); (bc_sashaU,hasTypeU,birthcertU);
	(bc_maliaU,hasPersonU,maliaU); (bc_sashaU,hasPersonU,sashaU);
	(bc_maliaU,hasFatherU,barackU); (bc_sashaU,hasFatherU,barackU)].

	(* Specification of a predicate to determine the type of a uri *)

	(* makePred1 is a predicate on the subject, useful for checking membership of terms to a type *)
	Definition makePred1 rel obj : query_pred := fun E x => (x, rel, obj) \in E.

	Definition personP := makePred1 hasTypeU personU.
	Definition birthcertP := makePred1 hasTypeU birthcertU.
	Definition defaultP := makePred1 hasTypeU defaultU.

	Compute barackU \in personP edgeL.
	Compute bc_maliaU \in birthcertP edgeL.
	Compute barackU \in birthcertP edgeL.

	Section TripleDict.

	Variable A : eqType.
	Implicit Type (s r : A).
	Implicit Type (vl : seq A).
	Notation B := (AAA)%type.
	Variable (e : B).
	Implicit Type (el : seq B).

	(*
	Generalized definition of query_pred
	Definition gen_query_pred := seq B -> pred A.
	*)

	(* Predicate on edge for given subject and relation *)
	Definition sub_rel s r (triple : B) := (triple.1 == (s,r)).

	(* Returns a triple containing the given subject and relation. nth ensures only the first triple is returned. *)
	Definition sub_rel2triple s r el := nth e el (find (sub_rel s r) el).

	(*
	Definition getObj s r : qp := fun el => fun x => (sub_rel2triple s r el) == (s, r, x).

	Lemma FindObj s r vl el : has (sub_rel s r) el -> (sub_rel2triple s r el).2 \in vl
	-> (sub_rel2triple s r el).2 \in [seq x <- vl \| getObj s r el x].
	Proof. pose H := has (sub_rel s r) el.
	have lem1 : H -> (sub_rel2triple s r el).1 == (s,r). { apply/nth_find. }
	move=> h m. move: (lem1 h)=> p.
	by rewrite mem_filter m /getObj -(eqP p) -surjective_pairing eq_refl.
	Qed.
	*)

	(* Lemma that finds the answer from the query *)
	Lemma FindAns s r vl el : has (sub_rel s r) el -> (sub_rel2triple s r el).2 \in vl
	-> (sub_rel2triple s r el).2 \in [seq x <- vl \| (s, r, x) \in el].
	Proof.
	pose H := has (sub_rel s r) el.
	have lem1 : H -> (sub_rel2triple s r el).1 == (s,r). { apply/nth_find. }
	have lem2 : H -> (find (sub_rel s r) el) < size el. { by rewrite -has_find. }
	move => h m; move: (lem1 h) => p; move: (lem2 h) => q.
	(* rewrite mem_filter. rewrite m. rewrite -{1}(eqP p). rewrite -surjective_pairing. rewrite mem_nth. *)
	by rewrite mem_filter m -{1}(eqP p) -surjective_pairing mem_nth.
	Qed.

	Definition swap_triple x : B := match x with (s, r, o) => (o, r, s) end.

	End TripleDict.

	(==============================================================================================================)

	(* Simplify notation for swapping triples in sequences *)
	Definition swap { T : eqType } s := map (swap_triple T) s.

	(* makePred2 predicate on object is compatible with FindAns *)
	Definition makePred2 rel sub : query_pred := fun E x => (sub, rel, x) \in E.

	(**
	Note: Any way of having a single predicate? FindAns is defined in the current way as
	sub_rel is easier defined to check subject, relation compared to object, relation.
	Thus makePred2 is used to construct predicates for querying.
	**)

	(* query_pred for edges of (bc_maliaU, hasPersonU, _) form *)
	Check makePred2 hasPersonU bc_maliaU.

	(* With (swap edgeL) we can check if bc_sashaU is one such vertex *)
	Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_sashaU.

	(* Query/Type to find all term related to bc_maliaU by hasPersonU *)
	Check query_type vertexL edgeL (makePred2 hasPersonU bc_maliaU).

	(**
	Objective:
	Compute (makePred2 rel sub el) x == true <=> x : query_type (makePred2 rel sub el)
	**)

	Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_sashaU == true.
	Compute bc_sashaU \in (makePred2 hasFatherU barackU (swap edgeL)).
	Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

	Theorem barack_BC : query_type vertexL (swap edgeL) (makePred2 hasFatherU barackU).
	Proof. by apply/Answer/(FindAns _ default_edgeU _ _ _ _). Defined.

	Compute (makePred2 hasFatherU barackU (swap edgeL)) barack_BC == true.

	Compute bc_maliaU == barack_BC.

	(* This expression is of type Set which is at the wrong level. *)
	(* now I think this is at the right level for us to do the query-as-types *)
	Check query_type vertexL edgeL (makePred2 hasFatherU barackU) : Set.

	(**
	This goal of
	e : personP x == true <==> x : personT
	... (thinking)
	**)

	(* Filtering is used to find all birthcerts with hasFatherU relation to barackU *)
	Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

	(* Examples of querying with query_type *)
	Theorem bc_malia_Person : query_type vertexL edgeL (makePred2 hasPersonU bc_maliaU).
	Proof. apply: Answer. rewrite/makePred2. apply: (FindAns _ default_edgeU _ _ _ _); done.
	Defined.
	Compute maliaU == bc_malia_Person.

	Theorem bc_sasha_Person : query_type vertexL edgeL (makePred2 hasPersonU bc_sashaU).
	Proof. by apply/Answer/(FindAns _ default_edgeU _ _ _ _). Defined.

	Ltac answer := by apply/Answer/(FindAns _ default_edgeU _ _ _ _).

	Theorem malia_BC : query_type vertexL (swap edgeL) (makePred2 hasPersonU maliaU).
	Proof. answer. Defined.

	Compute bc_maliaU == malia_BC.


	(==============================================================================================================)
	(* Continue from here *)

	(**
	e : personP x == true <==> x : personT
	**)
	(* Filtering to return possible answers *)
	Compute filter (makePred2 hasFatherU barackU (swap edgeL)) vertexL.

	(* pred vertexT *)
	Check (makePred2 hasFatherU barackU (swap edgeL)).

	(* Using as a predicate *)
	Compute (makePred2 hasFatherU barackU (swap edgeL)) bc_maliaU.

	(* Using the predicate, construct a type : Set. Specifically this is the type of birth certs with barack father *)
	Check query_type vertexL edgeL (makePred2 hasFatherU barackU) : Type.

	(** Attempt reflection for query_type with constructor memT (membership true), cannot formulate memF
	as it is of type Set and there is no negation for it. **)

	Inductive qtreflect (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (b : bool) :=
	\| memT (x : query_type vl el qp) (e : (qp el x) = true).

	Check memT.
	(* memT : forall (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (b : bool) (x : query_type vl el qp),
	qp el x = true -> qtreflect qp vl el b *)
	Check ReflectT.
	Lemma try (qp : query_pred) (vl : seq vertexT) (el : seq edgeT) (x : query_type vl el qp) : (qp el x = true).
	Proof. case: x => a b.




	(==============================================================================================================)


	(* query_type for the person type *)
	Definition personT := query_type vertexL edgeL personP.
	Definition testT := query_type vertexL (swap edgeL) (makePred2 hasPersonU maliaU).

	(* filtering allows us to list the uris of type person *)
	Compute filter (personP edgeL) vertexL.
	Compute filter (defaultP edgeL) vertexL.

	Check [eqType of testT].
	Check [choiceType of personT].
	Check [countType of personT].
	Check [finType of testT].

	Definition barack := Answer vertexL edgeL personP barackU erefl.
	Check (personP edgeL).
	Compute barackU \in (personP edgeL).

	Check barack : personT.
	Check nat_eqType. Check personT.
	Print nat_eqType.

	Compute barack == barack.