zunction/sw_pred.v

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.