zunction/tings_pred.v

Thinking about how to get multiple answers back:

From mathcomp Require Import all_ssreflect.

Inductive ting := a | b | c | d | aa | bb | cc | dd | default.
Scheme Equality for ting.
Lemma eq_tingP : Equality.axiom ting_beq.
Proof. by do 2!case; constructor. Qed.
Definition ting_eqMixin := Equality.Mixin eq_tingP.
Canonical ting_eqType := Equality.Pack ting_eqMixin.

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

Definition singleL := [:: a; b; c; d].
Definition singleP : query_pred := mem singleL. 

Definition doubleL := [:: aa; bb; cc; dd].
Definition doubleP : query_pred := mem doubleL. 

Definition singleT := query_type singleP.
Definition doubleT := query_type doubleP.

Definition a1 := Answer singleP a erefl.

Canonical queryt_subType (qp:query_pred) := Eval hnf in [subType for query_ting 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).

Compute a \in singleP.
Compute aa \in singleP.
Compute aa \in doubleP.

Definition sdL := [:: (a, aa); (b, bb); (c, cc); (d, dd); (a, dd)]. Check sdL.
Definition sdP : pred (ting * ting) := mem sdL.

Compute (a, bb) \in sdP.
Compute (b, bb) \in sdP.

Definition sd_1P (s : ting) : pred ting := fun x => sdP (s, x).
Definition sd_2P (d : ting) : pred ting := fun x => sdP (x, d).

Compute filter (sd_1P a) doubleL.
Check filter (sd_1P a) doubleL.
Compute filter (sd_2P dd) singleL.

Section uri.

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

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

Lemma cfst2pair1P : has fstpred l -> fst2pair.1 = a.
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 fst2sndP : has fstpred l -> (a, fst2snd) \in l.
Proof. move=> h; pose x := fst2pair; have: x.1 = a. { apply/cfst2pair1P/h. }
       move=> g; rewrite -{1} g; rewrite/fst2snd-/x.
       by rewrite -surjective_pairing; apply/mem_nth/fpredhas_find. Qed.

End uri.

Definition sd_1T (d : ting) := query_type (sd_1P d).

Definition fuu : sd_1T a.
Proof. by apply/Answer/(fst2sndP _ _ (default,default)). Defined.

Definition multi_sd1P (s : ting) : pred (seq ting) := mem [:: (filter (sd_1P s) doubleL)].

Definition multi_query_pred := pred (seq ting).

Record multi_query_type (qp: multi_query_pred) := Answers { query_tings :> seq ting ; _ : query_tings \in qp}.

Definition multi_sd_1T (d : ting) := multi_query_type (multi_sd1P d).

Definition fuus : multi_sd_1T a.
Proof.
apply: Answers. Check @fst2sndP.
apply: (fst2sndP _ _ [:: [:: (default, default)]]).  

(* reason why fst2sndP fails is because it was designed for pairs *)

Late night (early morning) work

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 : A.
Variable b : B.
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.

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.

Record father (x : uri) :=
  { val_bc : bc_child_2T x ;
    val_father :> bc_father_1T val_bc ;    
  }.
Check val_father.
Canonical father_subType (x:uri) := Eval hnf in [subType for (val_father x)].
Definition father_eqMixin (qp:query_pred) := Eval hnf in [eqMixin of (query_type qp) by <:].
Canonical father_eqType (qp:query_pred) := Eval hnf in EqType (query_type qp) (queryt_eqMixin qp).

Theorem malia_father : father maliaU.
Proof. unshelve apply:Build_father.
by apply/Answer/(snd2fstP _ _ (defaultU, defaultU)).
by apply/Answer/(fst2sndP _ _ (defaultU, defaultU)).
Defined.

Print malia_father.
Check bc_malia_father : uri.
Compute barackU == malia_father.