File DefaultModels
From MatchingLogic.Theories Require Export Bool_Semantics
Nat_Syntax
.
Import Definedness_Syntax.Notations.
Import Logic.Notations.
(*
Subtasks:
- eval/app_ext automatic simplification
*)
Section Definedness.
Context {Σ : Signature} {M : Model}
{string_vars : variables = StringMLVariables}.
(*
Option 2: use only a single-symbol signature for definedness, which will be
glued to other theories/specs
*)
Instance definedness_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols (@symbols (@ml_symbols Σ) + Definedness_Syntax.Symbols) _ _;
}.
Instance definedness_syntax : Definedness_Syntax.Syntax := {
sym_inj := inr;
}.
Definition definedness_carrier : Type := Domain M + unit.
Definition definedness_sym_interp (m : @symbols (@ml_symbols Σ) + Definedness_Syntax.Symbols)
: propset definedness_carrier :=
match m with
| inl x ⇒ inl <$> (sym_interp M x)
| inr x ⇒ {[ inr () ]}
end.
Definition definedness_app_interp (m1 m2 : definedness_carrier)
: propset definedness_carrier :=
match m1 with
| inr () ⇒ ⊤
| inl x1 ⇒
match m2 with
| inl x2 ⇒ inl <$> app_interp M x1 x2
| inr () ⇒ ∅
end
end.
Definition DefinednessModel : Model := {|
Domain := definedness_carrier;
app_interp := definedness_app_interp;
sym_interp := definedness_sym_interp;
|}.
Theorem DefinednessModel_satisfies_theory :
DefinednessModel ⊨ᵀ Definedness_Syntax.theory.
End Definedness.
(* This is independent of ModelExtension.v, but it is very similar to it *)
Section Sorts.
Context {Σ : Signature} {M : Model}
{string_vars : variables = StringMLVariables}
{sort_interp : Domain M → propset M}.
Instance sorts_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols (@symbols (@ml_symbols (definedness_Σ)) + Sorts_Syntax.Symbols) _ _;
}.
Instance sorts_syntax : @Sorts_Syntax.Syntax sorts_Σ := {
sym_inj := inr;
imported_definedness := {|
Definedness_Syntax.sym_inj :=
λ x : Definedness_Syntax.Symbols,
match x with
| definedness ⇒ inl (inr definedness)
end
|};
}.
Definition sorts_carrier : Type := Domain (@DefinednessModel Σ M) + unit.
Definition sorts_sym_interp (m : @symbols (@ml_symbols (@definedness_Σ Σ)) + Sorts_Syntax.Symbols)
: propset sorts_carrier :=
match m with
| inl x ⇒ inl <$> (sym_interp (@DefinednessModel Σ M) x)
| inr x ⇒ {[ inr () ]}
end.
Definition sorts_app_interp (m1 m2 : sorts_carrier)
: propset sorts_carrier :=
match m1, m2 with
| inr (), inr () ⇒ ∅ (* inh ⋅ inh *)
| inr (), inl (inr ()) ⇒ ∅ (* inh ⋅ def *)
| inr (), inl (inl x) ⇒ (* inh ⋅ x *)
(inl ∘ inl) <$> (sort_interp x)
| inl (inr _), inr _ ⇒ ⊤ (* ⌈ ⌉ ⋅ inh <- Notion of definedness has to be extended *)
| inl (inr _), inl _ ⇒ ⊤ (* ⌈ ⌉ ⋅ x <- Notion of definedness has to be extended *)
| inl (inl _), inr _ ⇒ ∅ (* x ⋅ inh *)
| inl x1, inl x2 ⇒ (* x ⋅ y*)
inl <$> app_interp DefinednessModel x1 x2
end.
Definition SortsModel : Model := {|
Domain := sorts_carrier;
app_interp := sorts_app_interp;
sym_interp := sorts_sym_interp;
|}.
Theorem SortsModel_satisfies_theory :
SortsModel ⊨ᵀ Definedness_Syntax.theory.
End Sorts.
Ltac eval_simpl :=
try simp eval;
try rewrite eval_not_simpl;
try rewrite eval_and_simpl;
try rewrite eval_or_simpl;
try rewrite eval_top_simpl;
try rewrite eval_iff_simpl;
try rewrite eval_all_simpl;
(* TODO: try rewrite eval_nu_simpl; *)
try unshelve (erewrite eval_forall_of_sort);
try unshelve (erewrite eval_exists_of_sort);
try apply propset_fa_union_full.
Ltac eval_simpl_in H :=
try simp eval in H;
try rewrite eval_not_simpl in H;
try rewrite eval_and_simpl in H;
try rewrite eval_or_simpl in H;
try rewrite eval_top_simpl in H;
try rewrite eval_iff_simpl in H;
try rewrite eval_all_simpl in H;
(* TODO: try rewrite eval_nu_simpl; *)
try unshelve (erewrite eval_forall_of_sort in H);
try unshelve (erewrite eval_exists_of_sort in H);
try apply propset_fa_union_full in H.
Section Bool.
(* NOTE - INVESTIGATE:
When we automatically generate carriers, should the partial
operations use Coq standard types, or use the generated core
symbols?
*)
Inductive bool_carrier :=
| coreBoolSym (s : Bool_Syntax.Symbols)
(* TODO: the next two should not be part of the signature/symbols but they are
elements of the model's carrier *)
| partialAnd (b : bool)
| partialAndThen (b : option bool)
(**)
| defBool
| inhBool
| SortsBool
.
#[global]
Instance bool_carrier_EqDec : EqDecision bool_carrier.
#[global]
Program Instance bool_carrier_finite : finite.Finite bool_carrier.
Global Instance bool_carrier_countable : countable.Countable bool_carrier.
(* TODO: if partial ops are removed from the symbols, this has to be
adjusted *)
Instance bools_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols bool_carrier _ _;
}.
Program Instance bool_syntax : @Bool_Syntax.Syntax bools_Σ := {
sym_inj := coreBoolSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ match x with
| sym_inh ⇒ inhBool
| sym_sorts ⇒ SortsBool
end;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ defBool;
|};
|};
}.
Definition bool_sym_interp (m : @symbols (@ml_symbols bools_Σ))
: propset bool_carrier := {[ m ]}.
Definition bool_app_interp (m1 m2 : bool_carrier)
: propset bool_carrier :=
match m1 with
| coreBoolSym sAnd ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ partialAnd true ]}
| coreBoolSym sFalse ⇒ {[ partialAnd false ]}
| _ ⇒ ∅
end
| coreBoolSym sAndThen ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ partialAndThen (Some true) ]}
| coreBoolSym sFalse ⇒ {[ partialAndThen (Some false) ]}
| _ ⇒ {[ partialAndThen None ]}
end
| coreBoolSym sNeg ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sFalse ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sTrue ]}
| _ ⇒ ∅
end
| coreBoolSym _ ⇒ ∅
| partialAnd false ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sFalse ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAnd true ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sTrue ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAndThen (Some false) ⇒ {[ coreBoolSym sFalse ]}
| partialAndThen (Some true) ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sTrue ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAndThen None ⇒
match m2 with
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
(**)
| defBool ⇒ ⊤
| inhBool ⇒
match m2 with
| coreBoolSym sBool ⇒ {[ coreBoolSym sFalse; coreBoolSym sTrue ]}
(* type value set *)
| SortsBool ⇒ {[coreBoolSym sBool]}
| _ ⇒ ∅
end
| SortsBool ⇒ ∅
end.
Global Instance bool_carrier_inhabited : Inhabited bool_carrier.
Program Definition BoolModel : Model := {|
Domain := bool_carrier;
app_interp := bool_app_interp;
sym_interp := bool_sym_interp;
|}.
Theorem indec_bool :
∀ ρ s (m : BoolModel),
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ).
Hint Resolve propset_leibniz_equiv : core.
Theorem BoolModel_satisfies_theory :
BoolModel ⊨ᵀ Bool_Syntax.theory.
End Bool.
Section Nat.
Inductive nat_carrier :=
| coreNatSym (s : Nat_Syntax.Symbols)
(* TODO: these two should not be in the signature, only in the carrier *)
| partialAdd (s : nat)
| natVal (n : nat)
(**)
| defNat
| inhNat
| SortsNat
.
#[global]
Instance nat_carrier_EqDec : EqDecision nat_carrier.
Global Instance nat_carrier_countable : countable.Countable nat_carrier.
Instance nat_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols nat_carrier _ _;
}.
Program Instance nat_syntax : @Nat_Syntax.Syntax nat_Σ := {
sym_inj := coreNatSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ match x with
| sym_inh ⇒ inhNat
| sym_sorts ⇒ SortsNat
end;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ defNat;
|};
|};
}.
Definition nat_sym_interp (m : symbols)
: propset nat_carrier :=
match m with
| coreNatSym sZero ⇒ {[ natVal 0 ]}
| x ⇒ {[ x ]}
end.
Definition nat_app_interp (m1 m2 : nat_carrier)
: propset nat_carrier :=
match m1 with
| coreNatSym sSucc ⇒
match m2 with
| natVal n ⇒ {[ natVal (S n) ]}
| _ ⇒ ∅
end
| coreNatSym sAddNat ⇒
match m2 with
| natVal n ⇒ {[ partialAdd n ]}
| _ ⇒ ∅
end
| coreNatSym _ ⇒ ∅
| partialAdd n ⇒
match m2 with
| natVal m ⇒ {[ natVal (n + m) ]}
| _ ⇒ ∅
end
(**)
| natVal _ ⇒ ∅
| defNat ⇒ ⊤
| inhNat ⇒
match m2 with
| coreNatSym sNat ⇒ {[ m | ∃ n, m = natVal n ]}
| SortsNat ⇒ {[coreNatSym sNat]}
| _ ⇒ ∅
end
| SortsNat ⇒ ∅
end.
Global Instance nat_carrier_inhabited : Inhabited nat_carrier.
Program Definition NatModel : Model := {|
Domain := nat_carrier;
app_interp := nat_app_interp;
sym_interp := nat_sym_interp;
|}.
Theorem indec_nat :
∀ ρ s (m : NatModel),
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ).
Hint Resolve propset_leibniz_equiv : core.
Theorem NatModel_satisfies_theory :
NatModel ⊨ᵀ Nat_Syntax.theory.
End Nat.
(*
Q: What happens to the signatures when importing a theory into another?
How to handle diamond dependencies in the syntax? For example
definedness is in Nat and Bool signatures too, how should we handle it
in the glued signature?
1. Do nothing, just use union, and add theory-level axioms saying that the
different definedness symbols are equal/interchangable.
2. Only define signature specific symbols (e.g., 0, succ, +), and inject
definedness and others.
3. Use a binary relation which expresses which symbols are repeated. Then use
union to express the signature, but tag each symbol (of one of the signatures)
with a proof based on this relation that it is unique.
*)
Require Import ModelExtension.
Inductive extend_def_inh {A B : Set} : Set :=
| inj_def
| inj_inh
| fromA (a : A)
| fromB (b : B).
Program Definition signature_fusion
(Σ1 Σ2 : Signature)
(* (def1 inh1 : @symbols (@ml_symbols Σ1))
(def2 inh2 : @symbols (@ml_symbols Σ2)) *)
(* (R : @symbols (@ml_symbols Σ1) -> @symbols (@ml_symbols Σ2) -> bool) *)
: Signature :=
{|
variables := StringMLVariables;
ml_symbols := {|
symbols := @extend_def_inh (@symbols (@ml_symbols Σ1)) (@symbols (@ml_symbols Σ2))
|};
|}
.
(* technical *)
Section BoolNat.
(* common carrier *)
(* Definition bool_nat_carrier : Set := bool_carrier + nat_carrier.
[global] Instance bool_nat_carrier_EqDec : EqDecision bool_nat_carrier. Proof. solve_decision. Defined. Global Instance bool_nat_carrier_countable : countable.Countable bool_nat_carrier. Proof. by apply sum_countable. Defined. Global Instance bool_nat_carrier_inhabited : Inhabited bool_nat_carrier. Proof. constructor. constructor. constructor. constructor. Defined. *)
(* common signature *)
Instance nat_bool_Σ : Signature := signature_fusion nat_Σ bools_Σ.
(*
Here, we say that we use the new definedness
*)
Program Instance nat_bool_syntax_bool_part : @Bool_Syntax.Syntax nat_bool_Σ := {
sym_inj := fromB ∘ coreBoolSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ inj_inh;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ inj_def;
|};
|};
}.
Program Instance nat_bool_syntax_nat_part : @Nat_Syntax.Syntax nat_bool_Σ := {
sym_inj := fromA ∘ coreNatSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ inj_inh;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ inj_def;
|};
|};
}.
Check @patt_defined nat_bool_Σ _ patt_bott.
(* Check @patt_defined bools_Σ (@imported_definedness bools_Σ
(@imported_sorts bools_Σ (@bool_syntax) )) patt_bott. *)
Check @patt_defined nat_Σ _ patt_bott.
(* Model extension's new_sym_interp does not define meaning to new symbols! *)
Definition nat_bool_app_interp := new_app_interp.
End BoolNat.
Nat_Syntax
.
Import Definedness_Syntax.Notations.
Import Logic.Notations.
(*
Subtasks:
- eval/app_ext automatic simplification
*)
Section Definedness.
Context {Σ : Signature} {M : Model}
{string_vars : variables = StringMLVariables}.
(*
Option 2: use only a single-symbol signature for definedness, which will be
glued to other theories/specs
*)
Instance definedness_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols (@symbols (@ml_symbols Σ) + Definedness_Syntax.Symbols) _ _;
}.
Instance definedness_syntax : Definedness_Syntax.Syntax := {
sym_inj := inr;
}.
Definition definedness_carrier : Type := Domain M + unit.
Definition definedness_sym_interp (m : @symbols (@ml_symbols Σ) + Definedness_Syntax.Symbols)
: propset definedness_carrier :=
match m with
| inl x ⇒ inl <$> (sym_interp M x)
| inr x ⇒ {[ inr () ]}
end.
Definition definedness_app_interp (m1 m2 : definedness_carrier)
: propset definedness_carrier :=
match m1 with
| inr () ⇒ ⊤
| inl x1 ⇒
match m2 with
| inl x2 ⇒ inl <$> app_interp M x1 x2
| inr () ⇒ ∅
end
end.
Definition DefinednessModel : Model := {|
Domain := definedness_carrier;
app_interp := definedness_app_interp;
sym_interp := definedness_sym_interp;
|}.
Theorem DefinednessModel_satisfies_theory :
DefinednessModel ⊨ᵀ Definedness_Syntax.theory.
End Definedness.
(* This is independent of ModelExtension.v, but it is very similar to it *)
Section Sorts.
Context {Σ : Signature} {M : Model}
{string_vars : variables = StringMLVariables}
{sort_interp : Domain M → propset M}.
Instance sorts_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols (@symbols (@ml_symbols (definedness_Σ)) + Sorts_Syntax.Symbols) _ _;
}.
Instance sorts_syntax : @Sorts_Syntax.Syntax sorts_Σ := {
sym_inj := inr;
imported_definedness := {|
Definedness_Syntax.sym_inj :=
λ x : Definedness_Syntax.Symbols,
match x with
| definedness ⇒ inl (inr definedness)
end
|};
}.
Definition sorts_carrier : Type := Domain (@DefinednessModel Σ M) + unit.
Definition sorts_sym_interp (m : @symbols (@ml_symbols (@definedness_Σ Σ)) + Sorts_Syntax.Symbols)
: propset sorts_carrier :=
match m with
| inl x ⇒ inl <$> (sym_interp (@DefinednessModel Σ M) x)
| inr x ⇒ {[ inr () ]}
end.
Definition sorts_app_interp (m1 m2 : sorts_carrier)
: propset sorts_carrier :=
match m1, m2 with
| inr (), inr () ⇒ ∅ (* inh ⋅ inh *)
| inr (), inl (inr ()) ⇒ ∅ (* inh ⋅ def *)
| inr (), inl (inl x) ⇒ (* inh ⋅ x *)
(inl ∘ inl) <$> (sort_interp x)
| inl (inr _), inr _ ⇒ ⊤ (* ⌈ ⌉ ⋅ inh <- Notion of definedness has to be extended *)
| inl (inr _), inl _ ⇒ ⊤ (* ⌈ ⌉ ⋅ x <- Notion of definedness has to be extended *)
| inl (inl _), inr _ ⇒ ∅ (* x ⋅ inh *)
| inl x1, inl x2 ⇒ (* x ⋅ y*)
inl <$> app_interp DefinednessModel x1 x2
end.
Definition SortsModel : Model := {|
Domain := sorts_carrier;
app_interp := sorts_app_interp;
sym_interp := sorts_sym_interp;
|}.
Theorem SortsModel_satisfies_theory :
SortsModel ⊨ᵀ Definedness_Syntax.theory.
End Sorts.
Ltac eval_simpl :=
try simp eval;
try rewrite eval_not_simpl;
try rewrite eval_and_simpl;
try rewrite eval_or_simpl;
try rewrite eval_top_simpl;
try rewrite eval_iff_simpl;
try rewrite eval_all_simpl;
(* TODO: try rewrite eval_nu_simpl; *)
try unshelve (erewrite eval_forall_of_sort);
try unshelve (erewrite eval_exists_of_sort);
try apply propset_fa_union_full.
Ltac eval_simpl_in H :=
try simp eval in H;
try rewrite eval_not_simpl in H;
try rewrite eval_and_simpl in H;
try rewrite eval_or_simpl in H;
try rewrite eval_top_simpl in H;
try rewrite eval_iff_simpl in H;
try rewrite eval_all_simpl in H;
(* TODO: try rewrite eval_nu_simpl; *)
try unshelve (erewrite eval_forall_of_sort in H);
try unshelve (erewrite eval_exists_of_sort in H);
try apply propset_fa_union_full in H.
Section Bool.
(* NOTE - INVESTIGATE:
When we automatically generate carriers, should the partial
operations use Coq standard types, or use the generated core
symbols?
*)
Inductive bool_carrier :=
| coreBoolSym (s : Bool_Syntax.Symbols)
(* TODO: the next two should not be part of the signature/symbols but they are
elements of the model's carrier *)
| partialAnd (b : bool)
| partialAndThen (b : option bool)
(**)
| defBool
| inhBool
| SortsBool
.
#[global]
Instance bool_carrier_EqDec : EqDecision bool_carrier.
#[global]
Program Instance bool_carrier_finite : finite.Finite bool_carrier.
Global Instance bool_carrier_countable : countable.Countable bool_carrier.
(* TODO: if partial ops are removed from the symbols, this has to be
adjusted *)
Instance bools_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols bool_carrier _ _;
}.
Program Instance bool_syntax : @Bool_Syntax.Syntax bools_Σ := {
sym_inj := coreBoolSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ match x with
| sym_inh ⇒ inhBool
| sym_sorts ⇒ SortsBool
end;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ defBool;
|};
|};
}.
Definition bool_sym_interp (m : @symbols (@ml_symbols bools_Σ))
: propset bool_carrier := {[ m ]}.
Definition bool_app_interp (m1 m2 : bool_carrier)
: propset bool_carrier :=
match m1 with
| coreBoolSym sAnd ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ partialAnd true ]}
| coreBoolSym sFalse ⇒ {[ partialAnd false ]}
| _ ⇒ ∅
end
| coreBoolSym sAndThen ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ partialAndThen (Some true) ]}
| coreBoolSym sFalse ⇒ {[ partialAndThen (Some false) ]}
| _ ⇒ {[ partialAndThen None ]}
end
| coreBoolSym sNeg ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sFalse ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sTrue ]}
| _ ⇒ ∅
end
| coreBoolSym _ ⇒ ∅
| partialAnd false ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sFalse ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAnd true ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sTrue ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAndThen (Some false) ⇒ {[ coreBoolSym sFalse ]}
| partialAndThen (Some true) ⇒
match m2 with
| coreBoolSym sTrue ⇒ {[ coreBoolSym sTrue ]}
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
| partialAndThen None ⇒
match m2 with
| coreBoolSym sFalse ⇒ {[ coreBoolSym sFalse ]}
| _ ⇒ ∅
end
(**)
| defBool ⇒ ⊤
| inhBool ⇒
match m2 with
| coreBoolSym sBool ⇒ {[ coreBoolSym sFalse; coreBoolSym sTrue ]}
(* type value set *)
| SortsBool ⇒ {[coreBoolSym sBool]}
| _ ⇒ ∅
end
| SortsBool ⇒ ∅
end.
Global Instance bool_carrier_inhabited : Inhabited bool_carrier.
Program Definition BoolModel : Model := {|
Domain := bool_carrier;
app_interp := bool_app_interp;
sym_interp := bool_sym_interp;
|}.
Theorem indec_bool :
∀ ρ s (m : BoolModel),
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ).
Hint Resolve propset_leibniz_equiv : core.
Theorem BoolModel_satisfies_theory :
BoolModel ⊨ᵀ Bool_Syntax.theory.
End Bool.
Section Nat.
Inductive nat_carrier :=
| coreNatSym (s : Nat_Syntax.Symbols)
(* TODO: these two should not be in the signature, only in the carrier *)
| partialAdd (s : nat)
| natVal (n : nat)
(**)
| defNat
| inhNat
| SortsNat
.
#[global]
Instance nat_carrier_EqDec : EqDecision nat_carrier.
Global Instance nat_carrier_countable : countable.Countable nat_carrier.
Instance nat_Σ : Signature := {
variables := StringMLVariables;
ml_symbols := Build_MLSymbols nat_carrier _ _;
}.
Program Instance nat_syntax : @Nat_Syntax.Syntax nat_Σ := {
sym_inj := coreNatSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ match x with
| sym_inh ⇒ inhNat
| sym_sorts ⇒ SortsNat
end;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ defNat;
|};
|};
}.
Definition nat_sym_interp (m : symbols)
: propset nat_carrier :=
match m with
| coreNatSym sZero ⇒ {[ natVal 0 ]}
| x ⇒ {[ x ]}
end.
Definition nat_app_interp (m1 m2 : nat_carrier)
: propset nat_carrier :=
match m1 with
| coreNatSym sSucc ⇒
match m2 with
| natVal n ⇒ {[ natVal (S n) ]}
| _ ⇒ ∅
end
| coreNatSym sAddNat ⇒
match m2 with
| natVal n ⇒ {[ partialAdd n ]}
| _ ⇒ ∅
end
| coreNatSym _ ⇒ ∅
| partialAdd n ⇒
match m2 with
| natVal m ⇒ {[ natVal (n + m) ]}
| _ ⇒ ∅
end
(**)
| natVal _ ⇒ ∅
| defNat ⇒ ⊤
| inhNat ⇒
match m2 with
| coreNatSym sNat ⇒ {[ m | ∃ n, m = natVal n ]}
| SortsNat ⇒ {[coreNatSym sNat]}
| _ ⇒ ∅
end
| SortsNat ⇒ ∅
end.
Global Instance nat_carrier_inhabited : Inhabited nat_carrier.
Program Definition NatModel : Model := {|
Domain := nat_carrier;
app_interp := nat_app_interp;
sym_interp := nat_sym_interp;
|}.
Theorem indec_nat :
∀ ρ s (m : NatModel),
Decision (m ∈ Minterp_inhabitant (patt_sym s) ρ).
Hint Resolve propset_leibniz_equiv : core.
Theorem NatModel_satisfies_theory :
NatModel ⊨ᵀ Nat_Syntax.theory.
End Nat.
(*
Q: What happens to the signatures when importing a theory into another?
How to handle diamond dependencies in the syntax? For example
definedness is in Nat and Bool signatures too, how should we handle it
in the glued signature?
1. Do nothing, just use union, and add theory-level axioms saying that the
different definedness symbols are equal/interchangable.
2. Only define signature specific symbols (e.g., 0, succ, +), and inject
definedness and others.
3. Use a binary relation which expresses which symbols are repeated. Then use
union to express the signature, but tag each symbol (of one of the signatures)
with a proof based on this relation that it is unique.
*)
Require Import ModelExtension.
Inductive extend_def_inh {A B : Set} : Set :=
| inj_def
| inj_inh
| fromA (a : A)
| fromB (b : B).
Program Definition signature_fusion
(Σ1 Σ2 : Signature)
(* (def1 inh1 : @symbols (@ml_symbols Σ1))
(def2 inh2 : @symbols (@ml_symbols Σ2)) *)
(* (R : @symbols (@ml_symbols Σ1) -> @symbols (@ml_symbols Σ2) -> bool) *)
: Signature :=
{|
variables := StringMLVariables;
ml_symbols := {|
symbols := @extend_def_inh (@symbols (@ml_symbols Σ1)) (@symbols (@ml_symbols Σ2))
|};
|}
.
(* technical *)
Section BoolNat.
(* common carrier *)
(* Definition bool_nat_carrier : Set := bool_carrier + nat_carrier.
[global] Instance bool_nat_carrier_EqDec : EqDecision bool_nat_carrier. Proof. solve_decision. Defined. Global Instance bool_nat_carrier_countable : countable.Countable bool_nat_carrier. Proof. by apply sum_countable. Defined. Global Instance bool_nat_carrier_inhabited : Inhabited bool_nat_carrier. Proof. constructor. constructor. constructor. constructor. Defined. *)
(* common signature *)
Instance nat_bool_Σ : Signature := signature_fusion nat_Σ bools_Σ.
(*
Here, we say that we use the new definedness
*)
Program Instance nat_bool_syntax_bool_part : @Bool_Syntax.Syntax nat_bool_Σ := {
sym_inj := fromB ∘ coreBoolSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ inj_inh;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ inj_def;
|};
|};
}.
Program Instance nat_bool_syntax_nat_part : @Nat_Syntax.Syntax nat_bool_Σ := {
sym_inj := fromA ∘ coreNatSym;
imported_sorts := {|
Sorts_Syntax.sym_inj := fun x ⇒ inj_inh;
imported_definedness := {|
Definedness_Syntax.sym_inj := fun x ⇒ inj_def;
|};
|};
}.
Check @patt_defined nat_bool_Σ _ patt_bott.
(* Check @patt_defined bools_Σ (@imported_definedness bools_Σ
(@imported_sorts bools_Σ (@bool_syntax) )) patt_bott. *)
Check @patt_defined nat_Σ _ patt_bott.
(* Model extension's new_sym_interp does not define meaning to new symbols! *)
Definition nat_bool_app_interp := new_app_interp.
End BoolNat.
This page has been generated by coqdoc