zunction/sw_pred.v

Able to select the nth answer for a query with multiple answers:

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.

Section uri.

Variables A B : eqType.
Variable x0 : A * B.
Variable a a0: A.
Variable b : B.
Variable al : seq A.
Variable l : seq (A * B).

Definition fstpred (p : A * B) := (p.1 == a).
Definition sndpred (p : A * B) := (p.2 == b).
Definition fst2pair := nth x0 l (find fstpred l).
Definition snd2pair := nth x0 l (find sndpred l).
Definition fst2snd := fst2pair.2.
Definition snd2fst := snd2pair.1.

Lemma fst2pair1P : has fstpred l -> fst2pair.1 = a.
Proof. by move=> h; apply/eqP; move: h; apply/nth_find. Qed.
Lemma snd2pair2P : has sndpred l -> snd2pair.2 = b.
Proof. by move=> h; apply/eqP; move: h; apply/nth_find. Qed.

Lemma fpredhas_find : has fstpred l -> (find fstpred l) < size l.
Proof. by rewrite has_find. Qed.
Lemma spredhas_find : has sndpred l -> (find sndpred l) < size l.
Proof. by rewrite has_find. Qed.

Lemma fst2sndP : has fstpred l -> (a, fst2snd) \in l.
Proof. move=> h; pose x := fst2pair; have: x.1 = a. { apply/fst2pair1P/h. }
       move=> g; rewrite -{1} g; rewrite/fst2snd-/x.
       by rewrite -surjective_pairing; apply/mem_nth/fpredhas_find. Qed.
Lemma snd2fstP : has sndpred l -> (snd2fst, b) \in l.
Proof. move=> h; pose x := snd2pair; have: x.2 = b. { apply/snd2pair2P/h. }
       move=> g; rewrite -{1} g; rewrite/snd2fst-/x.
       by rewrite -surjective_pairing; apply/mem_nth/spredhas_find. Qed.

Lemma headinlist : has (pred1 (head a0 al)) al-> (head a0 al) \in al.
Proof. by move=> h; rewrite -has_pred1. Qed.

Lemma inlist : forall n, has (pred1 (nth a0 al n)) al -> nth a0 al n \in al.
Proof. by move=> h; rewrite -has_pred1. Qed.


End uri.

(* 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].

Definition query_pred := pred uri.
Record query_type (qp: query_pred) := Answer { query_uri :> uri ; _ : query_uri \in qp}.

(* Building the uris *)
Definition barackU := Build_uri "barack".
Definition michelleU := Build_uri "michelle".
Definition maliaU := Build_uri "malia".
Definition sashaU := Build_uri "sasha".

Definition personuriL := [:: barackU; michelleU; maliaU; sashaU].
Definition personP : query_pred := mem personuriL.

Definition personT := query_type personP. 
Definition barack := Answer personP barackU erefl.
(* eqType not established *)
Fail Compute barack == barack.

(* Building eqType instances for all 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).
(* FINTYPES ARE STILL UNSOLVED...
 
Definition queryt_finMixin (qp:query_pred) := Eval hnf in [finMixin of (query_type qp) by <:].
Canonical queryt_finType (qp:query_pred) := Eval hnf in FinType (query_type qp) (queryt_finMixin qp).
*)
(* eqTypes available now *)
Compute barack == barack.

Definition bc_maliaU := Build_uri "birthcert_malia".
Definition bc_sashaU := Build_uri "birthcert_sasha".
Definition birthcerturiL := [:: bc_maliaU; bc_sashaU].
Definition birthcertP : pred uri := mem birthcerturiL.
Definition birthcertT := query_type birthcertP.

Compute bc_maliaU \in birthcertP.
Compute barackU \in birthcertP.

Definition bc_malia := Answer birthcertP bc_maliaU erefl.
Eval compute in bc_malia == bc_malia.

Definition bc_childL := [:: (bc_maliaU, maliaU); (bc_sashaU, sashaU)].
Definition bc_child : pred (uri*uri) := mem bc_childL.
Compute (bc_maliaU,maliaU) \in bc_child.
Compute (bc_maliaU,sashaU) \in bc_child.
Compute bc_child (bc_maliaU,maliaU).

Section Proj.

Variable A : eqType.
Variable a : A.

Definition fstP (pair_pred : pred (uri*uri)) (fstU : uri): pred uri := fun x => pair_pred (fstU, x).
Definition sndP (pair_pred : pred (uri*uri)) (sndU : uri): pred uri := fun x => pair_pred (x, sndU).
End Proj.

Definition bc_child_1P (bc:uri) := fstP bc_child bc.
Definition bc_child_2P (ch:uri) := sndP bc_child ch.

Definition bc_child_1T (bc:uri) := query_type (bc_child_1P bc).
Definition bc_child_2T (ch:uri) := query_type (bc_child_2P ch). 

Ltac dqt_snd :=  by apply/Answer/(fst2sndP _ _ (defaultU,defaultU)).
Ltac dqt_fst := by apply/Answer/(snd2fstP _ _ (defaultU,defaultU)).


Theorem bc_malia_child : bc_child_1T bc_maliaU.
Proof. by apply/Answer/(fst2sndP _ _ (defaultU,defaultU)). Defined.

Compute maliaU == bc_malia_child.

Theorem malia_bc : bc_child_2T maliaU.
Proof. by apply/Answer/(snd2fstP _ _ (defaultU,defaultU)). Defined.

Compute bc_maliaU == malia_bc.
Compute filter (bc_child_1P bc_maliaU) personuriL.

Definition bc_fatherL := [:: (bc_maliaU, barackU); (bc_sashaU, barackU)].
Definition bc_father : pred (uri*uri) := mem bc_fatherL.

Definition bc_father_1P (bc:uri) := fstP bc_father bc.
Definition bc_father_2P (f:uri) := sndP bc_father f.

Definition bc_father_1T (bc:uri) := query_type (bc_father_1P bc).
Definition bc_father_2T (f:uri) := query_type (bc_father_2P f).


Theorem bc_malia_father : bc_father_1T bc_maliaU.
Proof. dqt_snd. Defined.

Compute barackU == bc_malia_father.

(* Demo of query father *)
Definition bc_of_personL (x : uri) := filter (sndP bc_child x) birthcerturiL.
Compute bc_of_personL maliaU.

Definition father_of_bcL (x : uri) := filter (fstP bc_father (head defaultU (bc_of_personL x))) personuriL.
Compute father_of_bcL maliaU.
Definition father_of_bcP (x: uri):= mem (father_of_bcL x).

Definition father_T (x : uri) := query_type (father_of_bcP x).
Compute barackU \in (father_of_bcL sashaU).
Compute barackU \in (father_of_bcP sashaU). 

Theorem malia_father : father_T maliaU.
Proof. by apply/Answer/(headinlist _ defaultU). Defined.

Theorem malia_father' : father_T maliaU.
Proof. by apply/Answer/(inlist _ defaultU _ 0 ). Defined.

Theorem sasha_father : father_T sashaU.
Proof. by apply/Answer/(headinlist _ defaultU). Defined.

Compute barackU == malia_father.
Compute barackU == malia_father'.
Compute barackU == sasha_father.

(* Demo of query daughter *)
Definition bc_of_fatherL (x : uri) := filter (sndP bc_father x) birthcerturiL.
Compute bc_of_fatherL barackU.

(* Definition child_of_bcL (x : uri) := filter (fstP bc_child (head defaultU (bc_of_fatherL x))) personuriL. *)
Definition child_of_bcL (x : uri) n := filter (fstP bc_child (nth defaultU (bc_of_fatherL x) n)) personuriL.
Compute child_of_bcL barackU 1.
Definition child_of_bcP (x: uri) n := mem (child_of_bcL x n).

Compute sashaU \in child_of_bcP barackU 1.
Compute maliaU \in child_of_bcP barackU 0.
Definition child_T (x : uri) n := query_type (child_of_bcP x n).

(* from what we have below, we see that we can choose the different possible answers
   by giving the number n that will give us the nth answer. Turns out that inlist and headinlist 
   does not matter after changing the _head_ to _nth_ in the definition of child_of_bcL above.
*)

Theorem barack_child0 : child_T barackU 0.
Proof. by apply/Answer/(inlist _ defaultU _ 0). Defined.

Compute maliaU == barack_child0.

Theorem barack_child1 : child_T barackU 1.
Proof. by apply/Answer/(headinlist _ defaultU). Defined.

Compute sashaU == barack_child1.

my_pred.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.

(**
 This file extends the definition name suffix conventions as follows:
   F -- filter for obtaining terms satisfying the predicate
   L -- sequence of terms 
   P -- collective predicate based on a list
   T -- type formed with a collective predicate 
   U -- terms of uri type                                                **)

Section Dict.

Variables A B : eqType.
Variable x0 : A * B.
Implicit Type a : A.
Implicit Type b : B.
Implicit Type l : seq (A * B).

Definition key a (p : A * B) := (p.1 == a).
Definition key2pair a l := nth x0 l (find (key a) l).
Definition key2value a l := (key2pair a l).2.

Definition value b (p : A * B) := (p.2 == b).
Definition value2pair b l := nth x0 l (find (value b ) l).
Definition value2key b l := (value2pair b l).1.

Lemma has_key2value a l: has (key a) l -> (a, key2value a l) \in l.
Proof. 
pose H := has (key a) l.
have lem1 : H -> (key2pair a l).1 == a. { apply/nth_find. } 
have lem2 : H -> (find (key a) l) < size l. { by rewrite -has_find. } 
by move => h; move: (lem1 h) => p; move: (lem2 h) => q;
rewrite -{1}(eqP p) -surjective_pairing; apply /mem_nth.
Qed.

Lemma has_value2key b l: has (value b) l -> (value2key b l, b) \in l.
Proof. 
pose H := has (value b) l.
have lem1 : H -> (value2pair b l).2 == b. { apply/nth_find. } 
have lem2 : H -> (find (value b) l) < size l. { by rewrite -has_find. } 
by move => h; move: (lem1 h) => p;  move: (lem2 h) => q;
rewrite -{2}(eqP p) -surjective_pairing; apply /mem_nth. 
Qed.

End Dict.

(* 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].

(* Defining the basic type for querying with predicates *)
Definition query_pred := pred uri.
Record query_type (qp: query_pred) := Answer { query_uri :> uri ; _ : query_uri \in qp}.

(* Building the uris for some strings *)
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".

(* Subtyping specific uris to person type *)
Definition personuriL := [:: barackU; michelleU; maliaU; sashaU].
Definition personP : query_pred := mem personuriL.
Definition personT := query_type personP. 

(* a term of type personT can be constructed in this manner *)
Definition barack := Answer personP barackU erefl.
Check barack : personT.

Fail Compute barack == barack.

(* 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).

(* Now we have eqType up and running for any subtypes formed from query_type *)
Compute barack == barack.

(* Building the instances of choiceType, countType for query_type *)
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).

(* Specifying the birthcert uris to birthcert type *)
Definition birthcerturiL := [:: bc_maliaU; bc_sashaU].
Definition birthcertP : pred uri := mem birthcerturiL.
Definition birthcertT := query_type birthcertP.

(* Sequence of pairs list out all the pairs related by the same relation *)

(* Birthcerts to the person of the birthcert *)
Definition bc_personL := [:: (bc_maliaU, maliaU); (bc_sashaU, sashaU)].
Definition bc_person : pred (uri * uri) := mem bc_personL.

(* Birthcerts to the father of the birthcert owner *)
Definition bc_fatherL := [:: (bc_maliaU, barackU); (bc_sashaU, barackU)].
Definition bc_father : pred (uri * uri) := mem bc_fatherL.

(* How to do a direct query *)

Section Query.

Variable A : eqType.
Implicit Type al : seq A.


Definition fstP (pair_pred : pred (uri*uri)) (fstU : uri): pred uri := fun x => pair_pred (fstU, x).
Definition sndP (pair_pred : pred (uri*uri)) (sndU : uri): pred uri := fun x => pair_pred (x, sndU).

Lemma headinlist a0 al : has (pred1 (head a0 al)) al-> (head a0 al) \in al.
Proof. by move=> h; rewrite -has_pred1. Qed.

Lemma inlist a0 al : forall n, has (pred1 (nth a0 al n)) al -> nth a0 al n \in al.
Proof. by move=> h; rewrite -has_pred1. Qed.

End Query.

Definition bc_person_1P (bc: uri) := fstP bc_person bc.
Definition bc_person_2P (ch: uri) := sndP bc_person ch.

Definition bc_person_1T (bc: uri) := query_type (bc_person_1P bc).
Definition bc_person_2T (ch: uri) := query_type (bc_person_2P ch).

Ltac dqt_k2v := by apply/Answer/(has_key2value _ _ (defaultU, defaultU)).
Ltac dqt_v2k := by apply/Answer/(has_value2key _ _ (defaultU, defaultU)).

(* Query for the value given the key: returns person of the birthcert *)
Theorem malia_of_bc : bc_person_1T bc_maliaU.
Proof. dqt_k2v. Defined.

Compute maliaU == malia_of_bc.

(* Query for the key given the value: returns the birthcert of the person *)
Theorem bc_of_malia : bc_person_2T maliaU.
Proof. dqt_v2k. Defined.

Compute bc_maliaU == bc_of_malia.

(* Now we want to query for the father of malia *)

Definition bc_father_1P (bc: uri) := fstP bc_father bc.
Definition bc_father_2P (f: uri) := sndP bc_father f.

Definition bc_father_1T (bc: uri) := query_type (bc_father_1P bc).
Definition bc_father_2T (f: uri) := query_type (bc_father_2P f).

(* Filters all the birthcert related to a given person *)
Definition bc_of_personF (p : uri) := filter (sndP bc_person p) birthcerturiL.

(* Filters all the fathers related to a given birthcert *)
Definition father_of_personF (p : uri) n := filter (fstP bc_father (nth defaultU (bc_of_personF p) n)) personuriL.

(*  Collective predicate given a person *)
Definition father_of_personP (x: uri) n := mem (father_of_personF x n).
Definition father_of_personT (x: uri) n := query_type (father_of_personP x n).

Theorem malia_father : father_of_personT maliaU 0.
Proof. by apply/Answer/(inlist _ defaultU  _ 0). Defined.

Compute barackU == malia_father.

(* Now we want to query for the children of barack *)

(* Filters all the birthcert related to a given person *)
Definition bc_of_fatherF (p : uri) := filter (sndP bc_father p) birthcerturiL.

(* Filters all the person of the birthcert *)
Definition child_of_personF (p : uri) n := filter (fstP bc_person (nth defaultU (bc_of_fatherF p) n)) personuriL.

(*  Collective predicate given a person *)
Definition child_of_personP (x: uri) n := mem (child_of_personF x n).
Definition child_of_personT (x: uri) n := query_type (child_of_personP x n).

(* from what we have below, we see that we can choose the different possible answers
   by giving the number n that will give us the nth answer. Turns out that inlist and headinlist 
   does not matter after changing the _head_ to _nth_ in the definition of child_of_bcL above.
*)

Theorem barack_child0 : child_of_personT barackU 0.
Proof. by apply/Answer/(inlist _ defaultU _ 0). Defined.

Compute maliaU == barack_child0.

Theorem barack_child1 : child_of_personT barackU 1.
Proof. by apply/Answer/(inlist _ defaultU _ 0). Defined.

Compute sashaU == barack_child1.

Print bc_personL.

Print bc_fatherL.

Fixpoint samekey {A B : eqType} (a : A) (s : seq (A * B)) :=
  match s with
  | x :: s' => if x.1 == a then x.2 :: samekey a s' else samekey a s'
  | [::] => [::]                                              
  end.

Compute samekey 1 [:: (1,true); (1,false); (2,true)].
Compute [seq (5, i) | i <- samekey 1 [:: (1,true); (1,false); (2,true)]].

Fixpoint valueglue {A B C : eqType} (s : seq (A * B)) (t : seq (A * C))  {struct s} :=
  match s  with
  | x :: s' => if has (key _ _ x.1) t then cat [seq (x.2, i) | i <- samekey x.1 t ] (valueglue s' t) else valueglue s' t 
  | [::] => [::]                                                              
  end.                                                             


Definition l := [:: (1, true); (1, false); (3, true)].
Definition l' := [:: (1, false); (2, true); (3, true)].

Compute valueglue l l' .


Compute valueglue bc_personL bc_fatherL.

Definition child_fatherL := valueglue bc_personL bc_fatherL.
Definition child_father := mem child_fatherL.
Definition child_father_1P (ch:uri) :=  (fstP child_father ch).
Definition child_father_1T (ch:uri) := query_type (child_father_1P ch).
Definition child_father_2P (f:uri) :=  (sndP child_father f).
Definition child_father_2T (f:uri) := query_type (child_father_2P f).


Theorem fuu : child_father_1T maliaU.
Proof. dqt_k2v. Defined.

Compute barackU == fuu.

Theorem guu : child_father_2T barackU.
Proof. dqt_v2k. Defined.

Compute maliaU == guu.

Compute child_father_2P barackU barackU.