File FOEquality_ProofSystem
From MatchingLogic Require Export DeductionTheorem.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Open Scope list_scope.
Lemma membership_imp_equal {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) --->
(ex , (φ' =ml b0)) --->
(φ ∈ml φ') ---> (φ =ml φ').
Lemma membership_imp_equal_meta {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) →
Γ ⊢ (ex , (φ' =ml b0)) →
Γ ⊢ (φ ∈ml φ') ---> (φ =ml φ') .
Lemma membership_impl_subseteq {Σ : Signature} {syntax : Syntax} Γ g ψ :
theory ⊆ Γ → mu_free ψ → mu_free g →
well_formed g → well_formed ψ →
Γ ⊢ (ex , (g =ml b0)) →
Γ ⊢ (g ∈ml ψ) →
Γ ⊢ (g ⊆ml ψ).
Lemma functional_pattern_defined {Σ : Signature} {syntax : Syntax} :
∀ Γ φ, theory ⊆ Γ → well_formed φ →
Γ ⊢ (ex , (φ =ml b0)) ---> ⌈ φ ⌉.
Lemma membership_equal_equal {Σ : Signature} {syntax : Syntax} :
∀ Γ φ φ',
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) →
Γ ⊢ (ex , (φ' =ml b0)) →
Γ ⊢ (φ ∈ml φ') =ml (φ =ml φ') .
Lemma funcional_application {Σ : Signature} {syntax : Syntax} Γ t1 t2 :
theory ⊆ Γ →
well_formed t1 →
well_formed t2 →
Γ ⊢ (ex , t2 =ml b0) ---> (all , ex , (t1 ⋅ b1)%ml =ml b0) --->
ex , (t1 ⋅ t2)%ml =ml b0.
Section nary_functions.
Context {Σ : Signature} {syntax : Syntax}.
Fixpoint nary_function (f : Pattern) (n : nat) :=
match n with
| 0 ⇒ ex , f =ml b0
| S n' ⇒ all , nary_function (f ⋅ patt_bound_evar (S n')) n'
end.
Definition nary_function_symbol (f : symbols) (n : nat) := nary_function (patt_sym f) n.
Eval simpl in nary_function patt_bott 3.
Lemma nary_function_well_formed_positive :
∀ n φ, well_formed_positive φ → well_formed_positive (nary_function φ n).
Lemma nary_function_well_formed_closed_mu_aux :
∀ m n φ, well_formed_closed_mu_aux φ n →
well_formed_closed_mu_aux (nary_function φ m) n.
Lemma nary_function_well_formed_closed_ex_aux_helper :
∀ m n φ,
n > m →
well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (nary_function φ m) (n - S m).
Lemma nary_function_well_formed_closed_ex_aux :
∀ m n φ, well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (nary_function φ m) (n - S m).
Lemma nary_function_mu_free :
∀ m φ, mu_free φ → mu_free (nary_function φ m).
Lemma nary_function_bevar_subst :
∀ m n φ ψ,
(nary_function φ m)^[evar:n↦ψ] =
(nary_function φ^[evar: S m + n ↦ ψ] m).
Lemma function_application_many Γ l φ :
theory ⊆ Γ →
wf l →
well_formed φ →
mu_free φ →
foldr andb true (map mu_free l) →
Γ ⊢ nary_function φ (length l) --->
foldr (fun p acc ⇒ (ex , p =ml b0) ---> acc)
(ex , foldl patt_app φ l =ml b0) l.
End nary_functions.
Fixpoint deconstruct_function {Σ : Signature} (pat : Pattern) : option (symbols × list Pattern) :=
match pat with
| patt_app t1 t2 ⇒ match deconstruct_function t1 with
| Some (f, pats) ⇒ Some (f, pats ++ [t2])
| _ ⇒ None
end
| patt_sym s ⇒ Some (s, [])
| _ ⇒ None
end.
Ltac mlSplitAnds :=
match goal with
[ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (patt_and _ _) _)] ⇒
mlSplitAnd; mlSplitAnds
| _ ⇒ idtac
end.
Ltac solve_functional_var :=
lazymatch goal with
[ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (ex, patt_free_evar ?x =ml b0) _)] ⇒
mlExists x;
mlSimpl; cbn; try (rewrite bevar_subst_not_occur; wf_auto2);
mlReflexivity
| [ |- _ ] ⇒ fail "Not a functional variable claim"
end.
Ltac solve_functional_symbol :=
(* TODO: check the shape, this tactic is fragile *)
fromMLGoal;
gapply hypothesis;
try assumption;
wf_auto2;
set_solver
.
Ltac solve_functional_step :=
lazymatch goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (ex, ?p =ml patt_bound_evar 0) _)] ⇒
lazymatch eval cbv in (deconstruct_function p) with
| Some (?f, ?p::?pats) ⇒
mlApplyMeta (function_application_many Γ (p::pats) (patt_sym f) ltac:(set_solver) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(by simpl) ltac:(by simpl));
try mlSplitAnds
| Some (?f, []) ⇒ solve_functional_symbol
| None ⇒ fail "Claim does not contain a first function symbol"
end
| _ ⇒ fail "Claim is not shaped as 'ex, <pat> =ml b0'"
end.
Ltac solve_functional :=
(repeat solve_functional_step); try solve_functional_var; try solve_functional_symbol.
Goal
∀ {Σ : Signature} {syntax: Syntax} f g one Γ x y,
theory ⊆ Γ →
(all, all, all, ex, patt_app (patt_app (patt_app (patt_sym f) b3) b2) b1 =ml b0) ∈ Γ →
(all, ex, patt_app (patt_sym g) b1 =ml b0) ∈ Γ →
(ex , patt_sym one =ml b0) ∈ Γ →
Γ ⊢ ex, (patt_sym f ⋅ patt_free_evar x ⋅ (patt_sym g ⋅ patt_sym one) ⋅ (patt_sym g ⋅ patt_free_evar y))%ml =ml b0.
Theorem exists_functional_subst_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ φ' : Pattern) ,
Definedness_Syntax.theory ⊆ Γ →
mu_free φ →
well_formed φ' →
well_formed_closed_ex_aux φ 1 →
well_formed_closed_mu_aux φ 0 →
Γ ⊢ (ex , φ)^[φ'] →
Γ ⊢ is_functional φ' →
Γ ⊢i (ex , φ) using AnyReasoning.
Theorem membership_monotone_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern) (i : ProofInfo),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Γ ⊢i is_functional t using i →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i t ∈ml φ₁ ---> t ∈ml φ₂ using i .
Theorem membership_or_2_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t --->
t ∈ml φ₁ or t ∈ml φ₂ --->
t ∈ml (φ₁ or φ₂) using AnyReasoning.
Theorem membership_or_2_functional_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t using AnyReasoning →
Γ ⊢i t ∈ml φ₁ or t ∈ml φ₂ --->
t ∈ml (φ₁ or φ₂) using AnyReasoning.
Theorem membership_and_2_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ →
mu_free φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t --->
t ∈ml φ₁ and t ∈ml φ₂ --->
t ∈ml (φ₁ and φ₂) using AnyReasoning.
Theorem membership_and_2_functional_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ →
mu_free φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢ is_functional t →
Γ ⊢i t ∈ml φ₁ and t ∈ml φ₂ --->
t ∈ml (φ₁ and φ₂) using AnyReasoning.
Theorem membership_symbol_ceil_aux_0_functional:∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ t1 t2 : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
mu_free φ →
well_formed t1 →
well_formed t2 →
mu_free t2 →
Γ ⊢i is_functional t1 --->
is_functional t2 --->
⌈ t1 and φ ⌉ --->
⌈ t2 and ⌈ t1 and φ ⌉ ⌉ using AnyReasoning.
Theorem proved_membership_functional:
∀ {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
(Γ : Theory) (φ₁ φ₂ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ using AnyReasoning →
Γ ⊢i is_functional φ₂ ---> φ₂ ∈ml φ₁ using AnyReasoning .
Theorem proved_membership_functional_meta:
∀ {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
(Γ : Theory) (φ₁ φ₂ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i is_functional φ₂ using AnyReasoning →
Γ ⊢i φ₁ using AnyReasoning →
Γ ⊢i φ₂ ∈ml φ₁ using AnyReasoning .
(* Equality elimination for substitution using a functional *)
(* pattern. *)
Lemma equality_elimination_functional_subst {Σ : Signature} {syntax : Syntax} (Γ : Theory) p q p1 p2 x :
theory ⊆ Γ →
well_formed p →
well_formed q →
well_formed p1 →
well_formed p2 →
mu_free p →
mu_free q →
pattern_kt_well_formed p1 →
pattern_kt_well_formed p2 →
Γ ⊢ p =ml q →
Γ ⊢ p1 =ml p2 →
Γ ⊢ is_functional p1 →
Γ ⊢ p^[[evar: x ↦ p1]] =ml q^[[evar: x ↦ p2]].
Section EqCon.
Context {Σ : Signature} {syntax : Syntax}.
(* The remainder works for any theory containing definedness. *)
Context (Γ : Theory).
Hypothesis (HΓ : theory ⊆ Γ).
(* The patterns that will be equal, *)
(* and the evars that they will replace. *)
Context (σ : list (evar × Pattern × Pattern)).
(* They are well-formed... *)
Hypothesis (Hσ1 : wf (map (snd ∘ fst) σ)) (Hσ2 : wf (map snd σ)).
(* ... mu-free ... *)
Hypothesis (Hmfσ1 : foldr (fun c a ⇒ mu_free c && a) true (map (snd ∘ fst) σ)).
Hypothesis (Hmfσ2 : foldr (fun c a ⇒ mu_free c && a) true (map snd σ)).
(* ... and one of them is functional. *)
Hypothesis (Hfpσ : foldr (fun c a ⇒ ((Γ ⊢ is_functional c.1.2) × a)%type) unit σ).
(* Separate equalities as a hypothesis. *)
Definition hypos : Type := foldr (fun x t ⇒ ((Γ ⊢ x.1.2 =ml x.2) × t)%type) unit σ.
(* Same as `emplace`ing into a context with multiple holes. *)
Definition goal (φ : Pattern) : Pattern := (foldr (fun x p ⇒ p^[[evar: x.1.1 ↦ x.1.2]]) φ σ) =ml (foldr (fun x p ⇒ p^[[evar: x.1.1 ↦ x.2]]) φ σ).
(* For any pattern (which would serve as the core of the context), *)
(* given the eqalities as hypothesis, substituting into the *)
(* multihole context yields equality. *)
Lemma eqcon : ∀ φ,
well_formed φ →
mu_free φ →
hypos →
Γ ⊢ goal φ.
End EqCon.
Section Example.
Context {Σ : Signature} {syntax : Syntax}.
(* In any theory that contains the theory of definedness ... *)
Context (Γ : Theory).
Hypothesis (HΓ : theory ⊆ Γ).
(* ... given some function/context ... *)
Context (kseq_sym : symbols).
Definition kseq x y := patt_sym kseq_sym ⋅ x ⋅ y.
(* ... and two pairs of patterns ... *)
Context (one two one' two' : Pattern).
(* ... some of which are functional and all of which are *)
(* well-formed and free of fixed points ... *)
Hypothesis (fpone : Γ ⊢ is_functional one).
Hypothesis (fptwo : Γ ⊢ is_functional two).
Hypothesis (Hwf : well_formed one ∧ well_formed two ∧ well_formed one' ∧ well_formed two').
Hypothesis (Hmf : mu_free one ∧ mu_free two ∧ mu_free one' ∧ mu_free two').
(* ... and pairwise provable equal ... *)
Hypothesis (Heqone : Γ ⊢ one =ml one').
Hypothesis (Heqtwo : Γ ⊢ two =ml two').
(* ... and given two different evars, one of which is free *)
(* in two of the patterns ... *)
Context (x y : evar).
Hypothesis (Hxneqy : y ≠ x).
Hypothesis (Hxfree : x ∉ free_evars two ∪ free_evars two').
(* ... substituting the two into the same context *)
(* is also equal. *)
(* one = one' two = two' *)
(* ------------------------------------------------- *)
(* (kseq □₁ □₂)one, two = (kseq □₁ □₂)one', two' *)
Goal Γ ⊢ kseq one two =ml kseq one' two'.
End Example.
Lemma predicate_iff {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂ :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ --->
is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ <---> φ₂).
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Open Scope list_scope.
Lemma membership_imp_equal {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) --->
(ex , (φ' =ml b0)) --->
(φ ∈ml φ') ---> (φ =ml φ').
Lemma membership_imp_equal_meta {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) →
Γ ⊢ (ex , (φ' =ml b0)) →
Γ ⊢ (φ ∈ml φ') ---> (φ =ml φ') .
Lemma membership_impl_subseteq {Σ : Signature} {syntax : Syntax} Γ g ψ :
theory ⊆ Γ → mu_free ψ → mu_free g →
well_formed g → well_formed ψ →
Γ ⊢ (ex , (g =ml b0)) →
Γ ⊢ (g ∈ml ψ) →
Γ ⊢ (g ⊆ml ψ).
Lemma functional_pattern_defined {Σ : Signature} {syntax : Syntax} :
∀ Γ φ, theory ⊆ Γ → well_formed φ →
Γ ⊢ (ex , (φ =ml b0)) ---> ⌈ φ ⌉.
Lemma membership_equal_equal {Σ : Signature} {syntax : Syntax} :
∀ Γ φ φ',
theory ⊆ Γ → mu_free φ' →
well_formed φ → well_formed φ' →
Γ ⊢ (ex , (φ =ml b0)) →
Γ ⊢ (ex , (φ' =ml b0)) →
Γ ⊢ (φ ∈ml φ') =ml (φ =ml φ') .
Lemma funcional_application {Σ : Signature} {syntax : Syntax} Γ t1 t2 :
theory ⊆ Γ →
well_formed t1 →
well_formed t2 →
Γ ⊢ (ex , t2 =ml b0) ---> (all , ex , (t1 ⋅ b1)%ml =ml b0) --->
ex , (t1 ⋅ t2)%ml =ml b0.
Section nary_functions.
Context {Σ : Signature} {syntax : Syntax}.
Fixpoint nary_function (f : Pattern) (n : nat) :=
match n with
| 0 ⇒ ex , f =ml b0
| S n' ⇒ all , nary_function (f ⋅ patt_bound_evar (S n')) n'
end.
Definition nary_function_symbol (f : symbols) (n : nat) := nary_function (patt_sym f) n.
Eval simpl in nary_function patt_bott 3.
Lemma nary_function_well_formed_positive :
∀ n φ, well_formed_positive φ → well_formed_positive (nary_function φ n).
Lemma nary_function_well_formed_closed_mu_aux :
∀ m n φ, well_formed_closed_mu_aux φ n →
well_formed_closed_mu_aux (nary_function φ m) n.
Lemma nary_function_well_formed_closed_ex_aux_helper :
∀ m n φ,
n > m →
well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (nary_function φ m) (n - S m).
Lemma nary_function_well_formed_closed_ex_aux :
∀ m n φ, well_formed_closed_ex_aux φ n →
well_formed_closed_ex_aux (nary_function φ m) (n - S m).
Lemma nary_function_mu_free :
∀ m φ, mu_free φ → mu_free (nary_function φ m).
Lemma nary_function_bevar_subst :
∀ m n φ ψ,
(nary_function φ m)^[evar:n↦ψ] =
(nary_function φ^[evar: S m + n ↦ ψ] m).
Lemma function_application_many Γ l φ :
theory ⊆ Γ →
wf l →
well_formed φ →
mu_free φ →
foldr andb true (map mu_free l) →
Γ ⊢ nary_function φ (length l) --->
foldr (fun p acc ⇒ (ex , p =ml b0) ---> acc)
(ex , foldl patt_app φ l =ml b0) l.
End nary_functions.
Fixpoint deconstruct_function {Σ : Signature} (pat : Pattern) : option (symbols × list Pattern) :=
match pat with
| patt_app t1 t2 ⇒ match deconstruct_function t1 with
| Some (f, pats) ⇒ Some (f, pats ++ [t2])
| _ ⇒ None
end
| patt_sym s ⇒ Some (s, [])
| _ ⇒ None
end.
Ltac mlSplitAnds :=
match goal with
[ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (patt_and _ _) _)] ⇒
mlSplitAnd; mlSplitAnds
| _ ⇒ idtac
end.
Ltac solve_functional_var :=
lazymatch goal with
[ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (ex, patt_free_evar ?x =ml b0) _)] ⇒
mlExists x;
mlSimpl; cbn; try (rewrite bevar_subst_not_occur; wf_auto2);
mlReflexivity
| [ |- _ ] ⇒ fail "Not a functional variable claim"
end.
Ltac solve_functional_symbol :=
(* TODO: check the shape, this tactic is fragile *)
fromMLGoal;
gapply hypothesis;
try assumption;
wf_auto2;
set_solver
.
Ltac solve_functional_step :=
lazymatch goal with
| [ |- @of_MLGoal _ (@mkMLGoal _ ?Γ _ (ex, ?p =ml patt_bound_evar 0) _)] ⇒
lazymatch eval cbv in (deconstruct_function p) with
| Some (?f, ?p::?pats) ⇒
mlApplyMeta (function_application_many Γ (p::pats) (patt_sym f) ltac:(set_solver) ltac:(wf_auto2) ltac:(wf_auto2) ltac:(by simpl) ltac:(by simpl));
try mlSplitAnds
| Some (?f, []) ⇒ solve_functional_symbol
| None ⇒ fail "Claim does not contain a first function symbol"
end
| _ ⇒ fail "Claim is not shaped as 'ex, <pat> =ml b0'"
end.
Ltac solve_functional :=
(repeat solve_functional_step); try solve_functional_var; try solve_functional_symbol.
Goal
∀ {Σ : Signature} {syntax: Syntax} f g one Γ x y,
theory ⊆ Γ →
(all, all, all, ex, patt_app (patt_app (patt_app (patt_sym f) b3) b2) b1 =ml b0) ∈ Γ →
(all, ex, patt_app (patt_sym g) b1 =ml b0) ∈ Γ →
(ex , patt_sym one =ml b0) ∈ Γ →
Γ ⊢ ex, (patt_sym f ⋅ patt_free_evar x ⋅ (patt_sym g ⋅ patt_sym one) ⋅ (patt_sym g ⋅ patt_free_evar y))%ml =ml b0.
Theorem exists_functional_subst_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ φ' : Pattern) ,
Definedness_Syntax.theory ⊆ Γ →
mu_free φ →
well_formed φ' →
well_formed_closed_ex_aux φ 1 →
well_formed_closed_mu_aux φ 0 →
Γ ⊢ (ex , φ)^[φ'] →
Γ ⊢ is_functional φ' →
Γ ⊢i (ex , φ) using AnyReasoning.
Theorem membership_monotone_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern) (i : ProofInfo),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Γ ⊢i is_functional t using i →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i t ∈ml φ₁ ---> t ∈ml φ₂ using i .
Theorem membership_or_2_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t --->
t ∈ml φ₁ or t ∈ml φ₂ --->
t ∈ml (φ₁ or φ₂) using AnyReasoning.
Theorem membership_or_2_functional_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t using AnyReasoning →
Γ ⊢i t ∈ml φ₁ or t ∈ml φ₂ --->
t ∈ml (φ₁ or φ₂) using AnyReasoning.
Theorem membership_and_2_functional: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ →
mu_free φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢i is_functional t --->
t ∈ml φ₁ and t ∈ml φ₂ --->
t ∈ml (φ₁ and φ₂) using AnyReasoning.
Theorem membership_and_2_functional_meta: ∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ₁ φ₂ t : Pattern),
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ →
mu_free φ₂ →
well_formed t →
Definedness_Syntax.theory ⊆ Γ →
Γ ⊢ is_functional t →
Γ ⊢i t ∈ml φ₁ and t ∈ml φ₂ --->
t ∈ml (φ₁ and φ₂) using AnyReasoning.
Theorem membership_symbol_ceil_aux_0_functional:∀ {Σ : Signature} {syntax : Syntax} (Γ : Theory) (φ t1 t2 : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
mu_free φ →
well_formed t1 →
well_formed t2 →
mu_free t2 →
Γ ⊢i is_functional t1 --->
is_functional t2 --->
⌈ t1 and φ ⌉ --->
⌈ t2 and ⌈ t1 and φ ⌉ ⌉ using AnyReasoning.
Theorem proved_membership_functional:
∀ {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
(Γ : Theory) (φ₁ φ₂ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ using AnyReasoning →
Γ ⊢i is_functional φ₂ ---> φ₂ ∈ml φ₁ using AnyReasoning .
Theorem proved_membership_functional_meta:
∀ {Σ : Signature} {syntax : Definedness_Syntax.Syntax}
(Γ : Theory) (φ₁ φ₂ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i is_functional φ₂ using AnyReasoning →
Γ ⊢i φ₁ using AnyReasoning →
Γ ⊢i φ₂ ∈ml φ₁ using AnyReasoning .
(* Equality elimination for substitution using a functional *)
(* pattern. *)
Lemma equality_elimination_functional_subst {Σ : Signature} {syntax : Syntax} (Γ : Theory) p q p1 p2 x :
theory ⊆ Γ →
well_formed p →
well_formed q →
well_formed p1 →
well_formed p2 →
mu_free p →
mu_free q →
pattern_kt_well_formed p1 →
pattern_kt_well_formed p2 →
Γ ⊢ p =ml q →
Γ ⊢ p1 =ml p2 →
Γ ⊢ is_functional p1 →
Γ ⊢ p^[[evar: x ↦ p1]] =ml q^[[evar: x ↦ p2]].
Section EqCon.
Context {Σ : Signature} {syntax : Syntax}.
(* The remainder works for any theory containing definedness. *)
Context (Γ : Theory).
Hypothesis (HΓ : theory ⊆ Γ).
(* The patterns that will be equal, *)
(* and the evars that they will replace. *)
Context (σ : list (evar × Pattern × Pattern)).
(* They are well-formed... *)
Hypothesis (Hσ1 : wf (map (snd ∘ fst) σ)) (Hσ2 : wf (map snd σ)).
(* ... mu-free ... *)
Hypothesis (Hmfσ1 : foldr (fun c a ⇒ mu_free c && a) true (map (snd ∘ fst) σ)).
Hypothesis (Hmfσ2 : foldr (fun c a ⇒ mu_free c && a) true (map snd σ)).
(* ... and one of them is functional. *)
Hypothesis (Hfpσ : foldr (fun c a ⇒ ((Γ ⊢ is_functional c.1.2) × a)%type) unit σ).
(* Separate equalities as a hypothesis. *)
Definition hypos : Type := foldr (fun x t ⇒ ((Γ ⊢ x.1.2 =ml x.2) × t)%type) unit σ.
(* Same as `emplace`ing into a context with multiple holes. *)
Definition goal (φ : Pattern) : Pattern := (foldr (fun x p ⇒ p^[[evar: x.1.1 ↦ x.1.2]]) φ σ) =ml (foldr (fun x p ⇒ p^[[evar: x.1.1 ↦ x.2]]) φ σ).
(* For any pattern (which would serve as the core of the context), *)
(* given the eqalities as hypothesis, substituting into the *)
(* multihole context yields equality. *)
Lemma eqcon : ∀ φ,
well_formed φ →
mu_free φ →
hypos →
Γ ⊢ goal φ.
End EqCon.
Section Example.
Context {Σ : Signature} {syntax : Syntax}.
(* In any theory that contains the theory of definedness ... *)
Context (Γ : Theory).
Hypothesis (HΓ : theory ⊆ Γ).
(* ... given some function/context ... *)
Context (kseq_sym : symbols).
Definition kseq x y := patt_sym kseq_sym ⋅ x ⋅ y.
(* ... and two pairs of patterns ... *)
Context (one two one' two' : Pattern).
(* ... some of which are functional and all of which are *)
(* well-formed and free of fixed points ... *)
Hypothesis (fpone : Γ ⊢ is_functional one).
Hypothesis (fptwo : Γ ⊢ is_functional two).
Hypothesis (Hwf : well_formed one ∧ well_formed two ∧ well_formed one' ∧ well_formed two').
Hypothesis (Hmf : mu_free one ∧ mu_free two ∧ mu_free one' ∧ mu_free two').
(* ... and pairwise provable equal ... *)
Hypothesis (Heqone : Γ ⊢ one =ml one').
Hypothesis (Heqtwo : Γ ⊢ two =ml two').
(* ... and given two different evars, one of which is free *)
(* in two of the patterns ... *)
Context (x y : evar).
Hypothesis (Hxneqy : y ≠ x).
Hypothesis (Hxfree : x ∉ free_evars two ∪ free_evars two').
(* ... substituting the two into the same context *)
(* is also equal. *)
(* one = one' two = two' *)
(* ------------------------------------------------- *)
(* (kseq □₁ □₂)one, two = (kseq □₁ □₂)one', two' *)
Goal Γ ⊢ kseq one two =ml kseq one' two'.
End Example.
Lemma predicate_iff {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂ :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ --->
is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ <---> φ₂).
This page has been generated by coqdoc