File Definedness_Semantics
From Coq Require Import Logic.Classical_Prop
Classes.Morphisms_Prop.
From MatchingLogic Require Export Logic
Definedness_Syntax.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Section definedness.
Context
{Σ : Signature}
{syntax : Syntax}
.
Open Scope ml_scope.
Let sym (s : Symbols) : Pattern :=
@patt_sym Σ (sym_inj s).
Lemma definedness_app_ext_not_empty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ S, S ≠ ∅ →
app_ext (sym_interp M (sym_inj def_sym)) S = ⊤.
Lemma definedness_not_empty_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
(eval ρ ϕ) ≠ ∅ →
(@eval Σ M ρ ⌈ ϕ ⌉ ) = ⊤.
Lemma definedness_empty_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ = ∅ →
@eval Σ M ρ ⌈ ϕ ⌉ = ∅.
Theorem modus_tollens: ∀ (P Q : Prop), (P → Q) → ¬Q → ¬P.
Lemma definedness_empty_2 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌈ ϕ ⌉ = ∅ →
@eval Σ M ρ ϕ = ∅.
Lemma definedness_not_empty_2 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌈ ϕ ⌉ = ⊤ →
@eval Σ M ρ ϕ ≠ ∅.
Lemma definedness_not_empty_iff : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
(eval ρ ϕ) ≠ ∅ ↔
(@eval Σ M ρ ⌈ ϕ ⌉ ) = ⊤.
Lemma totality_not_full : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ ≠ ⊤ →
@eval Σ M ρ ⌊ ϕ ⌋ = ∅.
Lemma totality_full : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ = ⊤ →
@eval Σ M ρ ⌊ ϕ ⌋ = ⊤.
Lemma totality_result_empty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌊ ϕ ⌋ = ∅ →
@eval Σ M ρ ϕ ≠ ⊤.
Lemma totality_not_full_iff : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ ≠ ⊤ ↔
@eval Σ M ρ ⌊ ϕ ⌋ = ∅.
Lemma totality_result_nonempty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌊ ϕ ⌋ ≠ ∅ →
@eval Σ M ρ ϕ = ⊤.
Lemma equal_iff_both_subseteq : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ ↔
(
eval ρ (ϕ1 ⊆ml ϕ2) = ⊤ ∧
@eval Σ M ρ (patt_subseteq ϕ2 ϕ1) = ⊤).
Lemma subseteq_iff_interpr_subseteq : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 ⊆ml ϕ2) = ⊤ ↔
(eval ρ ϕ1)
⊆ (@eval Σ M ρ ϕ2).
Lemma equal_iff_interpr_same : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ ↔
eval ρ ϕ1
= @eval Σ M ρ ϕ2.
Lemma equal_refl : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
@eval Σ M ρ (patt_equal ϕ ϕ) = ⊤.
Lemma equal_sym : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ →
@eval Σ M ρ (patt_equal ϕ2 ϕ1) = ⊤.
Lemma equal_trans : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 ϕ3 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ →
eval ρ (patt_equal ϕ2 ϕ3) = ⊤ →
@eval Σ M ρ (patt_equal ϕ1 ϕ3) = ⊤.
Lemma free_evar_in_patt : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (x : evar)(ϕ : Pattern) (ρ : Valuation),
(evar_valuation ρ x ∈ (eval ρ ϕ)) ↔
@eval Σ M ρ (patt_in (patt_free_evar x) ϕ) = ⊤.
Lemma T_predicate_defined : ∀ ϕ, T_predicate theory ⌈ ϕ ⌉.
Lemma T_pre_predicate_defined : ∀ ϕ, T_pre_predicate theory ⌈ ϕ ⌉.
Hint Resolve T_predicate_defined : core.
Lemma T_predicate_total : ∀ ϕ, T_predicate theory ⌊ ϕ ⌋.
Lemma T_pre_predicate_total : ∀ ϕ, T_pre_predicate theory ⌊ ϕ ⌋.
Hint Resolve T_predicate_total : core.
Lemma T_predicate_subseteq : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_subseteq ϕ₁ ϕ₂).
Lemma T_pre_predicate_subseteq : ∀ ϕ₁ ϕ₂, T_pre_predicate theory (patt_subseteq ϕ₁ ϕ₂).
Hint Resolve T_predicate_subseteq : core.
Lemma T_predicate_equals : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_equal ϕ₁ ϕ₂).
Lemma T_pre_predicate_equal : ∀ ϕ₁ ϕ₂, T_pre_predicate theory (patt_equal ϕ₁ ϕ₂).
Hint Resolve T_predicate_equals : core.
Lemma T_predicate_in : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_in ϕ₁ ϕ₂).
Hint Resolve T_predicate_in : core.
Lemma T_predicate_eq_inversion : ∀ ϕ₁ ϕ₂,
T_predicate theory (patt_eq_inversion_of ϕ₁ ϕ₂).
Lemma eval_eq_inversion_of ϕ₁ ϕ₂ M ρ :
M ⊨ᵀ theory →
@eval Σ M ρ (patt_eq_inversion_of ϕ₁ ϕ₂) = ⊤
↔ (∀ m₁ m₂,
m₂ ∈ rel_of ρ ϕ₁ m₁ ↔ m₁ ∈ rel_of ρ ϕ₂ m₂ (* TODO make rel_of take one more parameter. *)
).
Lemma single_element_definedness_impl_satisfies_definedness (M : Model) :
(∃ (hashdef : Domain M),
sym_interp M (sym_inj def_sym) = {[hashdef]}
∧ ∀ x, app_interp _ hashdef x = ⊤
) →
satisfies_model M (axiom AxDefinedness).
Lemma satisfies_definedness_implies_has_element_for_every_element
(M : Model):
M ⊨ᵀ theory →
∀ (x y : Domain M),
∃ (z : Domain M),
z ∈ sym_interp M (sym_inj def_sym)
∧ y ∈ app_interp _ z x.
Lemma not_equal_iff_not_interpr_same_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
@eval Σ M ρ (ϕ1 =ml ϕ2) = ∅ ↔
eval ρ ϕ1
≠ eval ρ ϕ2.
Lemma not_subseteq_iff_not_interpr_subseteq_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 ⊆ml ϕ2) = ∅ ↔
~(eval ρ ϕ1)
⊆ (@eval Σ M ρ ϕ2).
Lemma patt_defined_dec : ∀ (M : Model),
M ⊨ᵀ theory →
∀ φ ρ,
@eval _ M ρ ⌈φ⌉ = ⊤ ∨
@eval _ M ρ ⌈φ⌉ = ∅.
Lemma patt_total_dec : ∀ (M : Model),
M ⊨ᵀ theory →
∀ φ ρ,
@eval _ M ρ ⌊φ⌋ = ⊤ ∨
@eval _ M ρ ⌊φ⌋ = ∅.
Lemma eval_equal_emplace : ∀ (M : Model),
M ⊨ᵀ theory →
∀ C (φ1 φ2 : Pattern) (ρ : Valuation),
well_formed φ1 →
well_formed φ2 →
@eval _ M ρ φ1 = eval ρ φ2 →
eval ρ (emplace C φ1) = eval ρ (emplace C φ2).
Classes.Morphisms_Prop.
From MatchingLogic Require Export Logic
Definedness_Syntax.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Section definedness.
Context
{Σ : Signature}
{syntax : Syntax}
.
Open Scope ml_scope.
Let sym (s : Symbols) : Pattern :=
@patt_sym Σ (sym_inj s).
Lemma definedness_app_ext_not_empty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ S, S ≠ ∅ →
app_ext (sym_interp M (sym_inj def_sym)) S = ⊤.
Lemma definedness_not_empty_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
(eval ρ ϕ) ≠ ∅ →
(@eval Σ M ρ ⌈ ϕ ⌉ ) = ⊤.
Lemma definedness_empty_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ = ∅ →
@eval Σ M ρ ⌈ ϕ ⌉ = ∅.
Theorem modus_tollens: ∀ (P Q : Prop), (P → Q) → ¬Q → ¬P.
Lemma definedness_empty_2 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌈ ϕ ⌉ = ∅ →
@eval Σ M ρ ϕ = ∅.
Lemma definedness_not_empty_2 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌈ ϕ ⌉ = ⊤ →
@eval Σ M ρ ϕ ≠ ∅.
Lemma definedness_not_empty_iff : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
(eval ρ ϕ) ≠ ∅ ↔
(@eval Σ M ρ ⌈ ϕ ⌉ ) = ⊤.
Lemma totality_not_full : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ ≠ ⊤ →
@eval Σ M ρ ⌊ ϕ ⌋ = ∅.
Lemma totality_full : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ = ⊤ →
@eval Σ M ρ ⌊ ϕ ⌋ = ⊤.
Lemma totality_result_empty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌊ ϕ ⌋ = ∅ →
@eval Σ M ρ ϕ ≠ ⊤.
Lemma totality_not_full_iff : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ϕ ≠ ⊤ ↔
@eval Σ M ρ ⌊ ϕ ⌋ = ∅.
Lemma totality_result_nonempty : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
eval ρ ⌊ ϕ ⌋ ≠ ∅ →
@eval Σ M ρ ϕ = ⊤.
Lemma equal_iff_both_subseteq : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ ↔
(
eval ρ (ϕ1 ⊆ml ϕ2) = ⊤ ∧
@eval Σ M ρ (patt_subseteq ϕ2 ϕ1) = ⊤).
Lemma subseteq_iff_interpr_subseteq : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 ⊆ml ϕ2) = ⊤ ↔
(eval ρ ϕ1)
⊆ (@eval Σ M ρ ϕ2).
Lemma equal_iff_interpr_same : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ ↔
eval ρ ϕ1
= @eval Σ M ρ ϕ2.
Lemma equal_refl : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ : Pattern) (ρ : Valuation),
@eval Σ M ρ (patt_equal ϕ ϕ) = ⊤.
Lemma equal_sym : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ →
@eval Σ M ρ (patt_equal ϕ2 ϕ1) = ⊤.
Lemma equal_trans : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 ϕ3 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 =ml ϕ2) = ⊤ →
eval ρ (patt_equal ϕ2 ϕ3) = ⊤ →
@eval Σ M ρ (patt_equal ϕ1 ϕ3) = ⊤.
Lemma free_evar_in_patt : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (x : evar)(ϕ : Pattern) (ρ : Valuation),
(evar_valuation ρ x ∈ (eval ρ ϕ)) ↔
@eval Σ M ρ (patt_in (patt_free_evar x) ϕ) = ⊤.
Lemma T_predicate_defined : ∀ ϕ, T_predicate theory ⌈ ϕ ⌉.
Lemma T_pre_predicate_defined : ∀ ϕ, T_pre_predicate theory ⌈ ϕ ⌉.
Hint Resolve T_predicate_defined : core.
Lemma T_predicate_total : ∀ ϕ, T_predicate theory ⌊ ϕ ⌋.
Lemma T_pre_predicate_total : ∀ ϕ, T_pre_predicate theory ⌊ ϕ ⌋.
Hint Resolve T_predicate_total : core.
Lemma T_predicate_subseteq : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_subseteq ϕ₁ ϕ₂).
Lemma T_pre_predicate_subseteq : ∀ ϕ₁ ϕ₂, T_pre_predicate theory (patt_subseteq ϕ₁ ϕ₂).
Hint Resolve T_predicate_subseteq : core.
Lemma T_predicate_equals : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_equal ϕ₁ ϕ₂).
Lemma T_pre_predicate_equal : ∀ ϕ₁ ϕ₂, T_pre_predicate theory (patt_equal ϕ₁ ϕ₂).
Hint Resolve T_predicate_equals : core.
Lemma T_predicate_in : ∀ ϕ₁ ϕ₂, T_predicate theory (patt_in ϕ₁ ϕ₂).
Hint Resolve T_predicate_in : core.
Lemma T_predicate_eq_inversion : ∀ ϕ₁ ϕ₂,
T_predicate theory (patt_eq_inversion_of ϕ₁ ϕ₂).
Lemma eval_eq_inversion_of ϕ₁ ϕ₂ M ρ :
M ⊨ᵀ theory →
@eval Σ M ρ (patt_eq_inversion_of ϕ₁ ϕ₂) = ⊤
↔ (∀ m₁ m₂,
m₂ ∈ rel_of ρ ϕ₁ m₁ ↔ m₁ ∈ rel_of ρ ϕ₂ m₂ (* TODO make rel_of take one more parameter. *)
).
Lemma single_element_definedness_impl_satisfies_definedness (M : Model) :
(∃ (hashdef : Domain M),
sym_interp M (sym_inj def_sym) = {[hashdef]}
∧ ∀ x, app_interp _ hashdef x = ⊤
) →
satisfies_model M (axiom AxDefinedness).
Lemma satisfies_definedness_implies_has_element_for_every_element
(M : Model):
M ⊨ᵀ theory →
∀ (x y : Domain M),
∃ (z : Domain M),
z ∈ sym_interp M (sym_inj def_sym)
∧ y ∈ app_interp _ z x.
Lemma not_equal_iff_not_interpr_same_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
@eval Σ M ρ (ϕ1 =ml ϕ2) = ∅ ↔
eval ρ ϕ1
≠ eval ρ ϕ2.
Lemma not_subseteq_iff_not_interpr_subseteq_1 : ∀ (M : Model),
M ⊨ᵀ theory →
∀ (ϕ1 ϕ2 : Pattern) (ρ : Valuation),
eval ρ (ϕ1 ⊆ml ϕ2) = ∅ ↔
~(eval ρ ϕ1)
⊆ (@eval Σ M ρ ϕ2).
Lemma patt_defined_dec : ∀ (M : Model),
M ⊨ᵀ theory →
∀ φ ρ,
@eval _ M ρ ⌈φ⌉ = ⊤ ∨
@eval _ M ρ ⌈φ⌉ = ∅.
Lemma patt_total_dec : ∀ (M : Model),
M ⊨ᵀ theory →
∀ φ ρ,
@eval _ M ρ ⌊φ⌋ = ⊤ ∨
@eval _ M ρ ⌊φ⌋ = ∅.
Lemma eval_equal_emplace : ∀ (M : Model),
M ⊨ᵀ theory →
∀ C (φ1 φ2 : Pattern) (ρ : Valuation),
well_formed φ1 →
well_formed φ2 →
@eval _ M ρ φ1 = eval ρ φ2 →
eval ρ (emplace C φ1) = eval ρ (emplace C φ2).
FUN_EXT axiom
Lemma eq_elim_is_top : ∀ (M : Model),
M ⊨ᵀ theory →
∀ C (φ1 φ2 : Pattern) (ρ : Valuation),
well_formed φ1 →
well_formed φ2 →
@eval _ M ρ (φ1 =ml φ2 ---> emplace C φ1 ---> emplace C φ2) = ⊤.
classic axiom:
End definedness.
From MatchingLogic Require Import StringSignature.
Module equivalence_insufficient.
Open Scope ml_scope.
Inductive exampleSymbols : Set :=
| sym_f.
#[local]
Instance mySignature : Signature :=
{| variables := StringMLVariables;
ml_symbols := {|
symbols := exampleSymbols;
sym_eqdec := exampleSymbols_eqdec;
|};
|}.
Inductive exampleDomain : Set :=
| one | two | f.
Theorem exampleDomain_Inhabited : Inhabited exampleDomain.
Definition example_app_interp (d1 d2 : exampleDomain) : propset exampleDomain :=
match d1, d2 with
| f, one ⇒ ⊤
| f, two ⇒ ∅
| _, _ ⇒ ∅
end.
Definition exampleModel : @Model mySignature :=
{|
Domain := exampleDomain;
Domain_inhabited := exampleDomain_Inhabited;
sym_interp := fun (x : symbols) ⇒
{[ f ]};
app_interp := example_app_interp;
|}.
Example equiv_not_eq :
∀ ρ, @eval _ exampleModel ρ (ex , (patt_sym sym_f ⋅ patt_free_evar "x"%string <---> b0)) = ⊤.
Close Scope ml_scope.
End equivalence_insufficient.
Module equivalence_insufficient2.
Open Scope ml_scope.
Inductive exampleSymbols : Set :=
| sym_f
| sym_g.
#[local]
Instance mySignature : Signature :=
{| variables := StringMLVariables;
ml_symbols := {|
symbols := exampleSymbols;
sym_eqdec := exampleSymbols_eqdec;
|};
|}.
Inductive exampleDomain : Set :=
| one | two | f | g.
Instance exampleDomain_Inhabited : Inhabited exampleDomain.
Definition example_sym_interp (x : symbols) : propset exampleDomain :=
match x with
| sym_f ⇒ {[f]}
| sym_g ⇒ {[g]}
end.
Definition example_app_interp (d1 d2 : exampleDomain) : propset exampleDomain :=
match d1, d2 with
| g, f ⇒ {[two]}
| g, g ⇒ {[f]}
| _, _ ⇒ ∅
end.
Definition exampleModel : @Model mySignature :=
{|
Domain := exampleDomain;
Domain_inhabited := exampleDomain_Inhabited;
sym_interp := example_sym_interp;
app_interp := example_app_interp;
|}.
Theorem app_ext_singleton : ∀ x y,
app_ext {[x]} {[y]} = @app_interp mySignature exampleModel x y.
Example equiv_elim_not :
∀ ρ,
@eval _ exampleModel ρ
(patt_sym sym_f <---> patt_sym sym_g --->
patt_sym sym_g ⋅ patt_sym sym_f ---> patt_sym sym_g ⋅ patt_sym sym_g) ≠ ⊤.
From MatchingLogic Require Import StringSignature.
Module equivalence_insufficient.
Open Scope ml_scope.
Inductive exampleSymbols : Set :=
| sym_f.
#[local]
Instance mySignature : Signature :=
{| variables := StringMLVariables;
ml_symbols := {|
symbols := exampleSymbols;
sym_eqdec := exampleSymbols_eqdec;
|};
|}.
Inductive exampleDomain : Set :=
| one | two | f.
Theorem exampleDomain_Inhabited : Inhabited exampleDomain.
Definition example_app_interp (d1 d2 : exampleDomain) : propset exampleDomain :=
match d1, d2 with
| f, one ⇒ ⊤
| f, two ⇒ ∅
| _, _ ⇒ ∅
end.
Definition exampleModel : @Model mySignature :=
{|
Domain := exampleDomain;
Domain_inhabited := exampleDomain_Inhabited;
sym_interp := fun (x : symbols) ⇒
{[ f ]};
app_interp := example_app_interp;
|}.
Example equiv_not_eq :
∀ ρ, @eval _ exampleModel ρ (ex , (patt_sym sym_f ⋅ patt_free_evar "x"%string <---> b0)) = ⊤.
Close Scope ml_scope.
End equivalence_insufficient.
Module equivalence_insufficient2.
Open Scope ml_scope.
Inductive exampleSymbols : Set :=
| sym_f
| sym_g.
#[local]
Instance mySignature : Signature :=
{| variables := StringMLVariables;
ml_symbols := {|
symbols := exampleSymbols;
sym_eqdec := exampleSymbols_eqdec;
|};
|}.
Inductive exampleDomain : Set :=
| one | two | f | g.
Instance exampleDomain_Inhabited : Inhabited exampleDomain.
Definition example_sym_interp (x : symbols) : propset exampleDomain :=
match x with
| sym_f ⇒ {[f]}
| sym_g ⇒ {[g]}
end.
Definition example_app_interp (d1 d2 : exampleDomain) : propset exampleDomain :=
match d1, d2 with
| g, f ⇒ {[two]}
| g, g ⇒ {[f]}
| _, _ ⇒ ∅
end.
Definition exampleModel : @Model mySignature :=
{|
Domain := exampleDomain;
Domain_inhabited := exampleDomain_Inhabited;
sym_interp := example_sym_interp;
app_interp := example_app_interp;
|}.
Theorem app_ext_singleton : ∀ x y,
app_ext {[x]} {[y]} = @app_interp mySignature exampleModel x y.
Example equiv_elim_not :
∀ ρ,
@eval _ exampleModel ρ
(patt_sym sym_f <---> patt_sym sym_g --->
patt_sym sym_g ⋅ patt_sym sym_f ---> patt_sym sym_g ⋅ patt_sym sym_g) ≠ ⊤.
First, we simplify the interpretation
Next, we simplify the model-specific parts:
Now we derive a counterexample by showing that the element "two"
won't be in the LHS of H. This only involves simplification of set
operations.
End equivalence_insufficient2.
#[export]
Hint Resolve T_predicate_defined : core.
#[export]
Hint Resolve T_predicate_total : core.
#[export]
Hint Resolve T_predicate_subseteq : core.
#[export]
Hint Resolve T_predicate_equals : core.
#[export]
Hint Resolve T_predicate_in : core.
This page has been generated by coqdoc