File GenericModel
(* From Coq Require Import ssreflect ssrfun ssrbool.
From stdpp Require Import base list list_numbers propset.
(* This is unset by stdpp. We need to set it again.*)
Set Transparent Obligations.
From Equations Require Import Equations.
(* Set Equations Transparent. *)
*)
Require Import Coq.Program.Equality. (* Dependent destruction *)
Require Import Coq.Logic.Classical_Prop. (* Proof irrelevance *)
From MatchingLogic.OPML Require Export OpmlModel.
Definition UnifiedCarrierInfo := Type.
Definition UnifiedCarrierFunctor : Type
:= Type → UnifiedCarrierInfo
.
Definition UnifiedCarrierCtorFamily
(UCF : UnifiedCarrierFunctor) (A : Type)
: Type
:= ((list nat)*(list A))%type → (* Choose a particuar constructor from the family, and arguments of the constructor from the underlying type *)
option (UCF A) (* maybe return something, and maybe not *)
.
Definition is_monotone (F : UnifiedCarrierFunctor)
: Type
:= ∀ x y, (x → y) → (F x → F y)
.
Record UnifiedCarrierComponent := {
ucc_functor : UnifiedCarrierFunctor ;
ucc_functor_monotone : is_monotone ucc_functor ;
ucc_ctor_family : ∀ A, UnifiedCarrierCtorFamily ucc_functor A ;
ucc_ctor_family_inj : ∀ A args1 args2 ret,
(ucc_ctor_family A args1 = Some ret) →
(ucc_ctor_family A args2 = Some ret) →
args1 = args2 ;
}.
(* We can bypass the check because of the `is_monotone` requirement. *)
#[bypass_check(positivity=yes)]
Inductive UnifiedCarrier
(F: UnifiedCarrierFunctor)
(pos : is_monotone F)
: Type :=
| c (st : F (UnifiedCarrier F pos))
.
Definition CompInvertorT
(UCC : UnifiedCarrierComponent)
: Type
:= ∀ (A : Type) (x : ucc_functor UCC A),
option ({ nla : ((list nat)*(list A))%type | ucc_ctor_family UCC A nla = Some x })
.
Definition CompSortedCarrierT
{Σ : OPMLSignature}
(s : opml_sort)
(UCC : UnifiedCarrierComponent)
(invertor : CompInvertorT UCC)
:=
∀ (A : Type) (x : ucc_functor UCC A), Prop
.
Record Component {Σ : OPMLSignature} := {
comp_UCC
: UnifiedCarrierComponent ;
comp_invertor
: CompInvertorT comp_UCC ;
comp_invertor_complete
: ∀
(A : Type)
(nla : ((list nat)*(list A))%type)
(x : ucc_functor comp_UCC A),
ucc_ctor_family comp_UCC A nla = Some x →
∃ pf,
comp_invertor A x = Some (exist _ nla pf)
;
(*
comp_sorted_carrier
: forall s, CompSortedCarrierT s comp_UCC comp_invertor
; *)
}.
Section constant.
Context
(UCI : UnifiedCarrierInfo)
.
Definition constant_UnifiedCarrierFunctor : UnifiedCarrierFunctor
:= fun _ ⇒ UCI
.
Lemma constant_UnifiedCarrierFunctor_monotone : is_monotone constant_UnifiedCarrierFunctor.
(* TODO *)
Definition constant_inversion
{A : Type}
(x : constant_UnifiedCarrierFunctor A)
:= 0.
End constant.
Program Definition bool_UCC : UnifiedCarrierComponent := {|
ucc_functor
:= constant_UnifiedCarrierFunctor bool ;
ucc_functor_monotone
:= constant_UnifiedCarrierFunctor_monotone bool ;
ucc_ctor_family
:= fun A nla ⇒
match nla with
| ([0], []) ⇒ Some true
| ([1], []) ⇒ Some false
| _ ⇒ None
end
;
|}.
Program Definition bool_component {Σ : OPMLSignature} : Component := {|
comp_UCC := bool_UCC ;
comp_invertor := fun A x ⇒
match x return option ({ nla : ((list nat)*(list A))%type | ucc_ctor_family bool_UCC A nla = Some x }) with
| true ⇒ Some (exist (fun y ⇒ ucc_ctor_family bool_UCC A y = Some true) ([0],([]):(list A)) erefl)
| false ⇒ Some (exist _ ([1],([]):(list A)) erefl)
end
;
comp_invertor_complete := _ ;
(*
comp_sorted_carrier := fun s A x => True
(* TODO we need to query the sort, whether it belongs to the Bool subsignature *)
; *)
|}.
Program Definition empty_component {Σ : OPMLSignature} : Component := {|
comp_UCC := {|
ucc_functor
:= constant_UnifiedCarrierFunctor Empty_set ;
ucc_functor_monotone
:= constant_UnifiedCarrierFunctor_monotone Empty_set ;
ucc_ctor_family
:= fun A nla ⇒ None ;
|};
comp_invertor :=
fun A x ⇒ match x with end
;
comp_invertor_complete
:= _;
|}.
Section paircomb_ucf.
Context
(F1 F2 : UnifiedCarrierComponent)
.
Definition paircomb_ucf_UnifiedCarrierFunctor : UnifiedCarrierFunctor
:=
fun A ⇒ ((ucc_functor F1 A)+(ucc_functor F2 A))%type
.
Lemma paircomb_ucf_UnifiedCarrierFunctor_monotone : is_monotone paircomb_ucf_UnifiedCarrierFunctor.
End paircomb_ucf.
Section paircomb.
Context
{Σ : OPMLSignature}
(C1 C2 : Component)
.
Program Definition paircomb : Component := {|
comp_UCC := {|
ucc_functor :=
paircomb_ucf_UnifiedCarrierFunctor
(comp_UCC C1)
(comp_UCC C2)
;
ucc_functor_monotone :=
paircomb_ucf_UnifiedCarrierFunctor_monotone
(comp_UCC C1)
(comp_UCC C2)
;
ucc_ctor_family :=
fun A nla ⇒
match nla with
| (0::ns, la) ⇒ @fmap option _ _ _ inl (@ucc_ctor_family (comp_UCC C1) A (ns,la))
| (1::ns, la) ⇒ @fmap option _ _ _ inr (@ucc_ctor_family (comp_UCC C2) A (ns,la))
| _ ⇒ None
end
;
|};
comp_invertor := fun A x ⇒
match x with
| inl y ⇒
let inv := (@comp_invertor Σ C1 A y) in
@fmap option _ _ _ (fun tmp ⇒ exist _ (0::((proj1_sig tmp).1), (proj1_sig tmp).2) _) inv
| inr y ⇒ @fmap option _ _ _ (fun tmp ⇒ exist _ (1::((proj1_sig tmp).1), (proj1_sig tmp).2) _) (@comp_invertor Σ C2 A y)
end
;
|}.
End paircomb.
Section combine.
Context
{Σ : OPMLSignature}
(l : list Component)
.
Definition combine : Component := foldr paircomb empty_component l.
End combine.
Section list_component.
Program Definition list_UCC : UnifiedCarrierComponent := {|
ucc_functor
:= fun A ⇒ list A ;
ucc_functor_monotone
:= fun A B f ⇒ @map A B f ;
ucc_ctor_family
:= fun (A : Type) nla ⇒
match nla with
| ([0], xs) ⇒ Some xs
| _ ⇒ None
end
;
|}.
Program Definition list_component {Σ : OPMLSignature} : Component := {|
comp_UCC := list_UCC ;
comp_invertor := fun A x ⇒
Some (exist _ ([0],(x):(list A)) erefl)
;
comp_invertor_complete := _ ;
|}.
End list_component.
Section with_signature.
Context
{Σ : OPMLSignature}
(UCI : UnifiedCarrierInfo)
(UCF : UnifiedCarrierFunctor)
(pos : is_monotone UCF)
.
Definition CarrierFunctor : Type :=
∀ (s : opml_sort),
propset UCI
.
(*
Context
(CF : CarrierFunctor)
(cfi : CarrierFunctorInvertor)
.
Definition lift_cf : propset (UnifiedCarrier UCF pos)
:= PropSet (fun (e : UnifiedCarrier UCF pos) =>
match e with
| c _ _ x =>
match (cfi x) with
| None => False
| Some ((A:Type),(y:A),pf) =>
(* Need to know that `x` came from UCF *)
True
end
end
).
*)
End with_signature.
(*
(*
Definition ModelInfo : Type :=
()*)
Record ModelInfo := {
}.
Definition ModelFunctor : Type -> Type :=
fun (CarrierBase : Type) =>
(Type*(ModelInfo))*)
From stdpp Require Import base list list_numbers propset.
(* This is unset by stdpp. We need to set it again.*)
Set Transparent Obligations.
From Equations Require Import Equations.
(* Set Equations Transparent. *)
*)
Require Import Coq.Program.Equality. (* Dependent destruction *)
Require Import Coq.Logic.Classical_Prop. (* Proof irrelevance *)
From MatchingLogic.OPML Require Export OpmlModel.
Definition UnifiedCarrierInfo := Type.
Definition UnifiedCarrierFunctor : Type
:= Type → UnifiedCarrierInfo
.
Definition UnifiedCarrierCtorFamily
(UCF : UnifiedCarrierFunctor) (A : Type)
: Type
:= ((list nat)*(list A))%type → (* Choose a particuar constructor from the family, and arguments of the constructor from the underlying type *)
option (UCF A) (* maybe return something, and maybe not *)
.
Definition is_monotone (F : UnifiedCarrierFunctor)
: Type
:= ∀ x y, (x → y) → (F x → F y)
.
Record UnifiedCarrierComponent := {
ucc_functor : UnifiedCarrierFunctor ;
ucc_functor_monotone : is_monotone ucc_functor ;
ucc_ctor_family : ∀ A, UnifiedCarrierCtorFamily ucc_functor A ;
ucc_ctor_family_inj : ∀ A args1 args2 ret,
(ucc_ctor_family A args1 = Some ret) →
(ucc_ctor_family A args2 = Some ret) →
args1 = args2 ;
}.
(* We can bypass the check because of the `is_monotone` requirement. *)
#[bypass_check(positivity=yes)]
Inductive UnifiedCarrier
(F: UnifiedCarrierFunctor)
(pos : is_monotone F)
: Type :=
| c (st : F (UnifiedCarrier F pos))
.
Definition CompInvertorT
(UCC : UnifiedCarrierComponent)
: Type
:= ∀ (A : Type) (x : ucc_functor UCC A),
option ({ nla : ((list nat)*(list A))%type | ucc_ctor_family UCC A nla = Some x })
.
Definition CompSortedCarrierT
{Σ : OPMLSignature}
(s : opml_sort)
(UCC : UnifiedCarrierComponent)
(invertor : CompInvertorT UCC)
:=
∀ (A : Type) (x : ucc_functor UCC A), Prop
.
Record Component {Σ : OPMLSignature} := {
comp_UCC
: UnifiedCarrierComponent ;
comp_invertor
: CompInvertorT comp_UCC ;
comp_invertor_complete
: ∀
(A : Type)
(nla : ((list nat)*(list A))%type)
(x : ucc_functor comp_UCC A),
ucc_ctor_family comp_UCC A nla = Some x →
∃ pf,
comp_invertor A x = Some (exist _ nla pf)
;
(*
comp_sorted_carrier
: forall s, CompSortedCarrierT s comp_UCC comp_invertor
; *)
}.
Section constant.
Context
(UCI : UnifiedCarrierInfo)
.
Definition constant_UnifiedCarrierFunctor : UnifiedCarrierFunctor
:= fun _ ⇒ UCI
.
Lemma constant_UnifiedCarrierFunctor_monotone : is_monotone constant_UnifiedCarrierFunctor.
(* TODO *)
Definition constant_inversion
{A : Type}
(x : constant_UnifiedCarrierFunctor A)
:= 0.
End constant.
Program Definition bool_UCC : UnifiedCarrierComponent := {|
ucc_functor
:= constant_UnifiedCarrierFunctor bool ;
ucc_functor_monotone
:= constant_UnifiedCarrierFunctor_monotone bool ;
ucc_ctor_family
:= fun A nla ⇒
match nla with
| ([0], []) ⇒ Some true
| ([1], []) ⇒ Some false
| _ ⇒ None
end
;
|}.
Program Definition bool_component {Σ : OPMLSignature} : Component := {|
comp_UCC := bool_UCC ;
comp_invertor := fun A x ⇒
match x return option ({ nla : ((list nat)*(list A))%type | ucc_ctor_family bool_UCC A nla = Some x }) with
| true ⇒ Some (exist (fun y ⇒ ucc_ctor_family bool_UCC A y = Some true) ([0],([]):(list A)) erefl)
| false ⇒ Some (exist _ ([1],([]):(list A)) erefl)
end
;
comp_invertor_complete := _ ;
(*
comp_sorted_carrier := fun s A x => True
(* TODO we need to query the sort, whether it belongs to the Bool subsignature *)
; *)
|}.
Program Definition empty_component {Σ : OPMLSignature} : Component := {|
comp_UCC := {|
ucc_functor
:= constant_UnifiedCarrierFunctor Empty_set ;
ucc_functor_monotone
:= constant_UnifiedCarrierFunctor_monotone Empty_set ;
ucc_ctor_family
:= fun A nla ⇒ None ;
|};
comp_invertor :=
fun A x ⇒ match x with end
;
comp_invertor_complete
:= _;
|}.
Section paircomb_ucf.
Context
(F1 F2 : UnifiedCarrierComponent)
.
Definition paircomb_ucf_UnifiedCarrierFunctor : UnifiedCarrierFunctor
:=
fun A ⇒ ((ucc_functor F1 A)+(ucc_functor F2 A))%type
.
Lemma paircomb_ucf_UnifiedCarrierFunctor_monotone : is_monotone paircomb_ucf_UnifiedCarrierFunctor.
End paircomb_ucf.
Section paircomb.
Context
{Σ : OPMLSignature}
(C1 C2 : Component)
.
Program Definition paircomb : Component := {|
comp_UCC := {|
ucc_functor :=
paircomb_ucf_UnifiedCarrierFunctor
(comp_UCC C1)
(comp_UCC C2)
;
ucc_functor_monotone :=
paircomb_ucf_UnifiedCarrierFunctor_monotone
(comp_UCC C1)
(comp_UCC C2)
;
ucc_ctor_family :=
fun A nla ⇒
match nla with
| (0::ns, la) ⇒ @fmap option _ _ _ inl (@ucc_ctor_family (comp_UCC C1) A (ns,la))
| (1::ns, la) ⇒ @fmap option _ _ _ inr (@ucc_ctor_family (comp_UCC C2) A (ns,la))
| _ ⇒ None
end
;
|};
comp_invertor := fun A x ⇒
match x with
| inl y ⇒
let inv := (@comp_invertor Σ C1 A y) in
@fmap option _ _ _ (fun tmp ⇒ exist _ (0::((proj1_sig tmp).1), (proj1_sig tmp).2) _) inv
| inr y ⇒ @fmap option _ _ _ (fun tmp ⇒ exist _ (1::((proj1_sig tmp).1), (proj1_sig tmp).2) _) (@comp_invertor Σ C2 A y)
end
;
|}.
End paircomb.
Section combine.
Context
{Σ : OPMLSignature}
(l : list Component)
.
Definition combine : Component := foldr paircomb empty_component l.
End combine.
Section list_component.
Program Definition list_UCC : UnifiedCarrierComponent := {|
ucc_functor
:= fun A ⇒ list A ;
ucc_functor_monotone
:= fun A B f ⇒ @map A B f ;
ucc_ctor_family
:= fun (A : Type) nla ⇒
match nla with
| ([0], xs) ⇒ Some xs
| _ ⇒ None
end
;
|}.
Program Definition list_component {Σ : OPMLSignature} : Component := {|
comp_UCC := list_UCC ;
comp_invertor := fun A x ⇒
Some (exist _ ([0],(x):(list A)) erefl)
;
comp_invertor_complete := _ ;
|}.
End list_component.
Section with_signature.
Context
{Σ : OPMLSignature}
(UCI : UnifiedCarrierInfo)
(UCF : UnifiedCarrierFunctor)
(pos : is_monotone UCF)
.
Definition CarrierFunctor : Type :=
∀ (s : opml_sort),
propset UCI
.
(*
Context
(CF : CarrierFunctor)
(cfi : CarrierFunctorInvertor)
.
Definition lift_cf : propset (UnifiedCarrier UCF pos)
:= PropSet (fun (e : UnifiedCarrier UCF pos) =>
match e with
| c _ _ x =>
match (cfi x) with
| None => False
| Some ((A:Type),(y:A),pf) =>
(* Need to know that `x` came from UCF *)
True
end
end
).
*)
End with_signature.
(*
(*
Definition ModelInfo : Type :=
()*)
Record ModelInfo := {
}.
Definition ModelFunctor : Type -> Type :=
fun (CarrierBase : Type) =>
(Type*(ModelInfo))*)
This page has been generated by coqdoc