File Sorts_Syntax
From MatchingLogic Require Export Definedness_Syntax.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Inductive Symbols := sym_inh | sym_sorts.
Global Instance Symbols_eqdec : EqDecision Symbols.
#[global]
Program Instance Symbols_finite : finite.Finite Symbols.
Global Instance Symbols_countable : countable.Countable Symbols.
Section sorts_syntax.
Context {Σ : Signature}.
Class Syntax :=
{ sym_inj : Symbols → symbols;
imported_definedness : Definedness_Syntax.Syntax;
}.
#[global] Existing Instance imported_definedness.
Context {self : Syntax}.
Local Definition sym (s : Symbols) : Pattern :=
patt_sym (sym_inj s).
Definition inhabitant := sym sym_inh.
Definition Sorts := sym sym_sorts.
Example test_pattern_1 := patt_equal (inhabitant) (inhabitant).
Definition patt_inhabitant_set(phi : Pattern) : Pattern := inhabitant ⋅ phi.
Definition patt_element_of (φ ψ : Pattern) := ⌈ φ and ψ ⌉.
End sorts_syntax.
Section sorts.
Context {Σ : Signature}.
Context {self : Syntax}.
Open Scope ml_scope.
Local Notation "〚 phi 〛" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Obligation Tactic := idtac.
Class ESortedBinder (binder : Pattern → Pattern → Pattern) := {
esorted_binder_morphism :
∀ {A : Type} (f : A → Pattern → Pattern)
(f_morph : PatternMorphism f)
(f_swap : SwappableEx f nest_ex f_morph)
(s phi : Pattern) a,
f a (binder s phi) = binder (f a s) (f (increase_ex pm_spec_data a) phi) ;
}.
#[global]
Program Instance Unary_inhabitant_set : Unary patt_inhabitant_set := {}.
Definition patt_sorted_neg (sort phi : Pattern) : Pattern :=
〚sort〛 and ! phi.
#[global]
Program Instance Binary_sorted_neg : Binary patt_sorted_neg := {}.
Definition patt_sorted_exists (sort phi : Pattern) : Pattern :=
ex , ((b0 ∈ml 〚nest_ex sort〛) and phi).
Local Notation "'ex' s , phi" :=
(patt_sorted_exists s phi) (at level 70) : ml_scope.
#[global]
Program Instance sorted_exists_binder : ESortedBinder patt_sorted_exists := {}.
Definition patt_sorted_forall (sort phi : Pattern) : Pattern :=
all , ((b0 ∈ml 〚nest_ex sort〛) ---> phi).
Local Notation "'all' s , phi" :=
(patt_sorted_forall s phi) (at level 70) : ml_scope.
#[global]
Program Instance sorted_forall_binder : ESortedBinder patt_sorted_forall := {}.
Definition patt_forall_sort (φ : Pattern) : Pattern :=
all Sorts , φ.
Local Notation "'allₛ' , phi" :=
(patt_forall_sort phi) (at level 70) : ml_scope.
Definition patt_exists_sort (φ : Pattern) : Pattern :=
ex Sorts , φ.
Local Notation "'exₛ' , phi" :=
(patt_exists_sort phi) (at level 70) : ml_scope.
#[global]
Program Instance forall_sort_ebinder : EBinder patt_forall_sort := {}.
#[global]
Program Instance exists_sort_ebinder : EBinder patt_exists_sort := {}.
(* TODO patt_sorted_forall and patt_sorted_exists are duals - a lemma *)
Definition patt_total_function(phi from to : Pattern) : Pattern :=
all from , (ex (nest_ex to) , ((nest_ex (nest_ex phi) ⋅ b1) =ml b0)).
Definition patt_partial_function(phi from to : Pattern) : Pattern :=
all from , (ex (nest_ex to), ((nest_ex (nest_ex phi) ⋅ b1) ⊆ml b0)).
(* Assuming `f` is a total function, says it is injective on given domain. Does not quite work for partial functions. *)
Definition patt_total_function_injective f from : Pattern :=
all from , (all (nest_ex from) ,
(((nest_ex (nest_ex f) ⋅ b1) =ml (nest_ex (nest_ex f) ⋅ b0)) --->
(b1 =ml b0))).
(* Assuming `f` is a partial function, says it is injective on given domain. Works for total functions, too. *)
Definition patt_partial_function_injective f from : Pattern :=
all
from ,
(all
(nest_ex from) ,
(
! ((nest_ex (nest_ex f) ⋅ b1) =ml ⊥ )
--->
((nest_ex (nest_ex f) ⋅ b1) =ml (nest_ex (nest_ex f) ⋅ b0))
---> (b1 =ml b0))).
Definition patt_total_binary_function(phi from1 from2 to : Pattern)
: Pattern :=
patt_sorted_forall from1 (
patt_sorted_forall (nest_ex from2) (
patt_sorted_exists (nest_ex (nest_ex to)) (
(((nest_ex (nest_ex (nest_ex phi)) ⋅ b2) ⋅ b1) =ml b0)
)
)
)
.
End sorts.
Module Notations.
Notation "⟦ phi ⟧" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Notation "'all' s , phi" := (patt_sorted_forall s phi) (at level 80) : ml_scope.
Notation "'ex' s , phi" := (patt_sorted_exists s phi) (at level 80) : ml_scope.
Notation "'allₛ' , phi" :=
(patt_forall_sort phi) (at level 80) : ml_scope.
Notation "'exₛ' , phi" :=
(patt_exists_sort phi) (at level 80) : ml_scope.
Notation "phi :ml s1 × s2 -> s3" := (patt_total_binary_function phi s1 s2 s3) (at level 70) : ml_scope.
End Notations.
Ltac mlESortedSimpl_single :=
match goal with
| |- context G [?f ?arg _ (?binder _ _)] ⇒
let Hyp := fresh "H" in
let Hyp2 := fresh "H" in
(* We check whether we have a sorted binder *)
assert (Hyp: ESortedBinder binder) by (typeclasses eauto + eauto);
(* We check wether we found a swappable substitution *)
assert (Hyp2: SwappableEx (f arg) nest_ex _) by (typeclasses eauto + eauto);
(* The previous checks are needed to correctly identify the position for
simplification, since using only rewrite fails on finding the right
instances *)
erewrite (@esorted_binder_morphism _ _ Hyp _ _ _ Hyp2);
clear Hyp Hyp2;
try rewrite [increase_ex _ _]/=
end.
Ltac mlESortedSimpl_single_hyp H :=
match type of H with
| context G [?f ?arg _ (?binder _ _)] ⇒
let Hyp := fresh "H" in
let Hyp2 := fresh "H" in
(* We check whether we have a sorted binder *)
assert (Hyp: ESortedBinder binder) by (typeclasses eauto + eauto);
(* We check wether we found a swappable substitution *)
assert (Hyp2: SwappableEx (f arg) nest_ex _) by (typeclasses eauto + eauto);
(* The previous checks are needed to correctly identify the position for
simplification, since using only rewrite fails on finding the right
instances *)
erewrite (@esorted_binder_morphism _ _ Hyp _ _ _ Hyp2) in H;
clear Hyp Hyp2;
try rewrite [increase_ex _ _]/= in H
end.
(* TODO: extend with mu *)
Tactic Notation "mlSortedSimpl" := repeat mlESortedSimpl_single.
Tactic Notation "mlSortedSimpl" "in" hyp(H) := repeat mlESortedSimpl_single_hyp H.
Tactic Notation "mlSimpl" := repeat (mlUnsortedSimpl; mlSortedSimpl); cbn.
Tactic Notation "mlSimpl" "in" hyp(H) := repeat (mlUnsortedSimpl in H; mlSortedSimpl in H); cbn.
Section simplTest.
(* NOTE: these tactics are not exported!!!!! *)
Import Substitution.Notations.
Import Notations.
Open Scope ml_scope.
Context {Σ : Signature} {S : Syntax}.
Goal ∀ s p x,
(all s , p)^{evar:0 ↦ x} = (all s^{evar:0 ↦ x}, p^{evar:1 ↦ x}) →
(all s , p)^{evar:0 ↦ x} = (all s^{evar:0 ↦ x}, p^{evar:1 ↦ x}).
Goal ∀ s p1 p2 p3 x,
(p1 ---> all s , p2 ---> p3)^{evar:0 ↦ x} =
(p1^{evar:0 ↦ x} ---> all s^{evar:0 ↦ x}, p2^{evar:1 ↦ x} ---> p3^{evar:1 ↦ x}).
Goal ∀ s ψ x X, well_formed_closed ψ →
(patt_sorted_forall s ψ)^[[evar: x ↦ ψ]] = patt_bott →
(patt_sorted_forall s ψ)^{evar: 0 ↦ x} = patt_bott →
(patt_sorted_forall s ψ)^{{evar: x ↦ 0}} = patt_bott →
(patt_sorted_forall s ψ)^[[svar: X ↦ ψ]] = patt_bott →
(patt_sorted_forall s ψ)^{svar: 0 ↦ X} = patt_bott →
(patt_sorted_forall s ψ)^{{svar: X ↦ 0}} = patt_bott →
(patt_sorted_forall s ψ)^[[svar: X ↦ ψ]] = patt_bott ∧
(patt_sorted_forall s ψ)^{svar: 0 ↦ X} = patt_bott ∧
(patt_sorted_forall s ψ)^{{svar: X ↦ 0}} = patt_bott ∧
(patt_sorted_forall s ψ)^[[evar: x ↦ ψ]] = patt_bott ∧
(patt_sorted_forall s ψ)^{evar: 0 ↦ x} = patt_bott ∧
(patt_sorted_forall s ψ)^{{evar: x ↦ 0}} = patt_bott
.
Goal ∀ s ψ x, (* well_formed_closed ψ -> *)
(patt_sorted_forall (patt_imp s s) ψ)^[[evar: x ↦ ψ]] = patt_bott
.
Local Definition ml_plus := patt_app.
Local Definition ml_in := patt_app.
Local Definition ml_eq := patt_app.
Import Substitution.Notations.
Import Pattern.Notations.
Import DerivedOperators_Syntax.Notations.
Import Pattern.BoundVarSugar.
Local Notation "a +ml b" := (ml_plus a b) (at level 67).
(* Local Notation "a =ml b" := (ml_eq a b) (at level 67).
Local Notation "a ∈ml b" := (ml_in a b) (at level 67). *)
(* Local Notation "'ex' , phi" := (patt_exists phi) (at level 80) : ml_scope.
Local Notation "'mu' , phi" := (patt_mu phi) (at level 80) : ml_scope.
*) Local Notation "⟦ phi ⟧" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Open Scope ml_scope.
Local Definition Nat := patt_bott.
Local Definition Zero := patt_bott.
Local Definition Succ := patt_bott.
Goal ∀ X,
(( patt_free_svar X ⊆ml ⟦ Nat ⟧ --->
Zero ∈ml patt_free_svar X --->
(all Nat, (b0 ∈ml patt_free_svar X --->
Succ ⋅ b0 ∈ml patt_free_svar X)) --->
(all Nat, b0 ∈ml patt_free_svar X ) ) ^[[svar:X↦ex Nat, b0 and Zero +ml b0 =ml b0]] ) =
( (ex Nat, b0 and Zero +ml b0 =ml b0) ⊆ml ⟦ Nat ⟧ --->
Zero ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) --->
(all Nat, (b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) --->
Succ ⋅ b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0))) --->
(all Nat, b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) ) ).
End simplTest.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Inductive Symbols := sym_inh | sym_sorts.
Global Instance Symbols_eqdec : EqDecision Symbols.
#[global]
Program Instance Symbols_finite : finite.Finite Symbols.
Global Instance Symbols_countable : countable.Countable Symbols.
Section sorts_syntax.
Context {Σ : Signature}.
Class Syntax :=
{ sym_inj : Symbols → symbols;
imported_definedness : Definedness_Syntax.Syntax;
}.
#[global] Existing Instance imported_definedness.
Context {self : Syntax}.
Local Definition sym (s : Symbols) : Pattern :=
patt_sym (sym_inj s).
Definition inhabitant := sym sym_inh.
Definition Sorts := sym sym_sorts.
Example test_pattern_1 := patt_equal (inhabitant) (inhabitant).
Definition patt_inhabitant_set(phi : Pattern) : Pattern := inhabitant ⋅ phi.
Definition patt_element_of (φ ψ : Pattern) := ⌈ φ and ψ ⌉.
End sorts_syntax.
Section sorts.
Context {Σ : Signature}.
Context {self : Syntax}.
Open Scope ml_scope.
Local Notation "〚 phi 〛" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Obligation Tactic := idtac.
Class ESortedBinder (binder : Pattern → Pattern → Pattern) := {
esorted_binder_morphism :
∀ {A : Type} (f : A → Pattern → Pattern)
(f_morph : PatternMorphism f)
(f_swap : SwappableEx f nest_ex f_morph)
(s phi : Pattern) a,
f a (binder s phi) = binder (f a s) (f (increase_ex pm_spec_data a) phi) ;
}.
#[global]
Program Instance Unary_inhabitant_set : Unary patt_inhabitant_set := {}.
Definition patt_sorted_neg (sort phi : Pattern) : Pattern :=
〚sort〛 and ! phi.
#[global]
Program Instance Binary_sorted_neg : Binary patt_sorted_neg := {}.
Definition patt_sorted_exists (sort phi : Pattern) : Pattern :=
ex , ((b0 ∈ml 〚nest_ex sort〛) and phi).
Local Notation "'ex' s , phi" :=
(patt_sorted_exists s phi) (at level 70) : ml_scope.
#[global]
Program Instance sorted_exists_binder : ESortedBinder patt_sorted_exists := {}.
Definition patt_sorted_forall (sort phi : Pattern) : Pattern :=
all , ((b0 ∈ml 〚nest_ex sort〛) ---> phi).
Local Notation "'all' s , phi" :=
(patt_sorted_forall s phi) (at level 70) : ml_scope.
#[global]
Program Instance sorted_forall_binder : ESortedBinder patt_sorted_forall := {}.
Definition patt_forall_sort (φ : Pattern) : Pattern :=
all Sorts , φ.
Local Notation "'allₛ' , phi" :=
(patt_forall_sort phi) (at level 70) : ml_scope.
Definition patt_exists_sort (φ : Pattern) : Pattern :=
ex Sorts , φ.
Local Notation "'exₛ' , phi" :=
(patt_exists_sort phi) (at level 70) : ml_scope.
#[global]
Program Instance forall_sort_ebinder : EBinder patt_forall_sort := {}.
#[global]
Program Instance exists_sort_ebinder : EBinder patt_exists_sort := {}.
(* TODO patt_sorted_forall and patt_sorted_exists are duals - a lemma *)
Definition patt_total_function(phi from to : Pattern) : Pattern :=
all from , (ex (nest_ex to) , ((nest_ex (nest_ex phi) ⋅ b1) =ml b0)).
Definition patt_partial_function(phi from to : Pattern) : Pattern :=
all from , (ex (nest_ex to), ((nest_ex (nest_ex phi) ⋅ b1) ⊆ml b0)).
(* Assuming `f` is a total function, says it is injective on given domain. Does not quite work for partial functions. *)
Definition patt_total_function_injective f from : Pattern :=
all from , (all (nest_ex from) ,
(((nest_ex (nest_ex f) ⋅ b1) =ml (nest_ex (nest_ex f) ⋅ b0)) --->
(b1 =ml b0))).
(* Assuming `f` is a partial function, says it is injective on given domain. Works for total functions, too. *)
Definition patt_partial_function_injective f from : Pattern :=
all
from ,
(all
(nest_ex from) ,
(
! ((nest_ex (nest_ex f) ⋅ b1) =ml ⊥ )
--->
((nest_ex (nest_ex f) ⋅ b1) =ml (nest_ex (nest_ex f) ⋅ b0))
---> (b1 =ml b0))).
Definition patt_total_binary_function(phi from1 from2 to : Pattern)
: Pattern :=
patt_sorted_forall from1 (
patt_sorted_forall (nest_ex from2) (
patt_sorted_exists (nest_ex (nest_ex to)) (
(((nest_ex (nest_ex (nest_ex phi)) ⋅ b2) ⋅ b1) =ml b0)
)
)
)
.
End sorts.
Module Notations.
Notation "⟦ phi ⟧" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Notation "'all' s , phi" := (patt_sorted_forall s phi) (at level 80) : ml_scope.
Notation "'ex' s , phi" := (patt_sorted_exists s phi) (at level 80) : ml_scope.
Notation "'allₛ' , phi" :=
(patt_forall_sort phi) (at level 80) : ml_scope.
Notation "'exₛ' , phi" :=
(patt_exists_sort phi) (at level 80) : ml_scope.
Notation "phi :ml s1 × s2 -> s3" := (patt_total_binary_function phi s1 s2 s3) (at level 70) : ml_scope.
End Notations.
Ltac mlESortedSimpl_single :=
match goal with
| |- context G [?f ?arg _ (?binder _ _)] ⇒
let Hyp := fresh "H" in
let Hyp2 := fresh "H" in
(* We check whether we have a sorted binder *)
assert (Hyp: ESortedBinder binder) by (typeclasses eauto + eauto);
(* We check wether we found a swappable substitution *)
assert (Hyp2: SwappableEx (f arg) nest_ex _) by (typeclasses eauto + eauto);
(* The previous checks are needed to correctly identify the position for
simplification, since using only rewrite fails on finding the right
instances *)
erewrite (@esorted_binder_morphism _ _ Hyp _ _ _ Hyp2);
clear Hyp Hyp2;
try rewrite [increase_ex _ _]/=
end.
Ltac mlESortedSimpl_single_hyp H :=
match type of H with
| context G [?f ?arg _ (?binder _ _)] ⇒
let Hyp := fresh "H" in
let Hyp2 := fresh "H" in
(* We check whether we have a sorted binder *)
assert (Hyp: ESortedBinder binder) by (typeclasses eauto + eauto);
(* We check wether we found a swappable substitution *)
assert (Hyp2: SwappableEx (f arg) nest_ex _) by (typeclasses eauto + eauto);
(* The previous checks are needed to correctly identify the position for
simplification, since using only rewrite fails on finding the right
instances *)
erewrite (@esorted_binder_morphism _ _ Hyp _ _ _ Hyp2) in H;
clear Hyp Hyp2;
try rewrite [increase_ex _ _]/= in H
end.
(* TODO: extend with mu *)
Tactic Notation "mlSortedSimpl" := repeat mlESortedSimpl_single.
Tactic Notation "mlSortedSimpl" "in" hyp(H) := repeat mlESortedSimpl_single_hyp H.
Tactic Notation "mlSimpl" := repeat (mlUnsortedSimpl; mlSortedSimpl); cbn.
Tactic Notation "mlSimpl" "in" hyp(H) := repeat (mlUnsortedSimpl in H; mlSortedSimpl in H); cbn.
Section simplTest.
(* NOTE: these tactics are not exported!!!!! *)
Import Substitution.Notations.
Import Notations.
Open Scope ml_scope.
Context {Σ : Signature} {S : Syntax}.
Goal ∀ s p x,
(all s , p)^{evar:0 ↦ x} = (all s^{evar:0 ↦ x}, p^{evar:1 ↦ x}) →
(all s , p)^{evar:0 ↦ x} = (all s^{evar:0 ↦ x}, p^{evar:1 ↦ x}).
Goal ∀ s p1 p2 p3 x,
(p1 ---> all s , p2 ---> p3)^{evar:0 ↦ x} =
(p1^{evar:0 ↦ x} ---> all s^{evar:0 ↦ x}, p2^{evar:1 ↦ x} ---> p3^{evar:1 ↦ x}).
Goal ∀ s ψ x X, well_formed_closed ψ →
(patt_sorted_forall s ψ)^[[evar: x ↦ ψ]] = patt_bott →
(patt_sorted_forall s ψ)^{evar: 0 ↦ x} = patt_bott →
(patt_sorted_forall s ψ)^{{evar: x ↦ 0}} = patt_bott →
(patt_sorted_forall s ψ)^[[svar: X ↦ ψ]] = patt_bott →
(patt_sorted_forall s ψ)^{svar: 0 ↦ X} = patt_bott →
(patt_sorted_forall s ψ)^{{svar: X ↦ 0}} = patt_bott →
(patt_sorted_forall s ψ)^[[svar: X ↦ ψ]] = patt_bott ∧
(patt_sorted_forall s ψ)^{svar: 0 ↦ X} = patt_bott ∧
(patt_sorted_forall s ψ)^{{svar: X ↦ 0}} = patt_bott ∧
(patt_sorted_forall s ψ)^[[evar: x ↦ ψ]] = patt_bott ∧
(patt_sorted_forall s ψ)^{evar: 0 ↦ x} = patt_bott ∧
(patt_sorted_forall s ψ)^{{evar: x ↦ 0}} = patt_bott
.
Goal ∀ s ψ x, (* well_formed_closed ψ -> *)
(patt_sorted_forall (patt_imp s s) ψ)^[[evar: x ↦ ψ]] = patt_bott
.
Local Definition ml_plus := patt_app.
Local Definition ml_in := patt_app.
Local Definition ml_eq := patt_app.
Import Substitution.Notations.
Import Pattern.Notations.
Import DerivedOperators_Syntax.Notations.
Import Pattern.BoundVarSugar.
Local Notation "a +ml b" := (ml_plus a b) (at level 67).
(* Local Notation "a =ml b" := (ml_eq a b) (at level 67).
Local Notation "a ∈ml b" := (ml_in a b) (at level 67). *)
(* Local Notation "'ex' , phi" := (patt_exists phi) (at level 80) : ml_scope.
Local Notation "'mu' , phi" := (patt_mu phi) (at level 80) : ml_scope.
*) Local Notation "⟦ phi ⟧" := (patt_inhabitant_set phi) (at level 0) : ml_scope.
Open Scope ml_scope.
Local Definition Nat := patt_bott.
Local Definition Zero := patt_bott.
Local Definition Succ := patt_bott.
Goal ∀ X,
(( patt_free_svar X ⊆ml ⟦ Nat ⟧ --->
Zero ∈ml patt_free_svar X --->
(all Nat, (b0 ∈ml patt_free_svar X --->
Succ ⋅ b0 ∈ml patt_free_svar X)) --->
(all Nat, b0 ∈ml patt_free_svar X ) ) ^[[svar:X↦ex Nat, b0 and Zero +ml b0 =ml b0]] ) =
( (ex Nat, b0 and Zero +ml b0 =ml b0) ⊆ml ⟦ Nat ⟧ --->
Zero ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) --->
(all Nat, (b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) --->
Succ ⋅ b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0))) --->
(all Nat, b0 ∈ml (ex Nat, b0 and Zero +ml b0 =ml b0) ) ).
End simplTest.
This page has been generated by coqdoc