File Firstorder
From MatchingLogic Require Export FreshnessManager.
From MatchingLogic.ProofMode Require Export Propositional.
Import MatchingLogic.Logic.Notations.
Section with_signature.
Context {Σ : Signature}.
(*
Γ ⊢ φ₁ → φ₂
-------------------- (x ∉ FV(φ₂))
Γ ⊢ (∃x. φ₁) → φ₂
*)
Lemma Ex_gen (Γ : Theory) (ϕ₁ ϕ₂ : Pattern) (x : evar) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := {[x]};
pi_substituted_svars := ∅;
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}) i} :
x ∉ free_evars ϕ₂ →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁ ---> ϕ₂) using i.
(*
Γ ⊢ φy/x → ∃x. φ
*)
Lemma Ex_quan (Γ : Theory) (ϕ : Pattern) (y : evar) :
well_formed (patt_exists ϕ) →
Γ ⊢i (instantiate (patt_exists ϕ) (patt_free_evar y) ---> (patt_exists ϕ))
using BasicReasoning.
(*
Γ ⊢ φ
--------------
Γ ⊢ ∀x. φ
*)
Lemma universal_generalization Γ ϕ x (i : ProofInfo) :
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
well_formed ϕ →
Γ ⊢i ϕ using i →
Γ ⊢i patt_forall (ϕ^{{evar: x ↦ 0}}) using i.
(*
Γ ⊢ (∀x. φ) → φ
DO NOT use quantification here instead of opening
*)
Lemma forall_variable_substitution Γ ϕ x:
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) ---> ϕ^{evar:0 ↦ x} using BasicReasoning.
Lemma forall_variable_substitution_meta Γ ϕ x i:
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) using i → Γ ⊢i ϕ^{evar:0 ↦ x} using i.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∃x. φ₁) → (∃x. φ₂)
*)
Lemma ex_quan_monotone Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i) :
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁) ---> (exists_quantify x ϕ₂) using i.
(*
Γ ⊢ (∃x. φ₁ /\ φ₂) -> (∃x. φ₁)
*)
Lemma ex_quan_and_proj1 Γ x ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
Γ ⊢i (exists_quantify x (ϕ₁ and ϕ₂)) ---> (exists_quantify x ϕ₁)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ (∃x. φ₁ /\ φ₂) -> (∃x. φ₂)
*)
Lemma ex_quan_and_proj2 Γ x ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
Γ ⊢i (exists_quantify x (ϕ₁ and ϕ₂)) ---> (exists_quantify x ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ φ₁ → φ₂
----------------------------
Γ ⊢ φ₁ → ∀x. φ₂
*)
(* identity *)
Lemma strip_exists_quantify_l Γ x P Q i :
x ∉ free_evars P →
well_formed_closed_ex_aux P 1 →
Γ ⊢i (exists_quantify x (P^{evar: 0 ↦ x}) ---> Q) using i →
Γ ⊢i (ex , P) ---> Q using i.
(* identity *)
Lemma strip_exists_quantify_r Γ x P Q i :
x ∉ free_evars Q →
well_formed_closed_ex_aux Q 1 →
Γ ⊢i P ---> (exists_quantify x (Q^{evar: 0 ↦ x})) using i →
Γ ⊢i P ---> ex, Q using i.
(* prenex-exists-and-left *)
(*
Γ ⊢ ((∃x. φ₁) /\ φ₂) → (∃x. (φ₁ /\ φ₂))
*)
Lemma prenex_exists_and_1 (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i ((ex, ϕ₁) and ϕ₂) ---> (ex, (ϕ₁ and ϕ₂))
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(* prenex-exists-and-right *)
(*
Γ ⊢ (∃x. (φ₁ /\ φ₂)) → ((∃x. φ₁) /\ φ₂)
*)
Lemma prenex_exists_and_2 (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i (ex, (ϕ₁ and ϕ₂)) ---> ((ex, ϕ₁) and ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ (∃x. (φ₁ /\ φ₂)) ↔ ((∃x. φ₁) /\ φ₂)
*)
Lemma prenex_exists_and_iff (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i (ex, (ϕ₁ and ϕ₂)) <---> ((ex, ϕ₁) and ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
This is basically universal_generalization
but under an implication.
I wonder if we could get an iterative version forall_gen_iter?
Like,
Γ ⊢ φ₁ → ... → φₖ → ψ
----------------------------
Γ ⊢ φ₁ → ... → φₖ → ∀x. ψ
*)
Lemma forall_gen Γ ϕ₁ ϕ₂ x (i : ProofInfo):
evar_is_fresh_in x ϕ₁ →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ---> all, (ϕ₂^{{evar: x ↦ 0}}) using i.
(*
Γ ⊢ (∀x. φ) → φ
This is the same as forall_variable_substitution
except that here we have a ProofInfoLe assumption
instead of a concrete using clause.
*)
Lemma forall_variable_substitution' Γ ϕ x (i : ProofInfo):
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) ---> ϕ^{evar:0 ↦ x} using i.
(*
Γ ⊢ ∀x. φ
----------
Γ ⊢ φ
*)
Lemma forall_elim Γ ϕ x (i : ProofInfo):
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) using i →
Γ ⊢i (ϕ^{evar: 0 ↦ x}) using i.
(*
Γ ⊢ ∀x. (φ₁ → φ₂)
------------------
Γ ⊢ (∃x. φ₁) → φ₂
When applied backwards,
turns an existential quantification on the LHS of an implication
into an universal quantification on top.
I wonder if we can get an iterative version, saying that
Γ ⊢ ∀ x. (φ₁ → ... → φᵢ → ... → φₖ → ψ)
------------------
Γ ⊢ φ₁ → ... → (∃x. φᵢ) → ... → φₖ → ψ
Even better, I would like to have a version which says that
Γ ⊢ ∀ x₁,...,xₘ,x. (φ₁ → ... → φᵢ → ... → φₖ → ψ)
------------------
Γ ⊢ ∀ x₁,...,xₘ. (φ₁ → ... → (∃x. φᵢ) → ... → φₖ → ψ)
because that would basically implement mgDestructEx,
assuming we hide the leading universal quantifiers.
TODO: parameterize this lemma with a variable which is fresh in (ϕ₁ ---> ϕ₂),
instead of hard-coding the fresh generation.
*)
Lemma prenex_forall_imp Γ ϕ₁ ϕ₂ i x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i (all, (ϕ₁ ---> ϕ₂)) using i →
Γ ⊢i (ex, ϕ₁) ---> (ϕ₂) using i.
Lemma Ex_gen_lifted (Γ : Theory) (ϕ₁ : Pattern) (l : hypotheses) (n : string) (g : Pattern) (x : evar)
(i : ProofInfo) :
evar_is_fresh_in x g →
evar_is_fresh_in_list x (patterns_of l) →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
bevar_occur ϕ₁ 0 = false →
mkMLGoal Σ Γ (mkNH _ n ϕ₁::l) g i →
mkMLGoal Σ Γ (mkNH _ n (exists_quantify x ϕ₁)::l) g i.
(* Weakening under existential *)
Local Example ex_exists Γ ϕ₁ ϕ₂ ϕ₃ i:
well_formed (ex, ϕ₁) →
well_formed (ex, ϕ₂) →
well_formed ϕ₃ →
ProofInfoLe ( (ExGen := {[(evar_fresh (elements (free_evars ϕ₁ ∪ free_evars ϕ₂ ∪ free_evars (ex, ϕ₃))))]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i (all, (ϕ₁ and ϕ₃ ---> ϕ₂)) using i →
Γ ⊢i (ex, ϕ₁) ---> ϕ₃ ---> (ex, ϕ₂) using i.
Lemma existential_instantiation :
∀ Γ (φ : Pattern) x y, well_formed φ → x ≠ y → y ∉ free_evars φ →
Γ ⊢i exists_quantify x φ ---> φ^[[evar: x ↦ patt_free_evar y]]
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma MLGoal_IntroVar : ∀ Γ l g i x,
x ∉ free_evars g →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
mkMLGoal Σ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal Σ Γ l (all , g) i.
Lemma propagate_forall (Γ : Theory):
∀ ϕ₁ ϕ₂ x,
well_formed ϕ₁ →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ →
Γ ⊢i ((all, (ϕ₁ ---> ϕ₂^{{evar:x↦0}})) ---> (ϕ₁ ---> all, ϕ₂^{{evar:x↦0}}))
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma universal_generalization_iter (Γ : Theory):
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed ϕ →
x ∉ free_evars_of_list l →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i foldr patt_imp ϕ l using i →
Γ ⊢i foldr patt_imp (all , ϕ^{{evar: x ↦ 0}}) l using i.
Lemma MLGoal_forallIntro Γ l g (x : evar) i :
x ∉ free_evars_of_list (patterns_of l) →
x ∉ free_evars g →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
mkMLGoal _ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal _ Γ l (all, g) i.
(* NOTE: this is not too good with quantification in the concusion.
Opening is better, when there is no condition about the
freshness of variables (i.e. Ex_gen is not used). *)
Lemma specialize_forall (Γ : Theory) :
∀ (l₁ l₂ : list Pattern) (ϕ ψ : Pattern) x i,
well_formed ϕ → well_formed (ex, ψ) → Pattern.wf l₁ → Pattern.wf l₂ →
Γ ⊢i foldr patt_imp ϕ (l₁ ++ ψ^{evar:0 ↦ x} :: l₂) using i →
Γ ⊢i foldr patt_imp ϕ (l₁ ++ (all, ψ) :: l₂) using i.
Lemma MLGoal_specializeAll Γ l₁ l₂ (g ψ : Pattern) x i name :
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (ψ^{evar:0 ↦ x})) :: l₂) g i →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (all, ψ)) :: l₂) g i.
(* This is more efficient in proof term size, than the version below based on specialize: *)
Lemma revert_forall_iter (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp (all , ϕ) l ---> foldr patt_imp ϕ^{evar: 0 ↦ x} l
using BasicReasoning.
Lemma revert_forall_iter_meta (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp (all , ϕ) l using i →
Γ ⊢i foldr patt_imp (ϕ^{evar: 0 ↦ x}) l using i.
(* Here, we change opening in the conclusion to quantification in the premise
to simplify pattern matching for the tactic *)
Lemma MLGoal_revertAll Γ l g (x : evar) i :
mkMLGoal _ Γ l (all, g^{{evar:x ↦ 0}}) i →
mkMLGoal _ Γ l g i.
Lemma ex_quan_iter (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp ϕ^{evar:0 ↦ x} l ---> foldr patt_imp (ex, ϕ) l
using BasicReasoning.
Lemma ex_quan_iter_meta (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp ϕ^{evar:0 ↦ x} l using i →
Γ ⊢i foldr patt_imp (ex, ϕ) l using i.
Lemma MLGoal_exists Γ l g (x : evar) i :
mkMLGoal _ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal _ Γ l (ex, g) i.
Lemma exists_elim Γ : ∀ l₁ l₂ g ϕ i x,
well_formed (ex, ϕ) → Pattern.wf l₁ → Pattern.wf l₂ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
x ∉ free_evars ϕ →
x ∉ free_evars g →
x ∉ free_evars_of_list l₁ →
x ∉ free_evars_of_list l₂ →
Γ ⊢i foldr patt_imp g (l₁ ++ ϕ^{evar:0 ↦ x} :: l₂) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ (ex, ϕ) :: l₂) using i.
Lemma MLGoal_destructEx Γ l₁ l₂ g (x : evar) name ϕ i :
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
x ∉ free_evars_of_list (map nh_patt l₁) →
x ∉ free_evars_of_list (map nh_patt l₂) →
x ∉ free_evars ϕ →
x ∉ free_evars g →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name ϕ^{evar:0 ↦ x}) :: l₂) g i →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (ex, ϕ)) :: l₂) g i.
End with_signature.
Open Scope ml_scope.
Open Scope string_scope.
(* TODO: reformulate in Ltac2 - depends on the Freshness Manager *)
(* NOTE: This tactic should work even if x was already introduced by the freshness manager. If x is present, but was not introduced by the freshness manager, use mlIntroAllManual. *)
Tactic Notation "mlIntroAll" ident(x) :=
_ensureProofMode;
try mlFreshEvar as x;
tryif apply (MLGoal_forallIntro _ _ _ x);
[ try fm_solve
| try fm_solve
| try subst x; try_solve_pile
| unfold evar_open; mlSimpl;
repeat (rewrite bevar_subst_not_occur; [by wf_auto2|])
]
then idtac
else fail "mlIntroAll: matching logic goal is not a universally quantified pattern".
Tactic Notation "mlIntroAllManual" constr(x) :=
_ensureProofMode;
tryif apply (MLGoal_forallIntro _ _ _ x);
[
|
|
| unfold evar_open; mlSimpl;
repeat (rewrite bevar_subst_not_occur; [try by wf_auto2|])
]
then idtac
else fail "mlIntroAll: matching logic goal is not a universally quantified pattern".
Local Example forall_test_1 {Σ : Signature} Γ ϕ:
well_formed ϕ →
Γ ⊢ all , (ϕ ---> ϕ and ϕ).
Restart.
Restart.
Qed.
(* The FreshMan does not handle this case yet
Local Example forall_test_2 {Σ : Signature} Γ ϕ ψ x:
well_formed ϕ -> well_formed (ex, ψ) ->
x ∉ free_evars ϕ ->
x ∉ free_evars ψ ->
Γ ⊢ ϕ ---> ψ^{evar:0 ↦ x} ->
Γ ⊢ (ϕ ---> all, ψ).
Proof.
intros.
toMLGoal. wf_auto2.
mlIntro. mlIntroAll x.
by fromMLGoal.
Qed.
*)
Tactic Notation "mlRevertAll" constr(x) :=
_ensureProofMode;
apply (MLGoal_revertAll _ _ _ x).
Local Example revert_test {Σ : Signature} Γ ϕ ψ x:
well_formed ϕ → well_formed (ex, ψ) →
x ∉ free_evars ϕ →
x ∉ free_evars ψ →
Γ ⊢ (ϕ ---> all, ψ) →
Γ ⊢ ϕ ---> ψ^{evar:0 ↦ x}.
Local Example forall_revert_test_1 {Σ : Signature} Γ ϕ ψ:
well_formed ϕ → well_formed (ex, ψ) →
Γ ⊢ (ϕ ---> all, ψ) →
Γ ⊢ all, ϕ ---> ψ.
Local Example forall_revert_test_2 {Σ : Signature} Γ ϕ ψ ξ:
well_formed ξ → well_formed ϕ → well_formed (ex, ψ) →
Γ ⊢ (ξ ---> ϕ ---> all, ψ) →
Γ ⊢ all, ξ ---> ϕ ---> ψ.
Local Example destruct_or_f {Σ : Signature} Γ ϕ₁ ϕ₂ ψ:
well_formed (ex, ϕ₁) → well_formed (ex, ϕ₂) → well_formed (ex, ψ) →
Γ ⊢ all, ϕ₁ ---> ψ → Γ ⊢ all, ϕ₂ ---> ψ →
Γ ⊢ all, ϕ₁ or ϕ₂ ---> ψ.
Tactic Notation "mlSpecialize" constr(name') "with" constr(var) :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply (MLGoal_specializeAll _ _ _ _ _ var);
_mlReshapeHypsBack
then idtac
else fail "mlSpecialize: given local hypothesis is not a universally quantified pattern".
(* revert is a corollary of specialize: *)
Local Lemma Private_revert_forall_iter {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed ϕ →
Γ ⊢i foldr patt_imp (all , ϕ^{{evar: x ↦ 0}}) l ---> foldr patt_imp ϕ l
using BasicReasoning.
Tactic Notation "mlExists" constr(var) :=
_ensureProofMode;
tryif apply (MLGoal_exists _ _ _ var);
try (rewrite evar_open_evar_quantify;[by wf_auto2|])
then idtac
else fail "mlExists: matching logic goal is not an existentially quantified pattern".
Local Lemma exists_test_1 {Σ : Signature} Γ ϕ :
well_formed (ex, ϕ) →
Γ ⊢ (all, ϕ) ---> (ex, ϕ).
(*(* The order of these two tactics matter! Do not exchange them! *)
Tactic Notation "mlDestructEx" constr(name') "as" constr(x) :=
_ensureProofMode;
_mlReshapeHypsByName name';
apply (MLGoal_destructEx _ _ _ _ x name'); try subst x; try_solve_pile | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | _mlReshapeHypsBack
.
(* The order of this and the previous tactic matter! *)
Tactic Notation "mlDestructEx" constr(name') "as" ident(x) :=
tryif ltac2:(hyp ident:(x))
then mlDestructEx name' as (constr:(x))
else
_ensureProofMode;
_mlReshapeHypsByName name';
mlFreshEvar as x;
apply (MLGoal_destructEx _ _ _ _ x name'); try subst x; try_solve_pile | fm_solve | fm_solve | fm_solve | fm_solve | _mlReshapeHypsBack
.*)
Ltac _mlDestructExManual name' x :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply (MLGoal_destructEx _ _ _ _ x name');[
|
|
|
|
| _mlReshapeHypsBack]
then idtac
else fail "_mlDestructExManual: given local hypothesis is not existentially quantified".
(* NOTE: This tactic should work even if x was already introduced by the freshness manager. If x is present, but was not introduced by the freshness manager, use mlDestructExManual. *)
Ltac _mlDestructExFresh name' x :=
_ensureProofMode;
_mlReshapeHypsByName name';
try mlFreshEvar as x;
tryif apply (MLGoal_destructEx _ _ _ _ x name');[
try subst x; try_solve_pile
| fm_solve
| fm_solve
| fm_solve
| fm_solve
| _mlReshapeHypsBack]
then idtac
else fail "_mlDestructExFresh: given local hypothesis is not existentially quantified".
Tactic Notation "mlDestructExManual" constr(name') "as" constr(x) :=
_mlDestructExManual name' x.
Tactic Notation "mlDestructEx" constr(name') "as" ident(x) :=
(* tryif is_var x (* we need to check whether x is a used ident! *)
then
_mlDestructExManual name' x (* Do not use idtac here, because it breaks tryif for some reason *)
else *)
_mlDestructExFresh name' x (* Do not use idtac here, because it breaks tryif for some reason *)
.
(* Ltac mlDestructEx name' x :=
tryif
match type of x with
| evar => idtac
| _ => fail 1
end
then _mlDestructExManual name' as x
else _mlDestructExFresh name' as x
. *)
Local Lemma destructExDouble_Test {Σ : Signature} Γ ϕ ψ :
well_formed (ex, ϕ) → well_formed (ex, ψ) →
Γ ⊢ (ex, ϕ and ψ) ---> (ex, ϕ and ψ) ---> ex, ϕ.
Local Lemma destructEx_Test {Σ : Signature} Γ ϕ ψ :
well_formed (ex, ϕ) → well_formed (ex, ψ) →
Γ ⊢ (ex, ϕ and ψ) ---> ex, ϕ.
From MatchingLogic.ProofMode Require Export Propositional.
Import MatchingLogic.Logic.Notations.
Section with_signature.
Context {Σ : Signature}.
(*
Γ ⊢ φ₁ → φ₂
-------------------- (x ∉ FV(φ₂))
Γ ⊢ (∃x. φ₁) → φ₂
*)
Lemma Ex_gen (Γ : Theory) (ϕ₁ ϕ₂ : Pattern) (x : evar) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := {[x]};
pi_substituted_svars := ∅;
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}) i} :
x ∉ free_evars ϕ₂ →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁ ---> ϕ₂) using i.
(*
Γ ⊢ φy/x → ∃x. φ
*)
Lemma Ex_quan (Γ : Theory) (ϕ : Pattern) (y : evar) :
well_formed (patt_exists ϕ) →
Γ ⊢i (instantiate (patt_exists ϕ) (patt_free_evar y) ---> (patt_exists ϕ))
using BasicReasoning.
(*
Γ ⊢ φ
--------------
Γ ⊢ ∀x. φ
*)
Lemma universal_generalization Γ ϕ x (i : ProofInfo) :
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
well_formed ϕ →
Γ ⊢i ϕ using i →
Γ ⊢i patt_forall (ϕ^{{evar: x ↦ 0}}) using i.
(*
Γ ⊢ (∀x. φ) → φ
DO NOT use quantification here instead of opening
*)
Lemma forall_variable_substitution Γ ϕ x:
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) ---> ϕ^{evar:0 ↦ x} using BasicReasoning.
Lemma forall_variable_substitution_meta Γ ϕ x i:
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) using i → Γ ⊢i ϕ^{evar:0 ↦ x} using i.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∃x. φ₁) → (∃x. φ₂)
*)
Lemma ex_quan_monotone Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i) :
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁) ---> (exists_quantify x ϕ₂) using i.
(*
Γ ⊢ (∃x. φ₁ /\ φ₂) -> (∃x. φ₁)
*)
Lemma ex_quan_and_proj1 Γ x ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
Γ ⊢i (exists_quantify x (ϕ₁ and ϕ₂)) ---> (exists_quantify x ϕ₁)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ (∃x. φ₁ /\ φ₂) -> (∃x. φ₂)
*)
Lemma ex_quan_and_proj2 Γ x ϕ₁ ϕ₂:
well_formed ϕ₁ = true →
well_formed ϕ₂ = true →
Γ ⊢i (exists_quantify x (ϕ₁ and ϕ₂)) ---> (exists_quantify x ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ φ₁ → φ₂
----------------------------
Γ ⊢ φ₁ → ∀x. φ₂
*)
(* identity *)
Lemma strip_exists_quantify_l Γ x P Q i :
x ∉ free_evars P →
well_formed_closed_ex_aux P 1 →
Γ ⊢i (exists_quantify x (P^{evar: 0 ↦ x}) ---> Q) using i →
Γ ⊢i (ex , P) ---> Q using i.
(* identity *)
Lemma strip_exists_quantify_r Γ x P Q i :
x ∉ free_evars Q →
well_formed_closed_ex_aux Q 1 →
Γ ⊢i P ---> (exists_quantify x (Q^{evar: 0 ↦ x})) using i →
Γ ⊢i P ---> ex, Q using i.
(* prenex-exists-and-left *)
(*
Γ ⊢ ((∃x. φ₁) /\ φ₂) → (∃x. (φ₁ /\ φ₂))
*)
Lemma prenex_exists_and_1 (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i ((ex, ϕ₁) and ϕ₂) ---> (ex, (ϕ₁ and ϕ₂))
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(* prenex-exists-and-right *)
(*
Γ ⊢ (∃x. (φ₁ /\ φ₂)) → ((∃x. φ₁) /\ φ₂)
*)
Lemma prenex_exists_and_2 (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i (ex, (ϕ₁ and ϕ₂)) ---> ((ex, ϕ₁) and ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
Γ ⊢ (∃x. (φ₁ /\ φ₂)) ↔ ((∃x. φ₁) /\ φ₂)
*)
Lemma prenex_exists_and_iff (Γ : Theory) ϕ₁ ϕ₂ x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
Γ ⊢i (ex, (ϕ₁ and ϕ₂)) <---> ((ex, ϕ₁) and ϕ₂)
using ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)).
(*
This is basically universal_generalization
but under an implication.
I wonder if we could get an iterative version forall_gen_iter?
Like,
Γ ⊢ φ₁ → ... → φₖ → ψ
----------------------------
Γ ⊢ φ₁ → ... → φₖ → ∀x. ψ
*)
Lemma forall_gen Γ ϕ₁ ϕ₂ x (i : ProofInfo):
evar_is_fresh_in x ϕ₁ →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ---> all, (ϕ₂^{{evar: x ↦ 0}}) using i.
(*
Γ ⊢ (∀x. φ) → φ
This is the same as forall_variable_substitution
except that here we have a ProofInfoLe assumption
instead of a concrete using clause.
*)
Lemma forall_variable_substitution' Γ ϕ x (i : ProofInfo):
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) ---> ϕ^{evar:0 ↦ x} using i.
(*
Γ ⊢ ∀x. φ
----------
Γ ⊢ φ
*)
Lemma forall_elim Γ ϕ x (i : ProofInfo):
well_formed (ex, ϕ) →
Γ ⊢i (all, ϕ) using i →
Γ ⊢i (ϕ^{evar: 0 ↦ x}) using i.
(*
Γ ⊢ ∀x. (φ₁ → φ₂)
------------------
Γ ⊢ (∃x. φ₁) → φ₂
When applied backwards,
turns an existential quantification on the LHS of an implication
into an universal quantification on top.
I wonder if we can get an iterative version, saying that
Γ ⊢ ∀ x. (φ₁ → ... → φᵢ → ... → φₖ → ψ)
------------------
Γ ⊢ φ₁ → ... → (∃x. φᵢ) → ... → φₖ → ψ
Even better, I would like to have a version which says that
Γ ⊢ ∀ x₁,...,xₘ,x. (φ₁ → ... → φᵢ → ... → φₖ → ψ)
------------------
Γ ⊢ ∀ x₁,...,xₘ. (φ₁ → ... → (∃x. φᵢ) → ... → φₖ → ψ)
because that would basically implement mgDestructEx,
assuming we hide the leading universal quantifiers.
TODO: parameterize this lemma with a variable which is fresh in (ϕ₁ ---> ϕ₂),
instead of hard-coding the fresh generation.
*)
Lemma prenex_forall_imp Γ ϕ₁ ϕ₂ i x:
well_formed (ex, ϕ₁) →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ ∪ free_evars ϕ₂ →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i (all, (ϕ₁ ---> ϕ₂)) using i →
Γ ⊢i (ex, ϕ₁) ---> (ϕ₂) using i.
Lemma Ex_gen_lifted (Γ : Theory) (ϕ₁ : Pattern) (l : hypotheses) (n : string) (g : Pattern) (x : evar)
(i : ProofInfo) :
evar_is_fresh_in x g →
evar_is_fresh_in_list x (patterns_of l) →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
bevar_occur ϕ₁ 0 = false →
mkMLGoal Σ Γ (mkNH _ n ϕ₁::l) g i →
mkMLGoal Σ Γ (mkNH _ n (exists_quantify x ϕ₁)::l) g i.
(* Weakening under existential *)
Local Example ex_exists Γ ϕ₁ ϕ₂ ϕ₃ i:
well_formed (ex, ϕ₁) →
well_formed (ex, ϕ₂) →
well_formed ϕ₃ →
ProofInfoLe ( (ExGen := {[(evar_fresh (elements (free_evars ϕ₁ ∪ free_evars ϕ₂ ∪ free_evars (ex, ϕ₃))))]}, SVSubst := ∅, KT := false, AKT := false)) i →
Γ ⊢i (all, (ϕ₁ and ϕ₃ ---> ϕ₂)) using i →
Γ ⊢i (ex, ϕ₁) ---> ϕ₃ ---> (ex, ϕ₂) using i.
Lemma existential_instantiation :
∀ Γ (φ : Pattern) x y, well_formed φ → x ≠ y → y ∉ free_evars φ →
Γ ⊢i exists_quantify x φ ---> φ^[[evar: x ↦ patt_free_evar y]]
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma MLGoal_IntroVar : ∀ Γ l g i x,
x ∉ free_evars g →
ProofInfoLe ( (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false)) i →
mkMLGoal Σ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal Σ Γ l (all , g) i.
Lemma propagate_forall (Γ : Theory):
∀ ϕ₁ ϕ₂ x,
well_formed ϕ₁ →
well_formed ϕ₂ →
x ∉ free_evars ϕ₁ →
Γ ⊢i ((all, (ϕ₁ ---> ϕ₂^{{evar:x↦0}})) ---> (ϕ₁ ---> all, ϕ₂^{{evar:x↦0}}))
using (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false).
Lemma universal_generalization_iter (Γ : Theory):
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed ϕ →
x ∉ free_evars_of_list l →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i foldr patt_imp ϕ l using i →
Γ ⊢i foldr patt_imp (all , ϕ^{{evar: x ↦ 0}}) l using i.
Lemma MLGoal_forallIntro Γ l g (x : evar) i :
x ∉ free_evars_of_list (patterns_of l) →
x ∉ free_evars g →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
mkMLGoal _ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal _ Γ l (all, g) i.
(* NOTE: this is not too good with quantification in the concusion.
Opening is better, when there is no condition about the
freshness of variables (i.e. Ex_gen is not used). *)
Lemma specialize_forall (Γ : Theory) :
∀ (l₁ l₂ : list Pattern) (ϕ ψ : Pattern) x i,
well_formed ϕ → well_formed (ex, ψ) → Pattern.wf l₁ → Pattern.wf l₂ →
Γ ⊢i foldr patt_imp ϕ (l₁ ++ ψ^{evar:0 ↦ x} :: l₂) using i →
Γ ⊢i foldr patt_imp ϕ (l₁ ++ (all, ψ) :: l₂) using i.
Lemma MLGoal_specializeAll Γ l₁ l₂ (g ψ : Pattern) x i name :
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (ψ^{evar:0 ↦ x})) :: l₂) g i →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (all, ψ)) :: l₂) g i.
(* This is more efficient in proof term size, than the version below based on specialize: *)
Lemma revert_forall_iter (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp (all , ϕ) l ---> foldr patt_imp ϕ^{evar: 0 ↦ x} l
using BasicReasoning.
Lemma revert_forall_iter_meta (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp (all , ϕ) l using i →
Γ ⊢i foldr patt_imp (ϕ^{evar: 0 ↦ x}) l using i.
(* Here, we change opening in the conclusion to quantification in the premise
to simplify pattern matching for the tactic *)
Lemma MLGoal_revertAll Γ l g (x : evar) i :
mkMLGoal _ Γ l (all, g^{{evar:x ↦ 0}}) i →
mkMLGoal _ Γ l g i.
Lemma ex_quan_iter (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp ϕ^{evar:0 ↦ x} l ---> foldr patt_imp (ex, ϕ) l
using BasicReasoning.
Lemma ex_quan_iter_meta (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x i,
Pattern.wf l →
well_formed (ex, ϕ) →
Γ ⊢i foldr patt_imp ϕ^{evar:0 ↦ x} l using i →
Γ ⊢i foldr patt_imp (ex, ϕ) l using i.
Lemma MLGoal_exists Γ l g (x : evar) i :
mkMLGoal _ Γ l (g^{evar: 0 ↦ x}) i →
mkMLGoal _ Γ l (ex, g) i.
Lemma exists_elim Γ : ∀ l₁ l₂ g ϕ i x,
well_formed (ex, ϕ) → Pattern.wf l₁ → Pattern.wf l₂ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
x ∉ free_evars ϕ →
x ∉ free_evars g →
x ∉ free_evars_of_list l₁ →
x ∉ free_evars_of_list l₂ →
Γ ⊢i foldr patt_imp g (l₁ ++ ϕ^{evar:0 ↦ x} :: l₂) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ (ex, ϕ) :: l₂) using i.
Lemma MLGoal_destructEx Γ l₁ l₂ g (x : evar) name ϕ i :
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
x ∉ free_evars_of_list (map nh_patt l₁) →
x ∉ free_evars_of_list (map nh_patt l₂) →
x ∉ free_evars ϕ →
x ∉ free_evars g →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name ϕ^{evar:0 ↦ x}) :: l₂) g i →
mkMLGoal _ Γ (l₁ ++ (mkNH _ name (ex, ϕ)) :: l₂) g i.
End with_signature.
Open Scope ml_scope.
Open Scope string_scope.
(* TODO: reformulate in Ltac2 - depends on the Freshness Manager *)
(* NOTE: This tactic should work even if x was already introduced by the freshness manager. If x is present, but was not introduced by the freshness manager, use mlIntroAllManual. *)
Tactic Notation "mlIntroAll" ident(x) :=
_ensureProofMode;
try mlFreshEvar as x;
tryif apply (MLGoal_forallIntro _ _ _ x);
[ try fm_solve
| try fm_solve
| try subst x; try_solve_pile
| unfold evar_open; mlSimpl;
repeat (rewrite bevar_subst_not_occur; [by wf_auto2|])
]
then idtac
else fail "mlIntroAll: matching logic goal is not a universally quantified pattern".
Tactic Notation "mlIntroAllManual" constr(x) :=
_ensureProofMode;
tryif apply (MLGoal_forallIntro _ _ _ x);
[
|
|
| unfold evar_open; mlSimpl;
repeat (rewrite bevar_subst_not_occur; [try by wf_auto2|])
]
then idtac
else fail "mlIntroAll: matching logic goal is not a universally quantified pattern".
Local Example forall_test_1 {Σ : Signature} Γ ϕ:
well_formed ϕ →
Γ ⊢ all , (ϕ ---> ϕ and ϕ).
Restart.
Restart.
Qed.
(* The FreshMan does not handle this case yet
Local Example forall_test_2 {Σ : Signature} Γ ϕ ψ x:
well_formed ϕ -> well_formed (ex, ψ) ->
x ∉ free_evars ϕ ->
x ∉ free_evars ψ ->
Γ ⊢ ϕ ---> ψ^{evar:0 ↦ x} ->
Γ ⊢ (ϕ ---> all, ψ).
Proof.
intros.
toMLGoal. wf_auto2.
mlIntro. mlIntroAll x.
by fromMLGoal.
Qed.
*)
Tactic Notation "mlRevertAll" constr(x) :=
_ensureProofMode;
apply (MLGoal_revertAll _ _ _ x).
Local Example revert_test {Σ : Signature} Γ ϕ ψ x:
well_formed ϕ → well_formed (ex, ψ) →
x ∉ free_evars ϕ →
x ∉ free_evars ψ →
Γ ⊢ (ϕ ---> all, ψ) →
Γ ⊢ ϕ ---> ψ^{evar:0 ↦ x}.
Local Example forall_revert_test_1 {Σ : Signature} Γ ϕ ψ:
well_formed ϕ → well_formed (ex, ψ) →
Γ ⊢ (ϕ ---> all, ψ) →
Γ ⊢ all, ϕ ---> ψ.
Local Example forall_revert_test_2 {Σ : Signature} Γ ϕ ψ ξ:
well_formed ξ → well_formed ϕ → well_formed (ex, ψ) →
Γ ⊢ (ξ ---> ϕ ---> all, ψ) →
Γ ⊢ all, ξ ---> ϕ ---> ψ.
Local Example destruct_or_f {Σ : Signature} Γ ϕ₁ ϕ₂ ψ:
well_formed (ex, ϕ₁) → well_formed (ex, ϕ₂) → well_formed (ex, ψ) →
Γ ⊢ all, ϕ₁ ---> ψ → Γ ⊢ all, ϕ₂ ---> ψ →
Γ ⊢ all, ϕ₁ or ϕ₂ ---> ψ.
Tactic Notation "mlSpecialize" constr(name') "with" constr(var) :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply (MLGoal_specializeAll _ _ _ _ _ var);
_mlReshapeHypsBack
then idtac
else fail "mlSpecialize: given local hypothesis is not a universally quantified pattern".
(* revert is a corollary of specialize: *)
Local Lemma Private_revert_forall_iter {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (ϕ : Pattern) x,
Pattern.wf l →
well_formed ϕ →
Γ ⊢i foldr patt_imp (all , ϕ^{{evar: x ↦ 0}}) l ---> foldr patt_imp ϕ l
using BasicReasoning.
Tactic Notation "mlExists" constr(var) :=
_ensureProofMode;
tryif apply (MLGoal_exists _ _ _ var);
try (rewrite evar_open_evar_quantify;[by wf_auto2|])
then idtac
else fail "mlExists: matching logic goal is not an existentially quantified pattern".
Local Lemma exists_test_1 {Σ : Signature} Γ ϕ :
well_formed (ex, ϕ) →
Γ ⊢ (all, ϕ) ---> (ex, ϕ).
(*(* The order of these two tactics matter! Do not exchange them! *)
Tactic Notation "mlDestructEx" constr(name') "as" constr(x) :=
_ensureProofMode;
_mlReshapeHypsByName name';
apply (MLGoal_destructEx _ _ _ _ x name'); try subst x; try_solve_pile | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | try subst x; try solve_fresh; try solve_free_evars 10 | _mlReshapeHypsBack
.
(* The order of this and the previous tactic matter! *)
Tactic Notation "mlDestructEx" constr(name') "as" ident(x) :=
tryif ltac2:(hyp ident:(x))
then mlDestructEx name' as (constr:(x))
else
_ensureProofMode;
_mlReshapeHypsByName name';
mlFreshEvar as x;
apply (MLGoal_destructEx _ _ _ _ x name'); try subst x; try_solve_pile | fm_solve | fm_solve | fm_solve | fm_solve | _mlReshapeHypsBack
.*)
Ltac _mlDestructExManual name' x :=
_ensureProofMode;
_mlReshapeHypsByName name';
tryif apply (MLGoal_destructEx _ _ _ _ x name');[
|
|
|
|
| _mlReshapeHypsBack]
then idtac
else fail "_mlDestructExManual: given local hypothesis is not existentially quantified".
(* NOTE: This tactic should work even if x was already introduced by the freshness manager. If x is present, but was not introduced by the freshness manager, use mlDestructExManual. *)
Ltac _mlDestructExFresh name' x :=
_ensureProofMode;
_mlReshapeHypsByName name';
try mlFreshEvar as x;
tryif apply (MLGoal_destructEx _ _ _ _ x name');[
try subst x; try_solve_pile
| fm_solve
| fm_solve
| fm_solve
| fm_solve
| _mlReshapeHypsBack]
then idtac
else fail "_mlDestructExFresh: given local hypothesis is not existentially quantified".
Tactic Notation "mlDestructExManual" constr(name') "as" constr(x) :=
_mlDestructExManual name' x.
Tactic Notation "mlDestructEx" constr(name') "as" ident(x) :=
(* tryif is_var x (* we need to check whether x is a used ident! *)
then
_mlDestructExManual name' x (* Do not use idtac here, because it breaks tryif for some reason *)
else *)
_mlDestructExFresh name' x (* Do not use idtac here, because it breaks tryif for some reason *)
.
(* Ltac mlDestructEx name' x :=
tryif
match type of x with
| evar => idtac
| _ => fail 1
end
then _mlDestructExManual name' as x
else _mlDestructExFresh name' as x
. *)
Local Lemma destructExDouble_Test {Σ : Signature} Γ ϕ ψ :
well_formed (ex, ϕ) → well_formed (ex, ψ) →
Γ ⊢ (ex, ϕ and ψ) ---> (ex, ϕ and ψ) ---> ex, ϕ.
Local Lemma destructEx_Test {Σ : Signature} Γ ϕ ψ :
well_formed (ex, ϕ) → well_formed (ex, ψ) →
Γ ⊢ (ex, ϕ and ψ) ---> ex, ϕ.
This page has been generated by coqdoc