Skip to content

Instantly share code, notes, and snippets.

@zunction

zunction/pred_type.v

Last active April 28, 2020 07:42
Show Gist options
  • Save zunction/013bb0a42c33480c97e1f9150fd2efce to your computer and use it in GitHub Desktop.
Save zunction/013bb0a42c33480c97e1f9150fd2efce to your computer and use it in GitHub Desktop.
Download ZIP
Code sharing to SW with reflection proofs
Raw
pred_type.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).
Definition E2V (E : seq edgeT) := undup ([seq e.1.1|e<-E]++[seq e.1.2|e<-E]++[seq e.2|e<-E]).
Section Query.
Variable E : seq edgeT.
Definition V : seq vertexT := E2V E.
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) }.
(* 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 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)].
Definition vertexL := E2V edgeL.
(* 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 personB := makePred1 hasTypeU personU.
Definition birthcertB := makePred1 hasTypeU birthcertU.
Definition defaultB := makePred1 hasTypeU defaultU.
Definition personT := query_type edgeL personB.
Compute barackU \in personB edgeL. (* x \in A *)
Compute (personB edgeL) barackU. (* P x *)
Compute bc_maliaU \in birthcertB edgeL.
Compute barackU \in birthcertB edgeL.
Lemma qp_filter (qp : query_pred) (u : uri) (E : seq edgeT) (_ : u \in (E2V E)) : (qp E u) -> (u \in filter (qp E) (E2V E)).
Proof. by move=> pt; rewrite mem_filter; apply /andP. Qed.
Lemma query_typeP {qp : query_pred} (u : uri) (E : seq edgeT) (pu : u \in (E2V E)):
reflect (exists x : (query_type E qp), u = x) (qp E u).
Proof. apply: (iffP idP).
by move=> pp; exists (Answer _ _ _ (qp_filter qp _ _ pu pp)).
by move=> [[a b] /= px]; move: b; rewrite mem_filter -px=> /andP[c d].
Qed.
Definition test (p : uri) (pv : p \in (E2V edgeL)) : (personB edgeL p) -> True.
Proof. do 2! move/(query_typeP p _ pv). move/(query_typeP p _ pv). move => [x xp]. done. Qed.
@zunction
Copy link
Author 

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.

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)}.

(* 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)). 
Check queryt_enum.
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 barackU := Build_uri "barack".
Definition michelleU := Build_uri "michelle".
Definition maliaU := Build_uri "malia".
Definition sashaU := Build_uri "sasha".
Definition hasTypeU := Build_uri "hasType".
Definition personU := Build_uri "person".
Definition bc_maliaU := Build_uri "birthcert_malia".
Definition bc_sashaU := Build_uri "birthcert_sasha".

Definition vertexL := [:: barackU;michelleU;maliaU;sashaU;hasTypeU;personU].
Definition edgeL := [:: (barackU,hasTypeU,personU); (michelleU,hasTypeU,personU); (maliaU,hasTypeU,personU); (sashaU,hasTypeU,personU)].

Definition personP : query_pred := fun E => fun x =>  (x,hasTypeU,personU) \in E.
Definition personT := query_type vertexL edgeL personP. 

Definition barack := Answer vertexL edgeL personP barackU erefl.

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

Compute barack == barack.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment