File Definedness_ProofSystem
From MatchingLogic Require Export Definedness_Syntax MLPM.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Open Scope list_scope.
Section ProofSystemTheorems.
Context
{Σ : Signature}
{syntax : Syntax}
.
Definition defFP : coWfpSet := {[(exist (λ p, well_formed p = true) (definedness) erefl)]}.
Lemma phi_impl_total_phi_meta Γ φ i:
well_formed φ →
ProofInfoLe BasicReasoning i →
Γ ⊢i φ using i →
Γ ⊢i ⌊ φ ⌋ using i.
Lemma patt_iff_implies_equal :
∀ (φ1 φ2 : Pattern) Γ i,
well_formed φ1 →
well_formed φ2 →
ProofInfoLe BasicReasoning i →
Γ ⊢i (φ1 <---> φ2) using i →
Γ ⊢i φ1 =ml φ2 using i .
Lemma patt_equal_refl :
∀ φ Γ,
well_formed φ →
Γ ⊢i φ =ml φ
using BasicReasoning.
#[global]
Instance patt_equal_is_reflexive : MLReflexive patt_equal.
End ProofSystemTheorems.
#[export]
Hint Resolve patt_equal_is_reflexive : core.
#[local]
Example reflexive_equal_test {Σ : Signature} {_ : Syntax} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p =ml p using i.
Section ProofSystemTheorems.
Context
{Σ : Signature}
{syntax : Syntax}
.
Lemma use_defined_axiom Γ:
theory ⊆ Γ →
Γ ⊢i patt_defined p_x
using BasicReasoning.
Definition BasicReasoningWithDefinedness := (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma defined_evar Γ x:
theory ⊆ Γ →
Γ ⊢i ⌈ patt_free_evar x ⌉
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_monotonic Γ φ₁ φ₂ i :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i ⌈ φ₁ ⌉ ---> ⌈ φ₂ ⌉ using i.
Lemma floor_monotonic Γ φ₁ φ₂ i :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i ⌊ φ₁ ⌋ ---> ⌊ φ₂ ⌋ using i.
Lemma patt_equal_sym Γ φ1 φ2:
theory ⊆ Γ →
well_formed φ1 → well_formed φ2 →
Γ ⊢i φ1 =ml φ2 ---> φ2 =ml φ1
using BasicReasoning.
Lemma patt_equal_comm φ φ' Γ:
theory ⊆ Γ →
well_formed φ →
well_formed φ' →
Γ ⊢i (φ =ml φ') <---> (φ' =ml φ) using BasicReasoning.
Lemma in_context_impl_defined Γ AC φ x:
theory ⊆ Γ →
x ∉ (free_evars φ ∪ AC_free_evars AC) →
well_formed φ →
Γ ⊢i (subst_ctx AC φ) ---> ⌈ φ ⌉
using (ExGen := {[ev_x]} ∪ {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma elements_union_empty φ:
elements (free_evars φ ∪ ∅) = elements (free_evars φ).
Lemma phi_impl_defined_phi Γ φ x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i φ ---> ⌈ φ ⌉
using
(ExGen := {[ev_x;x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma total_phi_impl_phi Γ φ x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ ---> φ
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma total_phi_impl_phi_meta Γ φ i x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ φ ⌋ using i →
Γ ⊢i φ using i.
Lemma framing_left_under_tot_impl Γ ψ phi1 phi2 psi x i:
well_formed ψ = true →
well_formed phi1 = true →
well_formed phi2 = true →
well_formed psi = true →
theory ⊆ Γ →
x ∉ free_evars ψ ∪ free_evars psi →
ProofInfoLe (ExGen := {[ev_x; x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ ψ ⌋ ---> phi1 ---> phi2 using i→
Γ ⊢i ⌊ ψ ⌋ ---> (phi1 ⋅ psi) ---> (phi2 ⋅ psi) using i.
Lemma framing_right_under_tot_impl Γ ψ phi1 phi2 psi x i:
well_formed ψ = true →
well_formed phi1 = true →
well_formed phi2 = true →
well_formed psi = true →
theory ⊆ Γ →
x ∉ free_evars ψ ∪ free_evars psi →
ProofInfoLe (ExGen := {[ev_x; x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ ψ ⌋ ---> phi1 ---> phi2 using i→
Γ ⊢i ⌊ ψ ⌋ ---> (psi ⋅ phi1) ---> (psi ⋅ phi2) using i.
Theorem deduction_theorem_noKT Γ φ ψ
(gpi : ProofInfo)
(pf : Γ ∪ {[ ψ ]} ⊢i φ using gpi) :
well_formed φ →
well_formed ψ →
theory ⊆ Γ →
(* x ∈ pi_generalized_evars gpi -> *)
pi_generalized_evars gpi ## (gset_to_coGset (free_evars ψ)) →
pi_substituted_svars gpi ## (gset_to_coGset (free_svars ψ)) →
pi_uses_kt gpi = false →
Γ ⊢i ⌊ ψ ⌋ ---> φ
using AnyReasoning.
Import MatchingLogic.Logic.Notations
MatchingLogic.Theories.Definedness_Syntax.Notations.
Open Scope list_scope.
Section ProofSystemTheorems.
Context
{Σ : Signature}
{syntax : Syntax}
.
Definition defFP : coWfpSet := {[(exist (λ p, well_formed p = true) (definedness) erefl)]}.
Lemma phi_impl_total_phi_meta Γ φ i:
well_formed φ →
ProofInfoLe BasicReasoning i →
Γ ⊢i φ using i →
Γ ⊢i ⌊ φ ⌋ using i.
Lemma patt_iff_implies_equal :
∀ (φ1 φ2 : Pattern) Γ i,
well_formed φ1 →
well_formed φ2 →
ProofInfoLe BasicReasoning i →
Γ ⊢i (φ1 <---> φ2) using i →
Γ ⊢i φ1 =ml φ2 using i .
Lemma patt_equal_refl :
∀ φ Γ,
well_formed φ →
Γ ⊢i φ =ml φ
using BasicReasoning.
#[global]
Instance patt_equal_is_reflexive : MLReflexive patt_equal.
End ProofSystemTheorems.
#[export]
Hint Resolve patt_equal_is_reflexive : core.
#[local]
Example reflexive_equal_test {Σ : Signature} {_ : Syntax} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p =ml p using i.
Section ProofSystemTheorems.
Context
{Σ : Signature}
{syntax : Syntax}
.
Lemma use_defined_axiom Γ:
theory ⊆ Γ →
Γ ⊢i patt_defined p_x
using BasicReasoning.
Definition BasicReasoningWithDefinedness := (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma defined_evar Γ x:
theory ⊆ Γ →
Γ ⊢i ⌈ patt_free_evar x ⌉
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_monotonic Γ φ₁ φ₂ i :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i ⌈ φ₁ ⌉ ---> ⌈ φ₂ ⌉ using i.
Lemma floor_monotonic Γ φ₁ φ₂ i :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ---> φ₂ using i →
Γ ⊢i ⌊ φ₁ ⌋ ---> ⌊ φ₂ ⌋ using i.
Lemma patt_equal_sym Γ φ1 φ2:
theory ⊆ Γ →
well_formed φ1 → well_formed φ2 →
Γ ⊢i φ1 =ml φ2 ---> φ2 =ml φ1
using BasicReasoning.
Lemma patt_equal_comm φ φ' Γ:
theory ⊆ Γ →
well_formed φ →
well_formed φ' →
Γ ⊢i (φ =ml φ') <---> (φ' =ml φ) using BasicReasoning.
Lemma in_context_impl_defined Γ AC φ x:
theory ⊆ Γ →
x ∉ (free_evars φ ∪ AC_free_evars AC) →
well_formed φ →
Γ ⊢i (subst_ctx AC φ) ---> ⌈ φ ⌉
using (ExGen := {[ev_x]} ∪ {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma elements_union_empty φ:
elements (free_evars φ ∪ ∅) = elements (free_evars φ).
Lemma phi_impl_defined_phi Γ φ x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i φ ---> ⌈ φ ⌉
using
(ExGen := {[ev_x;x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma total_phi_impl_phi Γ φ x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ ---> φ
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma total_phi_impl_phi_meta Γ φ i x:
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ φ ⌋ using i →
Γ ⊢i φ using i.
Lemma framing_left_under_tot_impl Γ ψ phi1 phi2 psi x i:
well_formed ψ = true →
well_formed phi1 = true →
well_formed phi2 = true →
well_formed psi = true →
theory ⊆ Γ →
x ∉ free_evars ψ ∪ free_evars psi →
ProofInfoLe (ExGen := {[ev_x; x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ ψ ⌋ ---> phi1 ---> phi2 using i→
Γ ⊢i ⌊ ψ ⌋ ---> (phi1 ⋅ psi) ---> (phi2 ⋅ psi) using i.
Lemma framing_right_under_tot_impl Γ ψ phi1 phi2 psi x i:
well_formed ψ = true →
well_formed phi1 = true →
well_formed phi2 = true →
well_formed psi = true →
theory ⊆ Γ →
x ∉ free_evars ψ ∪ free_evars psi →
ProofInfoLe (ExGen := {[ev_x; x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌊ ψ ⌋ ---> phi1 ---> phi2 using i→
Γ ⊢i ⌊ ψ ⌋ ---> (psi ⋅ phi1) ---> (psi ⋅ phi2) using i.
Theorem deduction_theorem_noKT Γ φ ψ
(gpi : ProofInfo)
(pf : Γ ∪ {[ ψ ]} ⊢i φ using gpi) :
well_formed φ →
well_formed ψ →
theory ⊆ Γ →
(* x ∈ pi_generalized_evars gpi -> *)
pi_generalized_evars gpi ## (gset_to_coGset (free_evars ψ)) →
pi_substituted_svars gpi ## (gset_to_coGset (free_svars ψ)) →
pi_uses_kt gpi = false →
Γ ⊢i ⌊ ψ ⌋ ---> φ
using AnyReasoning.
TODO: for this proof, the free variables in patterns of Framing need to be
traced!!!!
Lemma membership_introduction Γ φ i x:
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅,
KT := false,
AKT := false
) i →
well_formed φ →
x ∉ free_evars φ →
theory ⊆ Γ →
Γ ⊢i φ using i →
Γ ⊢i all, ((patt_bound_evar 0) ∈ml φ)
using i.
Lemma membership_implies_implication Γ ϕ x:
well_formed ϕ →
Γ ⊢i patt_free_evar x ∈ml ϕ ---> patt_free_evar x ---> ϕ using BasicReasoning.
Lemma membership_implies_implication_meta Γ ϕ x i:
well_formed ϕ →
Γ ⊢i patt_free_evar x ∈ml ϕ using i →
Γ ⊢i patt_free_evar x ---> ϕ using i.
Lemma membership_elimination Γ φ i x:
x ∉ free_evars φ →
ProofInfoLe
(ExGen := {[x]},
SVSubst := ∅,
KT := false,
AKT := false
) i →
well_formed φ →
theory ⊆ Γ →
Γ ⊢i all, ((patt_bound_evar 0) ∈ml φ) using i →
Γ ⊢i φ using i.
Lemma membership_not_1 Γ φ x:
well_formed φ →
theory ⊆ Γ →
Γ ⊢i ((patt_free_evar x) ∈ml (! φ)) ---> ! ((patt_free_evar x) ∈ml φ)
using BasicReasoning.
Lemma membership_not_2 Γ (φ : Pattern) x:
well_formed φ = true →
theory ⊆ Γ →
Γ ⊢i ((!(patt_free_evar x ∈ml φ)) ---> (patt_free_evar x ∈ml (! φ)))%ml
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_not_iff Γ φ x:
well_formed φ →
theory ⊆ Γ →
Γ ⊢i ((patt_free_evar x) ∈ml (! φ)) <---> ! ((patt_free_evar x) ∈ml φ)
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_or_1 Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ or φ₂)) ---> ((patt_free_evar x ∈ml φ₁) or (patt_free_evar x ∈ml φ₂))
using BasicReasoning.
Lemma membership_or_2 Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i ((patt_free_evar x ∈ml φ₁) or (patt_free_evar x ∈ml φ₂)) ---> (patt_free_evar x ∈ml (φ₁ or φ₂))
using BasicReasoning.
Lemma membership_or_iff Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ or φ₂)) <---> ((patt_free_evar x ∈ml φ₁) or (patt_free_evar x ∈ml φ₂))
using BasicReasoning.
Lemma membership_and_1 Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ and φ₂)) ---> ((patt_free_evar x ∈ml φ₁) and (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_and_2 Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i ((patt_free_evar x ∈ml φ₁) and (patt_free_evar x ∈ml φ₂)) ---> (patt_free_evar x ∈ml (φ₁ and φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_and_iff Γ x φ₁ φ₂:
well_formed φ₁ →
well_formed φ₂ →
theory ⊆ Γ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ and φ₂)) <---> ((patt_free_evar x ∈ml φ₁) and (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma mu_free_in_path φ:
mu_free φ = true → ∀ x, mu_in_evar_path x φ 0 = false.
Induction-based eq_elim proof
Lemma equality_elimination_basic_mfpath
Γ φ1 φ2 C x (xs : EVarSet) i
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C)
(Hfree : {[ev_x; x]} ∪ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C) ## xs)
(* TODO: use this: (Hfree : fresh_evars xs {ev_x; x} ∪ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C)) *)
(Hfree2 : x ∉ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C))
(Henough : size xs ≥ maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))
(Hmu_less : mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false):
ProofInfoLe (ExGen := {[ev_x; x]} ∪ coGset.gset_to_coGset xs,
SVSubst := ∅,
KT := false,
AKT := false) i →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) ---> (emplace C φ2)
using i.
Lemma equality_elimination_basic_mfpath_original Γ φ1 φ2 C
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C) :
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
Lemma equality_elimination_basic Γ φ1 φ2 C
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C) :
mu_free (pcPattern C) →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
Lemma equality_elimination_basic_ar Γ φ1 φ2 C:
theory ⊆ Γ →
well_formed φ1 →
well_formed φ2 →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
(* NOTE: could this also be solved withouth induction? *)
Lemma equality_elimination_basic_ar_iter_1 Γ φ₁ φ₂ l C :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Pattern.wf l →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i foldr patt_imp ((emplace C φ₁) <---> (emplace C φ₂)) ((φ₁ =ml φ₂) :: l)
using AnyReasoning.
(* TODO: this should NOT be done this way probably. There should be a general lemma, which can propagate another "foldr" lemma inside l₁, since there are other theorems that use the same scheme *)
Lemma equality_elimination_basic_ar_iter Γ φ₁ φ₂ l₁ l₂ C :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Pattern.wf l₁ →
Pattern.wf l₂ →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i foldr patt_imp ((emplace C φ₁) <---> (emplace C φ₂)) (l₁ ++ (φ₁ =ml φ₂)::l₂)
using AnyReasoning.
Corollary equality_elimination_proj Γ φ1 φ2 ψ:
theory ⊆ Γ →
mu_free ψ →
well_formed φ1 → well_formed φ2 → well_formed_closed_ex_aux ψ 1 → well_formed_closed_mu_aux ψ 0 →
Γ ⊢i (φ1 =ml φ2) --->
(ψ^[evar: 0 ↦ φ1]) ---> (ψ^[evar: 0 ↦ φ2])
using AnyReasoning.
Lemma evar_quantify_equal_simpl : ∀ φ1 φ2 x n,
evar_quantify x n (φ1 =ml φ2) = (evar_quantify x n φ1) =ml (evar_quantify x n φ2).
Definition is_functional φ : Pattern :=
(ex, φ =ml b0).
Lemma exists_functional_subst φ φ' Γ :
theory ⊆ Γ →
mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 → well_formed_closed_mu_aux φ 0 →
Γ ⊢i ((instantiate (patt_exists φ) φ') and is_functional φ') ---> (patt_exists φ)
using AnyReasoning.
Corollary forall_functional_subst φ φ' Γ :
theory ⊆ Γ →
mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 → well_formed_closed_mu_aux φ 0 →
Γ ⊢i ((patt_forall φ) and (patt_exists (patt_equal φ' (patt_bound_evar 0)))) ---> (φ^[evar: 0 ↦ φ'])
using AnyReasoning.
End ProofSystemTheorems.
Lemma MLGoal_rewriteBy {Σ : Signature} {syntax : Syntax}
(Γ : Theory) (l₁ l₂ : hypotheses) name (φ₁ φ₂ : Pattern) (C : PatternCtx) :
theory ⊆ Γ →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (φ₁ =ml φ₂)) :: l₂) (emplace C φ₂) AnyReasoning →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (φ₁ =ml φ₂)) :: l₂) (emplace C φ₁) AnyReasoning .
Ltac2 mlRewriteBy (name' : constr) (atn : int) :=
_mlReshapeHypsByName name';
lazy_match! goal with
| [ |- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?g (?l₁ ++ (mkNH _ _ (?a' =ml ?a))::?l₂) ?p AnyReasoning)]
⇒
let hr : HeatResult := heat atn a' p in
let heq := Control.hyp (hr.(equality)) in
let pc := (hr.(pc)) in
eapply (@cast_proof_ml_goal _ $g) >
[ rewrite $heq; reflexivity | ()];
Std.clear [hr.(equality)];
Control.plus(fun () ⇒
apply MLGoal_rewriteBy
> [ try (match! goal with
| [hyp : ?theory ⊆ _ |- _] ⇒ unfold theory
end); try ltac1:(
(* idtac "Trying set solving"; *)
timeout 5 set_solver)
| Control.plus
(fun () ⇒ ltac1:(now (apply mu_free_in_path; simpl; assumption)))
(fun exn ⇒ let star := hr.(star_ident) in
ltac1:(star |-
unfold mu_in_evar_path; simpl; repeat case_match;
try reflexivity; try congruence;
repeat match goal with
| [H : context G [maximal_mu_depth_to _ _ _] |- _ ] ⇒
(* idtac "rewriting"; *)
rewrite → maximal_mu_depth_to_0 in H by (try timeout 5 (subst star; try solve_fresh))(* This is potentially non-terminating, hence the timeout *)
end;
simpl in *; try lia
) (Ltac1.of_ident star))
(* TODO: improve these heuristics above *)
| lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?sgm ?g ?l ?p AnyReasoning)]
⇒
let heq2 := Fresh.in_goal ident:(heq2) in
let plugged := Pattern.instantiate (hr.(ctx)) a in
assert(heq2: ($p = $plugged))
> [
abstract (ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident (hr.(star_ident)));
reflexivity
)
| ()
];
let heq2_pf := Control.hyp heq2 in
eapply (@cast_proof_ml_goal _ $g)
with (goal := $plugged) >
[ ltac1:(heq2 |- rewrite [left in _ = left] heq2; reflexivity) (Ltac1.of_ident heq2) | ()];
Std.clear [heq2 ; (hr.(star_ident)); (hr.(star_eq))];
_mlReshapeHypsBack
end
]
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewriteBy: failed when rewriting '")
(Message.concat (Message.of_constr (a))
(Message.concat (Message.of_string "' to/from '")
(Message.concat (Message.of_constr (a'))
(Message.concat (Message.of_string "' in context ")
(Message.of_constr (pc))
)
)
)
)
)
)
| [|- _] ⇒ throw_pm_exn_with_goal "mlRewrite: not in proof mode"
end
.
Tactic Notation "mlRewriteBy" constr(name') "at" constr(atn) :=
(let ff := ltac2:(name'' atn |-
mlRewriteBy
(Option.get (Ltac1.to_constr(name'')))
(constr_to_int (Option.get (Ltac1.to_constr(atn))))
) in
ff name' atn).
Local Example ex_rewriteBy {Σ : Signature} {syntax : Syntax} Γ a a' b:
theory ⊆ Γ →
well_formed a →
well_formed a' →
well_formed b →
mu_free b →
Γ ⊢i a ⋅ b ---> (a' =ml a) ---> a' ⋅ b
using AnyReasoning.
Lemma patt_equal_implies_iff
{Σ : Signature} {syntax : Syntax} (φ1 φ2 : Pattern) (Γ : Theory) (i : ProofInfo) x :
theory ⊆ Γ →
x ∉ (free_evars φ1 ∪ free_evars φ2) →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
well_formed φ1 →
well_formed φ2 →
Γ ⊢i φ1 =ml φ2 using i →
Γ ⊢i (φ1 <---> φ2) using i.
Lemma patt_subseteq_refl {Σ : Signature} {syntax : Syntax} Γ φ:
well_formed φ →
Γ ⊢i φ ⊆ml φ using BasicReasoning.
#[global]
Instance patt_subseteq_is_reflexive {Σ : Signature} {syntax : Syntax} : MLReflexive patt_subseteq.
#[export]
Hint Resolve patt_subseteq_is_reflexive : core.
#[local]
Example reflexive_subseteq_test {Σ : Signature} {_ : Syntax} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p ⊆ml p using i.
Lemma disj_equals_greater_1_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂ i x:
theory ⊆ Γ →
x ∉ free_evars φ₁ ∪ free_evars φ₂ →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ⊆ml φ₂ using i →
Γ ⊢i (φ₁ or φ₂) =ml φ₂ using i.
Lemma def_not_phi_impl_not_total_phi {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed φ →
Γ ⊢i ⌈ ! φ ⌉ ---> ! ⌊ φ ⌋ using BasicReasoning.
Lemma def_def_phi_impl_def_phi
{Σ : Signature} {syntax : Syntax} {Γ : Theory} (φ : Pattern) x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌈ ⌈ φ ⌉ ⌉ ---> ⌈ φ ⌉
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma bott_not_defined {Σ : Signature} {syntax : Syntax} Γ :
Γ ⊢i ! ⌈ ⊥ ⌉ using BasicReasoning.
Lemma not_def_phi_impl_not_phi {Σ : Signature} {syntax : Syntax} Γ φ x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ! ⌈ φ ⌉ ---> ! φ
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma tot_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ ---> ⌊ ⌈ φ ⌉ ⌋
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma def_of_pred_impl_pred {Σ : Signature} {syntax : Syntax} Γ ψ :
theory ⊆ Γ →
well_formed ψ →
Γ ⊢i (ψ =ml patt_bott) or (ψ =ml patt_top) using AnyReasoning →
Γ ⊢i ⌈ ψ ⌉ ---> ψ using AnyReasoning.
(* TODO need this non-meta *)
Lemma subseteq_antisym_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ ⊆ml φ₂) and (φ₂ ⊆ml φ₁) using AnyReasoning →
Γ ⊢i φ₁ =ml φ₂ using AnyReasoning.
Lemma propagate_membership_conjunct_1 {Σ : Signature} {syntax : Syntax}
Γ AC x φ₁ φ₂ :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (subst_ctx AC (φ₁ and ((patt_free_evar x) ∈ml φ₂))) ---> ((patt_free_evar x) ∈ml φ₂)
using AnyReasoning.
Lemma double_not_ceil_alt {Σ : Signature} {syntax : Syntax} Γ φ i :
theory ⊆ Γ →
well_formed φ →
Γ ⊢i ( ⌈ ! ⌈ φ ⌉ ⌉ ---> (! ⌈ φ ⌉)) using i →
Γ ⊢i ( ⌈ φ ⌉ ---> ! ( ⌈ ! ⌈ φ ⌉ ⌉)) using i.
Lemma membership_imp {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ ---> φ₂)) <---> ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_imp_1 {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ ---> φ₂)) ---> ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_imp_2 {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂)) ---> (patt_free_evar x ∈ml (φ₁ ---> φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_propagation_exists_1 {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed (ex, φ) →
Γ ⊢i (⌈ ex, φ ⌉) ---> (ex, ⌈ φ ⌉)
using BasicReasoning.
Lemma ceil_propagation_exists_2 {Σ : Signature} {syntax : Syntax} Γ φ x:
theory ⊆ Γ →
well_formed (ex, φ) →
x ∉ free_evars φ →
Γ ⊢i (ex, ⌈ φ ⌉) ---> (⌈ ex, φ ⌉)
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_propagation_exists_iff {Σ : Signature} {syntax : Syntax} Γ φ x:
theory ⊆ Γ →
well_formed (ex, φ) →
x ∉ free_evars φ →
Γ ⊢i (⌈ ex, φ ⌉) <---> (ex, ⌈ φ ⌉)
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_exists {Σ : Signature} {syntax : Syntax} Γ ψ y φ i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ψ ∈ml (ex, φ)) <---> (ex, ψ ∈ml φ)
using i.
Lemma membership_exists_1 {Σ : Signature} {syntax : Syntax} Γ ψ φ y i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ψ ∈ml (ex, φ)) ---> (ex, ψ ∈ml φ)
using i.
Lemma membership_exists_2 {Σ : Signature} {syntax : Syntax} Γ ψ φ y i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ex, ψ ∈ml φ) ---> (ψ ∈ml (ex, φ))
using i.
Lemma membership_forall_1 {Σ : Signature} {syntax : Definedness_Syntax.Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed (ex , φ) →
y ∉ free_evars φ ∪ {[x]}->
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i patt_free_evar x ∈ml (all , φ) ---> (all , patt_free_evar x ∈ml φ) using i.
Lemma membership_forall_2 {Σ : Signature} {syntax : Definedness_Syntax.Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed (ex , φ) →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (all , patt_free_evar x ∈ml φ) ---> patt_free_evar x ∈ml (all , φ) using i.
Lemma membership_symbol_ceil_aux_aux_0 {Σ : Signature} {syntax : Syntax} Γ x φ i:
theory ⊆ Γ →
well_formed φ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ((⌈ patt_free_evar x and φ ⌉) ---> (⌊ ⌈ patt_free_evar x and φ ⌉ ⌋))
using i.
Lemma patt_defined_or_1 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ or φ₂ ⌉) ---> (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉))
using BasicReasoning.
Lemma patt_defined_or_2 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉) ---> (⌈ φ₁ or φ₂ ⌉))
using BasicReasoning.
Lemma patt_defined_or {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ or φ₂ ⌉) <---> (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉))
using BasicReasoning.
Lemma helper_propositional_lemma_1 (Σ : Signature) Γ φ₁ φ₂:
well_formed φ₁ = true →
well_formed φ₂ = true →
Γ ⊢i (! φ₁ or φ₂) ---> (! φ₁ or (φ₂ and φ₁)) using BasicReasoning.
Lemma membership_symbol_ceil_aux_0 {Σ : Signature} {syntax : Syntax} Γ x y φ i:
theory ⊆ Γ →
well_formed φ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (⌈ patt_free_evar x and φ ⌉) ---> ⌈ patt_free_evar y and ⌈ patt_free_evar x and φ ⌉ ⌉
using i.
Lemma membership_symbol_ceil_left_aux_0 {Σ : Signature} {syntax : Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i φ ---> (ex, ⌈ b0 and φ ⌉)
using i.
Lemma ceil_and_x_ceil_phi_impl_ceil_phi {Σ : Signature} {syntax : Syntax} Γ (φ : Pattern) ψ y i:
theory ⊆ Γ →
well_formed φ →
well_formed ψ →
y ∉ free_evars φ →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ( (⌈ ψ and ⌈ φ ⌉ ⌉) ---> (⌈ φ ⌉))
using i.
Lemma membership_monotone {Σ : Signature} {syntax : Syntax} Γ (φ₁ φ₂ : Pattern) ψ i:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
well_formed ψ →
Γ ⊢i (φ₁ ---> φ₂) using i →
Γ ⊢i (ψ ∈ml φ₁) ---> (ψ ∈ml φ₂) using i.
Lemma defined_not_iff_not_total {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ : Pattern) i,
theory ⊆ Γ → well_formed φ → Γ ⊢i ⌈ ! φ ⌉ <---> ! ⌊ φ ⌋
using i.
Lemma patt_or_total {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ i,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ ⌋ or ⌊ ψ ⌋ ---> ⌊ φ or ψ ⌋
using i.
Lemma patt_defined_and {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ i,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌈ φ and ψ ⌉ ---> ⌈ φ ⌉ and ⌈ ψ ⌉
using i.
Lemma membership_symbol_ceil_left {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (patt_free_evar x ∈ml ⌈ φ ⌉) ---> (ex, (patt_bound_evar 0 ∈ml φ))
using i.
Lemma membership_symbol_ceil_right_aux_0 {Σ : Signature} {syntax : Syntax} Γ φ i x:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ex, (⌈ b0 and φ ⌉ and b0)) ---> φ
using i.
Ltac2 formula_of_proof (t : constr) :=
lazy_match! t with
| (@derives_using _ _ ?p _) ⇒ p
| _ ⇒ Message.print (Message.concat (Message.of_string "Cannot obtain a formula from") (Message.of_constr t));
Control.throw_invalid_argument "Cannot obtain a matching logic formula from given term"
end
.
Lemma membership_symbol_ceil_right {Σ : Signature} {syntax : Syntax} Γ φ x i y:
theory ⊆ Γ →
well_formed φ →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ((ex, (BoundVarSugar.b0 ∈ml φ)) ---> (patt_free_evar x ∈ml ⌈ φ ⌉))
using i.
Lemma def_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ i x y z:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ φ ⌉ ---> ⌊ ⌈ φ ⌉ ⌋
using i.
Lemma def_tot_phi_impl_tot_phi {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ ⌊ φ ⌋ ⌉ ---> ⌊ φ ⌋ using i.
Lemma floor_is_predicate {Σ : Signature} {syntax : Syntax} Γ φ i x y z:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i is_predicate_pattern (⌊ φ ⌋)
using i.
Lemma def_propagate_not {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed φ →
Γ ⊢i (! ⌈ φ ⌉) <---> (⌊ ! φ ⌋)
using BasicReasoning.
Lemma def_def_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ ⌈ φ ⌉ ⌉ ---> ⌊ ⌈ φ ⌉ ⌋
using i.
Lemma ceil_is_predicate {Σ : Signature} {syntax : Syntax} Γ φ :
theory ⊆ Γ →
well_formed φ →
Γ ⊢i is_predicate_pattern (⌈ φ ⌉)
using AnyReasoning.
Lemma predicate_elim
{Σ : Signature} {syntax : Syntax} Γ (C : PatternCtx) (ψ : Pattern):
theory ⊆ Γ →
well_formed (pcPattern C) →
well_formed ψ →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ emplace C patt_bott →
Γ ⊢ emplace C patt_top →
Γ ⊢ emplace C ψ
.
Lemma predicate_propagate_right_2 {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ ---> ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma predicate_propagate_right_2_meta {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma predicate_propagate_left_2 {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ ---> ψ and P ⋅ ϕ <---> (ψ and P) ⋅ ϕ.
Lemma predicate_propagate_left_2_meta {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> (ψ and P) ⋅ ϕ.
Corollary app_prop_under_implication
{Σ : Signature} {syntax : Syntax} Γ: ∀ φ1 φ2 φ3 ψ,
theory ⊆ Γ →
well_formed φ1 →
well_formed φ2 →
well_formed φ3 →
well_formed ψ →
Γ ⊢ is_predicate_pattern φ3 →
Γ ⊢ (φ1 ---> (ψ ⋅ φ2)) ---> (φ1 and φ3) ---> (ψ ⋅ (φ2 and φ3)).
(* TODO: Put in a different file? *)
Lemma predicate_propagate_right {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
mu_free ϕ →
mu_free ψ →
mu_free P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma equal_imp_membership {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ →
well_formed φ → well_formed φ' →
Γ ⊢ ⌈ φ' ⌉ →
Γ ⊢ (φ =ml φ') ---> (φ ∈ml φ').
Lemma phi_impl_ex_in_phi {Σ : Signature} {syntax : Syntax} Γ ϕ:
theory ⊆ Γ →
well_formed ϕ →
Γ ⊢ ϕ ---> (ex , b0 ∈ml ϕ and b0).
Lemma membership_symbol_right {Σ : Signature} {syntax : Syntax} Γ ϕ ψ x :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
mu_free ϕ →
mu_free ψ →
Γ ⊢ (patt_free_evar x ∈ml ψ ⋅ ϕ) ---> (ex , (b0 ∈ml ϕ and patt_free_evar x ∈ml ψ ⋅ b0)).
Lemma disj_equals_greater_1 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ ⊆ml φ₂) ---> ((φ₁ or φ₂) =ml φ₂)
using AnyReasoning.
Lemma disj_equals_greater_2_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ or φ₂) =ml φ₂ using AnyReasoning →
Γ ⊢i φ₁ ⊆ml φ₂ using AnyReasoning.
Lemma disj_equals_greater_2 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ → (* TODO get rid of it *)
Γ ⊢i ((φ₁ or φ₂) =ml φ₂) ---> (φ₁ ⊆ml φ₂)
using AnyReasoning.
Lemma bott_not_total {Σ : Signature} {syntax : Syntax}:
∀ Γ, theory ⊆ Γ →
Γ ⊢i ! ⌊ ⊥ ⌋
using AnyReasoning.
Lemma patt_total_and_1 {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ and ψ ⌋ ---> ⌊ φ ⌋ and ⌊ ψ ⌋
using BasicReasoning.
Lemma patt_total_and_2 {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ ⌋ and ⌊ ψ ⌋ ---> ⌊ φ and ψ ⌋
using BasicReasoning.
Lemma patt_total_and {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ and ψ ⌋ <---> ⌊ φ ⌋ and ⌊ ψ ⌋
using BasicReasoning.
Lemma membership_var {Σ : Signature} {syntax : Syntax} :
∀ x y Γ,
theory ⊆ Γ →
Γ ⊢ patt_free_evar y ∈ml patt_free_evar x ---> patt_free_evar y =ml patt_free_evar x.
Lemma mlSpecializeMeta {Σ : Signature} {syntax : Syntax} :
∀ Γ φ ψ, theory ⊆ Γ→
well_formed (ex , φ) → well_formed ψ → mu_free φ →
Γ ⊢i (all , φ) using AnyReasoning →
Γ ⊢i ex , ψ =ml b0 using AnyReasoning →
Γ ⊢i φ^[evar: 0 ↦ ψ] using AnyReasoning.
(* TODO: make sure that the final assumption does not solve goals we do not want to solve. *)
Tactic Notation "mlSpecMeta" ident(hyp) "with" constr(t) :=
unshelve (eapply (@mlSpecializeMeta _ _ _ _ t) in hyp); try_wfauto2; try assumption.
Local Lemma test_spec {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ, theory ⊆ Γ→
well_formed (ex , φ) → well_formed ψ → mu_free φ →
Γ ⊢i (all , φ) using AnyReasoning →
Γ ⊢i ex , ψ =ml b0 using AnyReasoning →
Γ ⊢i φ^[evar: 0 ↦ ψ] using AnyReasoning.
Lemma MLGoal_mlSpecialize {Σ : Signature} {syntax : Syntax} Γ l₁ l₂ p t g name:
theory ⊆ Γ →
mu_free p → well_formed t →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name p^[evar: 0 ↦ t]) ::l₂ ) g AnyReasoning →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((all, p) and (ex , t =ml b0)))::l₂) g AnyReasoning.
Γ φ1 φ2 C x (xs : EVarSet) i
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C)
(Hfree : {[ev_x; x]} ∪ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C) ## xs)
(* TODO: use this: (Hfree : fresh_evars xs {ev_x; x} ∪ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C)) *)
(Hfree2 : x ∉ free_evars φ1 ∪ free_evars φ2 ∪ free_evars (pcPattern C))
(Henough : size xs ≥ maximal_exists_depth_to 0 (pcEvar C) (pcPattern C))
(Hmu_less : mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false):
ProofInfoLe (ExGen := {[ev_x; x]} ∪ coGset.gset_to_coGset xs,
SVSubst := ∅,
KT := false,
AKT := false) i →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) ---> (emplace C φ2)
using i.
Lemma equality_elimination_basic_mfpath_original Γ φ1 φ2 C
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C) :
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
Lemma equality_elimination_basic Γ φ1 φ2 C
(HΓ : theory ⊆ Γ)
(WF1 : well_formed φ1)
(WF2 : well_formed φ2)
(WFC : PC_wf C) :
mu_free (pcPattern C) →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
Lemma equality_elimination_basic_ar Γ φ1 φ2 C:
theory ⊆ Γ →
well_formed φ1 →
well_formed φ2 →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i (φ1 =ml φ2) --->
(emplace C φ1) <---> (emplace C φ2)
using AnyReasoning.
(* NOTE: could this also be solved withouth induction? *)
Lemma equality_elimination_basic_ar_iter_1 Γ φ₁ φ₂ l C :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Pattern.wf l →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i foldr patt_imp ((emplace C φ₁) <---> (emplace C φ₂)) ((φ₁ =ml φ₂) :: l)
using AnyReasoning.
(* TODO: this should NOT be done this way probably. There should be a general lemma, which can propagate another "foldr" lemma inside l₁, since there are other theorems that use the same scheme *)
Lemma equality_elimination_basic_ar_iter Γ φ₁ φ₂ l₁ l₂ C :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Pattern.wf l₁ →
Pattern.wf l₂ →
PC_wf C →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢i foldr patt_imp ((emplace C φ₁) <---> (emplace C φ₂)) (l₁ ++ (φ₁ =ml φ₂)::l₂)
using AnyReasoning.
Corollary equality_elimination_proj Γ φ1 φ2 ψ:
theory ⊆ Γ →
mu_free ψ →
well_formed φ1 → well_formed φ2 → well_formed_closed_ex_aux ψ 1 → well_formed_closed_mu_aux ψ 0 →
Γ ⊢i (φ1 =ml φ2) --->
(ψ^[evar: 0 ↦ φ1]) ---> (ψ^[evar: 0 ↦ φ2])
using AnyReasoning.
Lemma evar_quantify_equal_simpl : ∀ φ1 φ2 x n,
evar_quantify x n (φ1 =ml φ2) = (evar_quantify x n φ1) =ml (evar_quantify x n φ2).
Definition is_functional φ : Pattern :=
(ex, φ =ml b0).
Lemma exists_functional_subst φ φ' Γ :
theory ⊆ Γ →
mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 → well_formed_closed_mu_aux φ 0 →
Γ ⊢i ((instantiate (patt_exists φ) φ') and is_functional φ') ---> (patt_exists φ)
using AnyReasoning.
Corollary forall_functional_subst φ φ' Γ :
theory ⊆ Γ →
mu_free φ → well_formed φ' → well_formed_closed_ex_aux φ 1 → well_formed_closed_mu_aux φ 0 →
Γ ⊢i ((patt_forall φ) and (patt_exists (patt_equal φ' (patt_bound_evar 0)))) ---> (φ^[evar: 0 ↦ φ'])
using AnyReasoning.
End ProofSystemTheorems.
Lemma MLGoal_rewriteBy {Σ : Signature} {syntax : Syntax}
(Γ : Theory) (l₁ l₂ : hypotheses) name (φ₁ φ₂ : Pattern) (C : PatternCtx) :
theory ⊆ Γ →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (φ₁ =ml φ₂)) :: l₂) (emplace C φ₂) AnyReasoning →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name (φ₁ =ml φ₂)) :: l₂) (emplace C φ₁) AnyReasoning .
Ltac2 mlRewriteBy (name' : constr) (atn : int) :=
_mlReshapeHypsByName name';
lazy_match! goal with
| [ |- @of_MLGoal ?sgm (@mkMLGoal ?sgm ?g (?l₁ ++ (mkNH _ _ (?a' =ml ?a))::?l₂) ?p AnyReasoning)]
⇒
let hr : HeatResult := heat atn a' p in
let heq := Control.hyp (hr.(equality)) in
let pc := (hr.(pc)) in
eapply (@cast_proof_ml_goal _ $g) >
[ rewrite $heq; reflexivity | ()];
Std.clear [hr.(equality)];
Control.plus(fun () ⇒
apply MLGoal_rewriteBy
> [ try (match! goal with
| [hyp : ?theory ⊆ _ |- _] ⇒ unfold theory
end); try ltac1:(
(* idtac "Trying set solving"; *)
timeout 5 set_solver)
| Control.plus
(fun () ⇒ ltac1:(now (apply mu_free_in_path; simpl; assumption)))
(fun exn ⇒ let star := hr.(star_ident) in
ltac1:(star |-
unfold mu_in_evar_path; simpl; repeat case_match;
try reflexivity; try congruence;
repeat match goal with
| [H : context G [maximal_mu_depth_to _ _ _] |- _ ] ⇒
(* idtac "rewriting"; *)
rewrite → maximal_mu_depth_to_0 in H by (try timeout 5 (subst star; try solve_fresh))(* This is potentially non-terminating, hence the timeout *)
end;
simpl in *; try lia
) (Ltac1.of_ident star))
(* TODO: improve these heuristics above *)
| lazy_match! goal with
| [ |- of_MLGoal (@mkMLGoal ?sgm ?g ?l ?p AnyReasoning)]
⇒
let heq2 := Fresh.in_goal ident:(heq2) in
let plugged := Pattern.instantiate (hr.(ctx)) a in
assert(heq2: ($p = $plugged))
> [
abstract (ltac1:(star |- simplify_emplace_2 star) (Ltac1.of_ident (hr.(star_ident)));
reflexivity
)
| ()
];
let heq2_pf := Control.hyp heq2 in
eapply (@cast_proof_ml_goal _ $g)
with (goal := $plugged) >
[ ltac1:(heq2 |- rewrite [left in _ = left] heq2; reflexivity) (Ltac1.of_ident heq2) | ()];
Std.clear [heq2 ; (hr.(star_ident)); (hr.(star_eq))];
_mlReshapeHypsBack
end
]
)
(fun _ ⇒ throw_pm_exn (Message.concat (Message.of_string "mlRewriteBy: failed when rewriting '")
(Message.concat (Message.of_constr (a))
(Message.concat (Message.of_string "' to/from '")
(Message.concat (Message.of_constr (a'))
(Message.concat (Message.of_string "' in context ")
(Message.of_constr (pc))
)
)
)
)
)
)
| [|- _] ⇒ throw_pm_exn_with_goal "mlRewrite: not in proof mode"
end
.
Tactic Notation "mlRewriteBy" constr(name') "at" constr(atn) :=
(let ff := ltac2:(name'' atn |-
mlRewriteBy
(Option.get (Ltac1.to_constr(name'')))
(constr_to_int (Option.get (Ltac1.to_constr(atn))))
) in
ff name' atn).
Local Example ex_rewriteBy {Σ : Signature} {syntax : Syntax} Γ a a' b:
theory ⊆ Γ →
well_formed a →
well_formed a' →
well_formed b →
mu_free b →
Γ ⊢i a ⋅ b ---> (a' =ml a) ---> a' ⋅ b
using AnyReasoning.
Lemma patt_equal_implies_iff
{Σ : Signature} {syntax : Syntax} (φ1 φ2 : Pattern) (Γ : Theory) (i : ProofInfo) x :
theory ⊆ Γ →
x ∉ (free_evars φ1 ∪ free_evars φ2) →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
well_formed φ1 →
well_formed φ2 →
Γ ⊢i φ1 =ml φ2 using i →
Γ ⊢i (φ1 <---> φ2) using i.
Lemma patt_subseteq_refl {Σ : Signature} {syntax : Syntax} Γ φ:
well_formed φ →
Γ ⊢i φ ⊆ml φ using BasicReasoning.
#[global]
Instance patt_subseteq_is_reflexive {Σ : Signature} {syntax : Syntax} : MLReflexive patt_subseteq.
#[export]
Hint Resolve patt_subseteq_is_reflexive : core.
#[local]
Example reflexive_subseteq_test {Σ : Signature} {_ : Syntax} Γ p q p' q' i:
well_formed p →
well_formed q →
well_formed p' →
well_formed q' →
Γ ⊢i q ---> q' ---> p' ---> p ⊆ml p using i.
Lemma disj_equals_greater_1_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂ i x:
theory ⊆ Γ →
x ∉ free_evars φ₁ ∪ free_evars φ₂ →
ProofInfoLe
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false) i →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i φ₁ ⊆ml φ₂ using i →
Γ ⊢i (φ₁ or φ₂) =ml φ₂ using i.
Lemma def_not_phi_impl_not_total_phi {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed φ →
Γ ⊢i ⌈ ! φ ⌉ ---> ! ⌊ φ ⌋ using BasicReasoning.
Lemma def_def_phi_impl_def_phi
{Σ : Signature} {syntax : Syntax} {Γ : Theory} (φ : Pattern) x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌈ ⌈ φ ⌉ ⌉ ---> ⌈ φ ⌉
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma bott_not_defined {Σ : Signature} {syntax : Syntax} Γ :
Γ ⊢i ! ⌈ ⊥ ⌉ using BasicReasoning.
Lemma not_def_phi_impl_not_phi {Σ : Signature} {syntax : Syntax} Γ φ x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ! ⌈ φ ⌉ ---> ! φ
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma tot_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ x :
theory ⊆ Γ →
x ∉ free_evars φ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ ---> ⌊ ⌈ φ ⌉ ⌋
using
(ExGen := {[ev_x; x]},
SVSubst := ∅, KT := false, AKT := false).
Lemma def_of_pred_impl_pred {Σ : Signature} {syntax : Syntax} Γ ψ :
theory ⊆ Γ →
well_formed ψ →
Γ ⊢i (ψ =ml patt_bott) or (ψ =ml patt_top) using AnyReasoning →
Γ ⊢i ⌈ ψ ⌉ ---> ψ using AnyReasoning.
(* TODO need this non-meta *)
Lemma subseteq_antisym_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ ⊆ml φ₂) and (φ₂ ⊆ml φ₁) using AnyReasoning →
Γ ⊢i φ₁ =ml φ₂ using AnyReasoning.
Lemma propagate_membership_conjunct_1 {Σ : Signature} {syntax : Syntax}
Γ AC x φ₁ φ₂ :
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (subst_ctx AC (φ₁ and ((patt_free_evar x) ∈ml φ₂))) ---> ((patt_free_evar x) ∈ml φ₂)
using AnyReasoning.
Lemma double_not_ceil_alt {Σ : Signature} {syntax : Syntax} Γ φ i :
theory ⊆ Γ →
well_formed φ →
Γ ⊢i ( ⌈ ! ⌈ φ ⌉ ⌉ ---> (! ⌈ φ ⌉)) using i →
Γ ⊢i ( ⌈ φ ⌉ ---> ! ( ⌈ ! ⌈ φ ⌉ ⌉)) using i.
Lemma membership_imp {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ ---> φ₂)) <---> ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_imp_1 {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (patt_free_evar x ∈ml (φ₁ ---> φ₂)) ---> ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_imp_2 {Σ : Signature} {syntax : Syntax} Γ x φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ((patt_free_evar x ∈ml φ₁) ---> (patt_free_evar x ∈ml φ₂)) ---> (patt_free_evar x ∈ml (φ₁ ---> φ₂))
using (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_propagation_exists_1 {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed (ex, φ) →
Γ ⊢i (⌈ ex, φ ⌉) ---> (ex, ⌈ φ ⌉)
using BasicReasoning.
Lemma ceil_propagation_exists_2 {Σ : Signature} {syntax : Syntax} Γ φ x:
theory ⊆ Γ →
well_formed (ex, φ) →
x ∉ free_evars φ →
Γ ⊢i (ex, ⌈ φ ⌉) ---> (⌈ ex, φ ⌉)
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma ceil_propagation_exists_iff {Σ : Signature} {syntax : Syntax} Γ φ x:
theory ⊆ Γ →
well_formed (ex, φ) →
x ∉ free_evars φ →
Γ ⊢i (⌈ ex, φ ⌉) <---> (ex, ⌈ φ ⌉)
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma membership_exists {Σ : Signature} {syntax : Syntax} Γ ψ y φ i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ψ ∈ml (ex, φ)) <---> (ex, ψ ∈ml φ)
using i.
Lemma membership_exists_1 {Σ : Signature} {syntax : Syntax} Γ ψ φ y i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ψ ∈ml (ex, φ)) ---> (ex, ψ ∈ml φ)
using i.
Lemma membership_exists_2 {Σ : Signature} {syntax : Syntax} Γ ψ φ y i:
theory ⊆ Γ →
well_formed (ex, φ) →
well_formed ψ →
y ∉ free_evars φ ∪ free_evars ψ →
ProofInfoLe (ExGen := {[y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ex, ψ ∈ml φ) ---> (ψ ∈ml (ex, φ))
using i.
Lemma membership_forall_1 {Σ : Signature} {syntax : Definedness_Syntax.Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed (ex , φ) →
y ∉ free_evars φ ∪ {[x]}->
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i patt_free_evar x ∈ml (all , φ) ---> (all , patt_free_evar x ∈ml φ) using i.
Lemma membership_forall_2 {Σ : Signature} {syntax : Definedness_Syntax.Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed (ex , φ) →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (all , patt_free_evar x ∈ml φ) ---> patt_free_evar x ∈ml (all , φ) using i.
Lemma membership_symbol_ceil_aux_aux_0 {Σ : Signature} {syntax : Syntax} Γ x φ i:
theory ⊆ Γ →
well_formed φ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ((⌈ patt_free_evar x and φ ⌉) ---> (⌊ ⌈ patt_free_evar x and φ ⌉ ⌋))
using i.
Lemma patt_defined_or_1 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ or φ₂ ⌉) ---> (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉))
using BasicReasoning.
Lemma patt_defined_or_2 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉) ---> (⌈ φ₁ or φ₂ ⌉))
using BasicReasoning.
Lemma patt_defined_or {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( (⌈ φ₁ or φ₂ ⌉) <---> (⌈ φ₁ ⌉ or ⌈ φ₂ ⌉))
using BasicReasoning.
Lemma helper_propositional_lemma_1 (Σ : Signature) Γ φ₁ φ₂:
well_formed φ₁ = true →
well_formed φ₂ = true →
Γ ⊢i (! φ₁ or φ₂) ---> (! φ₁ or (φ₂ and φ₁)) using BasicReasoning.
Lemma membership_symbol_ceil_aux_0 {Σ : Signature} {syntax : Syntax} Γ x y φ i:
theory ⊆ Γ →
well_formed φ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (⌈ patt_free_evar x and φ ⌉) ---> ⌈ patt_free_evar y and ⌈ patt_free_evar x and φ ⌉ ⌉
using i.
Lemma membership_symbol_ceil_left_aux_0 {Σ : Signature} {syntax : Syntax} Γ φ x y i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i φ ---> (ex, ⌈ b0 and φ ⌉)
using i.
Lemma ceil_and_x_ceil_phi_impl_ceil_phi {Σ : Signature} {syntax : Syntax} Γ (φ : Pattern) ψ y i:
theory ⊆ Γ →
well_formed φ →
well_formed ψ →
y ∉ free_evars φ →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ( (⌈ ψ and ⌈ φ ⌉ ⌉) ---> (⌈ φ ⌉))
using i.
Lemma membership_monotone {Σ : Signature} {syntax : Syntax} Γ (φ₁ φ₂ : Pattern) ψ i:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
well_formed ψ →
Γ ⊢i (φ₁ ---> φ₂) using i →
Γ ⊢i (ψ ∈ml φ₁) ---> (ψ ∈ml φ₂) using i.
Lemma defined_not_iff_not_total {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ : Pattern) i,
theory ⊆ Γ → well_formed φ → Γ ⊢i ⌈ ! φ ⌉ <---> ! ⌊ φ ⌋
using i.
Lemma patt_or_total {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ i,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ ⌋ or ⌊ ψ ⌋ ---> ⌊ φ or ψ ⌋
using i.
Lemma patt_defined_and {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ i,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌈ φ and ψ ⌉ ---> ⌈ φ ⌉ and ⌈ ψ ⌉
using i.
Lemma membership_symbol_ceil_left {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (patt_free_evar x ∈ml ⌈ φ ⌉) ---> (ex, (patt_bound_evar 0 ∈ml φ))
using i.
Lemma membership_symbol_ceil_right_aux_0 {Σ : Signature} {syntax : Syntax} Γ φ i x:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i (ex, (⌈ b0 and φ ⌉ and b0)) ---> φ
using i.
Ltac2 formula_of_proof (t : constr) :=
lazy_match! t with
| (@derives_using _ _ ?p _) ⇒ p
| _ ⇒ Message.print (Message.concat (Message.of_string "Cannot obtain a formula from") (Message.of_constr t));
Control.throw_invalid_argument "Cannot obtain a matching logic formula from given term"
end
.
Lemma membership_symbol_ceil_right {Σ : Signature} {syntax : Syntax} Γ φ x i y:
theory ⊆ Γ →
well_formed φ →
y ∉ free_evars φ ∪ {[x]} →
ProofInfoLe (ExGen := {[ev_x; y]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ((ex, (BoundVarSugar.b0 ∈ml φ)) ---> (patt_free_evar x ∈ml ⌈ φ ⌉))
using i.
Lemma def_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ i x y z:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ φ ⌉ ---> ⌊ ⌈ φ ⌉ ⌋
using i.
Lemma def_tot_phi_impl_tot_phi {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ ⌊ φ ⌋ ⌉ ---> ⌊ φ ⌋ using i.
Lemma floor_is_predicate {Σ : Signature} {syntax : Syntax} Γ φ i x y z:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i is_predicate_pattern (⌊ φ ⌋)
using i.
Lemma def_propagate_not {Σ : Signature} {syntax : Syntax} Γ φ:
theory ⊆ Γ →
well_formed φ →
Γ ⊢i (! ⌈ φ ⌉) <---> (⌊ ! φ ⌋)
using BasicReasoning.
Lemma def_def_phi_impl_tot_def_phi {Σ : Signature} {syntax : Syntax} Γ φ x y z i:
theory ⊆ Γ →
well_formed φ →
x ∉ free_evars φ →
y ∉ free_evars φ ∪ {[x]} →
z ∉ free_evars φ ∪ {[x; y]} →
ProofInfoLe (ExGen := {[ev_x; x; y; z]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ⌈ ⌈ φ ⌉ ⌉ ---> ⌊ ⌈ φ ⌉ ⌋
using i.
Lemma ceil_is_predicate {Σ : Signature} {syntax : Syntax} Γ φ :
theory ⊆ Γ →
well_formed φ →
Γ ⊢i is_predicate_pattern (⌈ φ ⌉)
using AnyReasoning.
Lemma predicate_elim
{Σ : Signature} {syntax : Syntax} Γ (C : PatternCtx) (ψ : Pattern):
theory ⊆ Γ →
well_formed (pcPattern C) →
well_formed ψ →
mu_in_evar_path (pcEvar C) (pcPattern C) 0 = false →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ emplace C patt_bott →
Γ ⊢ emplace C patt_top →
Γ ⊢ emplace C ψ
.
Lemma predicate_propagate_right_2 {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ ---> ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma predicate_propagate_right_2_meta {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma predicate_propagate_left_2 {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ ---> ψ and P ⋅ ϕ <---> (ψ and P) ⋅ ϕ.
Lemma predicate_propagate_left_2_meta {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> (ψ and P) ⋅ ϕ.
Corollary app_prop_under_implication
{Σ : Signature} {syntax : Syntax} Γ: ∀ φ1 φ2 φ3 ψ,
theory ⊆ Γ →
well_formed φ1 →
well_formed φ2 →
well_formed φ3 →
well_formed ψ →
Γ ⊢ is_predicate_pattern φ3 →
Γ ⊢ (φ1 ---> (ψ ⋅ φ2)) ---> (φ1 and φ3) ---> (ψ ⋅ (φ2 and φ3)).
(* TODO: Put in a different file? *)
Lemma predicate_propagate_right {Σ : Signature} {syntax : Syntax} Γ ϕ ψ P :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
well_formed P →
mu_free ϕ →
mu_free ψ →
mu_free P →
Γ ⊢ is_predicate_pattern ψ →
Γ ⊢ ψ and P ⋅ ϕ <---> P ⋅ (ψ and ϕ).
Lemma equal_imp_membership {Σ : Signature} {syntax : Syntax} Γ φ φ' :
theory ⊆ Γ →
well_formed φ → well_formed φ' →
Γ ⊢ ⌈ φ' ⌉ →
Γ ⊢ (φ =ml φ') ---> (φ ∈ml φ').
Lemma phi_impl_ex_in_phi {Σ : Signature} {syntax : Syntax} Γ ϕ:
theory ⊆ Γ →
well_formed ϕ →
Γ ⊢ ϕ ---> (ex , b0 ∈ml ϕ and b0).
Lemma membership_symbol_right {Σ : Signature} {syntax : Syntax} Γ ϕ ψ x :
theory ⊆ Γ →
well_formed ϕ →
well_formed ψ →
mu_free ϕ →
mu_free ψ →
Γ ⊢ (patt_free_evar x ∈ml ψ ⋅ ϕ) ---> (ex , (b0 ∈ml ϕ and patt_free_evar x ∈ml ψ ⋅ b0)).
Lemma disj_equals_greater_1 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ ⊆ml φ₂) ---> ((φ₁ or φ₂) =ml φ₂)
using AnyReasoning.
Lemma disj_equals_greater_2_meta {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i (φ₁ or φ₂) =ml φ₂ using AnyReasoning →
Γ ⊢i φ₁ ⊆ml φ₂ using AnyReasoning.
Lemma disj_equals_greater_2 {Σ : Signature} {syntax : Syntax} Γ φ₁ φ₂:
theory ⊆ Γ →
well_formed φ₁ →
well_formed φ₂ →
mu_free φ₁ → (* TODO get rid of it *)
Γ ⊢i ((φ₁ or φ₂) =ml φ₂) ---> (φ₁ ⊆ml φ₂)
using AnyReasoning.
Lemma bott_not_total {Σ : Signature} {syntax : Syntax}:
∀ Γ, theory ⊆ Γ →
Γ ⊢i ! ⌊ ⊥ ⌋
using AnyReasoning.
Lemma patt_total_and_1 {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ and ψ ⌋ ---> ⌊ φ ⌋ and ⌊ ψ ⌋
using BasicReasoning.
Lemma patt_total_and_2 {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ ⌋ and ⌊ ψ ⌋ ---> ⌊ φ and ψ ⌋
using BasicReasoning.
Lemma patt_total_and {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ,
theory ⊆ Γ →
well_formed φ → well_formed ψ →
Γ ⊢i ⌊ φ and ψ ⌋ <---> ⌊ φ ⌋ and ⌊ ψ ⌋
using BasicReasoning.
Lemma membership_var {Σ : Signature} {syntax : Syntax} :
∀ x y Γ,
theory ⊆ Γ →
Γ ⊢ patt_free_evar y ∈ml patt_free_evar x ---> patt_free_evar y =ml patt_free_evar x.
Lemma mlSpecializeMeta {Σ : Signature} {syntax : Syntax} :
∀ Γ φ ψ, theory ⊆ Γ→
well_formed (ex , φ) → well_formed ψ → mu_free φ →
Γ ⊢i (all , φ) using AnyReasoning →
Γ ⊢i ex , ψ =ml b0 using AnyReasoning →
Γ ⊢i φ^[evar: 0 ↦ ψ] using AnyReasoning.
(* TODO: make sure that the final assumption does not solve goals we do not want to solve. *)
Tactic Notation "mlSpecMeta" ident(hyp) "with" constr(t) :=
unshelve (eapply (@mlSpecializeMeta _ _ _ _ t) in hyp); try_wfauto2; try assumption.
Local Lemma test_spec {Σ : Signature} {syntax : Syntax}:
∀ Γ φ ψ, theory ⊆ Γ→
well_formed (ex , φ) → well_formed ψ → mu_free φ →
Γ ⊢i (all , φ) using AnyReasoning →
Γ ⊢i ex , ψ =ml b0 using AnyReasoning →
Γ ⊢i φ^[evar: 0 ↦ ψ] using AnyReasoning.
Lemma MLGoal_mlSpecialize {Σ : Signature} {syntax : Syntax} Γ l₁ l₂ p t g name:
theory ⊆ Γ →
mu_free p → well_formed t →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name p^[evar: 0 ↦ t]) ::l₂ ) g AnyReasoning →
mkMLGoal Σ Γ (l₁ ++ (mkNH _ name ((all, p) and (ex , t =ml b0)))::l₂) g AnyReasoning.
This tactic can be used on local hypotheses shaped in the following way:
(all , φ) and ex , t = b0
Tactic Notation "mlSpecn" constr(n) :=
_mlReshapeHypsByIdx n;
apply MLGoal_mlSpecialize; [ auto | wf_auto2 | wf_auto2 | _mlReshapeHypsBack ].
Tactic Notation "mlSpec" constr(name') :=
_mlReshapeHypsByName name';
apply MLGoal_mlSpecialize; [ auto | wf_auto2 | wf_auto2 | _mlReshapeHypsBack ].
Goal ∀ (Σ : Signature) (syntax : Syntax) Γ φ t,
theory ⊆ Γ → mu_free φ → well_formed t → well_formed (ex , φ) →
Γ ⊢i (all , φ) ---> (ex , t =ml b0) ---> φ^[evar: 0 ↦ t] using AnyReasoning.
_mlReshapeHypsByIdx n;
apply MLGoal_mlSpecialize; [ auto | wf_auto2 | wf_auto2 | _mlReshapeHypsBack ].
Tactic Notation "mlSpec" constr(name') :=
_mlReshapeHypsByName name';
apply MLGoal_mlSpecialize; [ auto | wf_auto2 | wf_auto2 | _mlReshapeHypsBack ].
Goal ∀ (Σ : Signature) (syntax : Syntax) Γ φ t,
theory ⊆ Γ → mu_free φ → well_formed t → well_formed (ex , φ) →
Γ ⊢i (all , φ) ---> (ex , t =ml b0) ---> φ^[evar: 0 ↦ t] using AnyReasoning.
Lemma forall_defined {Σ : Signature} {syntax : Syntax}:
∀ Γ i, theory ⊆ Γ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i all , ⌈b0⌉ using i.
Lemma membership_refl {Σ : Signature} {syntax : Syntax}:
∀ Γ t, well_formed t →
theory ⊆ Γ→ Γ ⊢i ((ex , t =ml b0) ---> t ∈ml t) using AnyReasoning.
Lemma MLGoal_reflexivity {Σ : Signature} {syntax : Syntax} Γ l ϕ i :
theory ⊆ Γ →
mkMLGoal _ Γ l (ϕ =ml ϕ) i.
Local Example mlReflexivity_test {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i ϕ ---> ψ ---> ψ =ml ψ using BasicReasoning.
(* TODO: strengthen proof info about this: *)
Lemma MLGoal_symmetry {Σ : Signature} {syntax : Syntax} Γ l ϕ ψ i :
theory ⊆ Γ →
mkMLGoal _ Γ l (ϕ =ml ψ) i →
mkMLGoal _ Γ l (ψ =ml ϕ) i.
(* TODO: strengthen proof info about this: *)
Lemma MLGoal_symmetryIn {Σ : Signature} {syntax : Syntax} name Γ l1 l2 ϕ ψ g i :
theory ⊆ Γ →
mkMLGoal _ Γ (l1 ++ (mkNH _ name (ϕ =ml ψ)) :: l2) g i →
mkMLGoal _ Γ (l1 ++ (mkNH _ name (ψ =ml ϕ)) :: l2) g i.
Tactic Notation "mlSymmetry" :=
_ensureProofMode;
tryif apply MLGoal_symmetry; [try assumption; try timeout 5 set_solver|]
then idtac
else fail "mlSymmetry: matching logic goal is not an equality".
Tactic Notation "mlSymmetry" "in" constr(name) :=
_ensureProofMode;
_mlReshapeHypsByName name;
tryif apply (MLGoal_symmetryIn name); [try assumption; try timeout 5 set_solver|];
_mlReshapeHypsBack
then idtac
else fail "mlSymmetry: given local hypothesis is not an equality".
Local Example mlSymmetry_test {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i ψ ---> ϕ =ml ψ ---> ϕ =ml ψ using AnyReasoning.
Tactic Notation "mlRewriteBy" "->" constr(name) "at" constr(atn) := mlRewriteBy name at atn.
Tactic Notation "mlRewriteBy" "<-" constr(name) "at" constr(atn) :=
mlSymmetry in name;
mlRewriteBy name at atn;
mlSymmetry in name.
(* TODO: Replace with something safer *)
Tactic Notation "mlRewriteBy" constr(name) "at" constr(atn) "in" constr(hypo) :=
mlRevert hypo;
mlRewriteBy name at atn;
mlIntro hypo.
Tactic Notation "mlRewriteBy" "->" constr(name) "at" constr(atn) "in" constr(hypo) := mlRewriteBy name at atn in hypo.
Tactic Notation "mlRewriteBy" "<-" constr(name) "at" constr(atn) "in" constr(hypo) :=
mlSymmetry in name;
mlRewriteBy name at atn in hypo;
mlSymmetry in name.
Local Example mlRewriteBy_test_in_barr {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
! (ψ ---> ϕ) --->
! (ϕ =ml ψ)
using AnyReasoning.
Local Example mlRewriteBy_test_in {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
! (ψ ---> ϕ) --->
! (ψ =ml ϕ)
using AnyReasoning.
Local Example mlRewriteBy_test_barr {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
(ψ =ml ϕ) --->
! ψ ---> ! ϕ
using AnyReasoning.
Tactic Notation "mlTransitivity" constr(a1) "->" constr(a2) "as" constr(nam) :=
_ensureProofMode;
match goal with
| [ |- context[mkNH _ a1 (@patt_equal _ _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_equal _ _ b ?c)] ] ⇒
mlAssert (nam : (a =ml c)); [wf_auto2 | mlRewriteBy a1 at 1; mlAssumption | ]
end
| [ |- context[mkNH _ a1 (@patt_imp _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_imp _ b ?c)] ] ⇒
mlAssert (nam : (a ---> c)); [wf_auto2 | mlIntro; mlApply a2; mlApply a1; mlAssumption | ]
end
| [ |- context[mkNH _ a1 (@patt_iff _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_iff _ b ?c)] ] ⇒
mlAssert (nam : (a <---> c)); [wf_auto2 | mlSplitAnd; mlIntro; mlDestructAnd a1; mlDestructAnd a2; [mlTauto|mlTauto]|]
end
end.
Local Example mlTransitivity_test_imp {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a ---> b) --->
(b ---> c) --->
a ---> c
using AnyReasoning.
Local Example mlTransitivity_test_mleq {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a =ml b) --->
(b =ml c) --->
a =ml c
using AnyReasoning.
(* TODO: Super slow due to mlTauto *)
Local Example mlTransitivity_test_iff {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a <---> b) --->
(b <---> c) --->
a <---> c
using AnyReasoning.
(* TODO: eliminate mu_free *)
Lemma patt_equal_trans {Σ : Signature} {syntax : Syntax} Γ φ1 φ2 φ3:
theory ⊆ Γ →
well_formed φ1 → well_formed φ2 → well_formed φ3 →
mu_free φ1 → mu_free φ2 → mu_free φ3 →
Γ ⊢i φ1 =ml φ2 ---> φ2 =ml φ3 ---> φ1 =ml φ3
using AnyReasoning.
(* These are from/should be part of this branch: *)
(* https://github.com/harp-project/AML-Formalization/blob/09f24d95119769ce578c8c15eceba5a3a00c45d4/matching-logic/src/Theories/Nat_ProofSystem.vL392 *)
Section predicate_lemmas.
Context {Σ : Signature} {syntax : Syntax}.
Lemma predicate_equiv :
∀ Γ φ,
theory ⊆ Γ →
well_formed φ →
Γ ⊢ is_predicate_pattern φ ---> φ <---> ⌊φ⌋.
Lemma predicate_imp :
∀ Γ φ ψ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed ψ →
Γ ⊢ is_predicate_pattern φ --->
is_predicate_pattern ψ --->
is_predicate_pattern (φ ---> ψ).
Lemma predicate_bott : ∀ Γ,
theory ⊆ Γ → Γ ⊢ is_predicate_pattern ⊥.
Lemma predicate_not : ∀ Γ φ,
theory ⊆ Γ → well_formed φ →
Γ ⊢ is_predicate_pattern φ ---> is_predicate_pattern (! φ).
Lemma predicate_or : ∀ Γ φ₁ φ₂,
theory ⊆ Γ → well_formed φ₁ → well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ ---> is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ or φ₂).
Lemma predicate_and : ∀ Γ φ₁ φ₂,
theory ⊆ Γ → well_formed φ₁ → well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ ---> is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ and φ₂).
End predicate_lemmas.
Theorem subset_iff_eq {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ φ' : Pattern) (i : ProofInfo) ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed φ' →
Γ ⊢i φ ⊆ml φ' and φ' ⊆ml φ <--->
φ =ml φ' using i.
Theorem subset_disj {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ φ₁ φ₂ : Pattern) (i : ProofInfo) ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( φ₁ or φ₂ ) ⊆ml φ <--->
φ₁ ⊆ml φ and φ₂ ⊆ml φ using i.
Theorem forall_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 →
Γ ⊢ is_functional φ' →
Γ ⊢ (all , φ) → Γ ⊢i φ^[evar:0↦φ'] using AnyReasoning.
Theorem total_iff_top {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ <---> (φ =ml patt_top) using AnyReasoning.
∀ Γ i, theory ⊆ Γ →
ProofInfoLe (ExGen := {[ev_x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i all , ⌈b0⌉ using i.
Lemma membership_refl {Σ : Signature} {syntax : Syntax}:
∀ Γ t, well_formed t →
theory ⊆ Γ→ Γ ⊢i ((ex , t =ml b0) ---> t ∈ml t) using AnyReasoning.
Lemma MLGoal_reflexivity {Σ : Signature} {syntax : Syntax} Γ l ϕ i :
theory ⊆ Γ →
mkMLGoal _ Γ l (ϕ =ml ϕ) i.
Local Example mlReflexivity_test {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i ϕ ---> ψ ---> ψ =ml ψ using BasicReasoning.
(* TODO: strengthen proof info about this: *)
Lemma MLGoal_symmetry {Σ : Signature} {syntax : Syntax} Γ l ϕ ψ i :
theory ⊆ Γ →
mkMLGoal _ Γ l (ϕ =ml ψ) i →
mkMLGoal _ Γ l (ψ =ml ϕ) i.
(* TODO: strengthen proof info about this: *)
Lemma MLGoal_symmetryIn {Σ : Signature} {syntax : Syntax} name Γ l1 l2 ϕ ψ g i :
theory ⊆ Γ →
mkMLGoal _ Γ (l1 ++ (mkNH _ name (ϕ =ml ψ)) :: l2) g i →
mkMLGoal _ Γ (l1 ++ (mkNH _ name (ψ =ml ϕ)) :: l2) g i.
Tactic Notation "mlSymmetry" :=
_ensureProofMode;
tryif apply MLGoal_symmetry; [try assumption; try timeout 5 set_solver|]
then idtac
else fail "mlSymmetry: matching logic goal is not an equality".
Tactic Notation "mlSymmetry" "in" constr(name) :=
_ensureProofMode;
_mlReshapeHypsByName name;
tryif apply (MLGoal_symmetryIn name); [try assumption; try timeout 5 set_solver|];
_mlReshapeHypsBack
then idtac
else fail "mlSymmetry: given local hypothesis is not an equality".
Local Example mlSymmetry_test {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i ψ ---> ϕ =ml ψ ---> ϕ =ml ψ using AnyReasoning.
Tactic Notation "mlRewriteBy" "->" constr(name) "at" constr(atn) := mlRewriteBy name at atn.
Tactic Notation "mlRewriteBy" "<-" constr(name) "at" constr(atn) :=
mlSymmetry in name;
mlRewriteBy name at atn;
mlSymmetry in name.
(* TODO: Replace with something safer *)
Tactic Notation "mlRewriteBy" constr(name) "at" constr(atn) "in" constr(hypo) :=
mlRevert hypo;
mlRewriteBy name at atn;
mlIntro hypo.
Tactic Notation "mlRewriteBy" "->" constr(name) "at" constr(atn) "in" constr(hypo) := mlRewriteBy name at atn in hypo.
Tactic Notation "mlRewriteBy" "<-" constr(name) "at" constr(atn) "in" constr(hypo) :=
mlSymmetry in name;
mlRewriteBy name at atn in hypo;
mlSymmetry in name.
Local Example mlRewriteBy_test_in_barr {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
! (ψ ---> ϕ) --->
! (ϕ =ml ψ)
using AnyReasoning.
Local Example mlRewriteBy_test_in {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
! (ψ ---> ϕ) --->
! (ψ =ml ϕ)
using AnyReasoning.
Local Example mlRewriteBy_test_barr {Σ : Signature} {syntax : Syntax} Γ ϕ ψ :
theory ⊆ Γ → well_formed ϕ → well_formed ψ →
Γ ⊢i
(ψ =ml ϕ) --->
! ψ ---> ! ϕ
using AnyReasoning.
Tactic Notation "mlTransitivity" constr(a1) "->" constr(a2) "as" constr(nam) :=
_ensureProofMode;
match goal with
| [ |- context[mkNH _ a1 (@patt_equal _ _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_equal _ _ b ?c)] ] ⇒
mlAssert (nam : (a =ml c)); [wf_auto2 | mlRewriteBy a1 at 1; mlAssumption | ]
end
| [ |- context[mkNH _ a1 (@patt_imp _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_imp _ b ?c)] ] ⇒
mlAssert (nam : (a ---> c)); [wf_auto2 | mlIntro; mlApply a2; mlApply a1; mlAssumption | ]
end
| [ |- context[mkNH _ a1 (@patt_iff _ ?a ?b)] ] ⇒
match goal with
| [ |- context[mkNH _ a2 (@patt_iff _ b ?c)] ] ⇒
mlAssert (nam : (a <---> c)); [wf_auto2 | mlSplitAnd; mlIntro; mlDestructAnd a1; mlDestructAnd a2; [mlTauto|mlTauto]|]
end
end.
Local Example mlTransitivity_test_imp {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a ---> b) --->
(b ---> c) --->
a ---> c
using AnyReasoning.
Local Example mlTransitivity_test_mleq {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a =ml b) --->
(b =ml c) --->
a =ml c
using AnyReasoning.
(* TODO: Super slow due to mlTauto *)
Local Example mlTransitivity_test_iff {Σ : Signature} {syntax : Syntax} Γ a b c :
theory ⊆ Γ → well_formed a → well_formed b → well_formed c →
Γ ⊢i
(a <---> b) --->
(b <---> c) --->
a <---> c
using AnyReasoning.
(* TODO: eliminate mu_free *)
Lemma patt_equal_trans {Σ : Signature} {syntax : Syntax} Γ φ1 φ2 φ3:
theory ⊆ Γ →
well_formed φ1 → well_formed φ2 → well_formed φ3 →
mu_free φ1 → mu_free φ2 → mu_free φ3 →
Γ ⊢i φ1 =ml φ2 ---> φ2 =ml φ3 ---> φ1 =ml φ3
using AnyReasoning.
(* These are from/should be part of this branch: *)
(* https://github.com/harp-project/AML-Formalization/blob/09f24d95119769ce578c8c15eceba5a3a00c45d4/matching-logic/src/Theories/Nat_ProofSystem.vL392 *)
Section predicate_lemmas.
Context {Σ : Signature} {syntax : Syntax}.
Lemma predicate_equiv :
∀ Γ φ,
theory ⊆ Γ →
well_formed φ →
Γ ⊢ is_predicate_pattern φ ---> φ <---> ⌊φ⌋.
Lemma predicate_imp :
∀ Γ φ ψ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed ψ →
Γ ⊢ is_predicate_pattern φ --->
is_predicate_pattern ψ --->
is_predicate_pattern (φ ---> ψ).
Lemma predicate_bott : ∀ Γ,
theory ⊆ Γ → Γ ⊢ is_predicate_pattern ⊥.
Lemma predicate_not : ∀ Γ φ,
theory ⊆ Γ → well_formed φ →
Γ ⊢ is_predicate_pattern φ ---> is_predicate_pattern (! φ).
Lemma predicate_or : ∀ Γ φ₁ φ₂,
theory ⊆ Γ → well_formed φ₁ → well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ ---> is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ or φ₂).
Lemma predicate_and : ∀ Γ φ₁ φ₂,
theory ⊆ Γ → well_formed φ₁ → well_formed φ₂ →
Γ ⊢ is_predicate_pattern φ₁ ---> is_predicate_pattern φ₂ --->
is_predicate_pattern (φ₁ and φ₂).
End predicate_lemmas.
Theorem subset_iff_eq {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ φ' : Pattern) (i : ProofInfo) ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed φ' →
Γ ⊢i φ ⊆ml φ' and φ' ⊆ml φ <--->
φ =ml φ' using i.
Theorem subset_disj {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ φ₁ φ₂ : Pattern) (i : ProofInfo) ,
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
well_formed φ₁ →
well_formed φ₂ →
Γ ⊢i ( φ₁ or φ₂ ) ⊆ml φ <--->
φ₁ ⊆ml φ and φ₂ ⊆ml φ using i.
Theorem forall_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 →
Γ ⊢ is_functional φ' →
Γ ⊢ (all , φ) → Γ ⊢i φ^[evar:0↦φ'] using AnyReasoning.
Theorem total_iff_top {Σ : Signature} {syntax : Syntax}:
∀ (Γ : Theory) (φ : Pattern),
Definedness_Syntax.theory ⊆ Γ →
well_formed φ →
Γ ⊢i ⌊ φ ⌋ <---> (φ =ml patt_top) using AnyReasoning.
This page has been generated by coqdoc