File BasicProofSystemLemmas
From MatchingLogic Require Export Logic.
Import Logic.Notations.
Lemma MP {Σ : Signature} {Γ : Theory} {ϕ₁ ϕ₂ : Pattern} {i : ProofInfo} :
Γ ⊢i ϕ₁ using i →
Γ ⊢i (ϕ₁ ---> ϕ₂) using i →
Γ ⊢i ϕ₂ using i.
Lemma P1 {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed ϕ →
well_formed ψ →
Γ ⊢i ϕ ---> ψ ---> ϕ
using BasicReasoning.
Lemma P2 {Σ : Signature} (Γ : Theory) (ϕ ψ ξ : Pattern) :
well_formed ϕ →
well_formed ψ →
well_formed ξ →
Γ ⊢i (ϕ ---> ψ ---> ξ) ---> (ϕ ---> ψ) ---> (ϕ ---> ξ)
using BasicReasoning.
Lemma P3 {Σ : Signature} (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i (((ϕ ---> ⊥) ---> ⊥) ---> ϕ)
using BasicReasoning.
Lemma A_impl_A {Σ : Signature} (Γ : Theory) (A : Pattern) :
(well_formed A) →
Γ ⊢i (A ---> A)
using BasicReasoning.
Lemma prf_add_assumption {Σ : Signature} Γ a b i :
well_formed a →
well_formed b →
Γ ⊢i b using i →
Γ ⊢i (a ---> b) using i.
Lemma hypothesis {Σ : Signature} (Γ : Theory) (axiom : Pattern) :
well_formed axiom →
(axiom ∈ Γ) →
Γ ⊢i axiom
using BasicReasoning.
Arguments P1 {Σ} _ (_%_ml) (_%_ml) _ _ .
Arguments P2 {Σ} _ (_%_ml) (_%_ml) (_%_ml) _ _ _.
Arguments P3 {Σ} _ (_%_ml) _.
Lemma P4m {Σ : Signature}(Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((A ---> !B) ---> !A))
using BasicReasoning.
Lemma P4i {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i ((A ---> !A) ---> !A)
using BasicReasoning.
Lemma reorder {Σ : Signature} (Γ : Theory) (A B C : Pattern) :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i ((A ---> B ---> C) ---> ( B ---> A ---> C))
using BasicReasoning.
Lemma reorder_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A ---> B ---> C) using i →
Γ ⊢i (B ---> A ---> C) using i.
Lemma syllogism {Σ : Signature} (Γ : Theory) (A B C : Pattern) :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i ((A ---> B) ---> (B ---> C) ---> (A ---> C))
using BasicReasoning.
Lemma syllogism_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (B ---> C) using i →
Γ ⊢i (A ---> C) using i.
Lemma modus_ponens {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (A ---> B) ---> B)
using BasicReasoning.
Lemma not_not_intro {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (A ---> !(!A))
using BasicReasoning.
Lemma P4 {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (((! A) ---> (! B)) ---> (B ---> A))
using BasicReasoning.
Lemma conj_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> B ---> (A and B))
using BasicReasoning.
Lemma conj_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A using i →
Γ ⊢i B using i →
Γ ⊢i (A and B) using i.
Lemma syllogism_4_meta {Σ : Signature} (Γ : Theory) (A B C D : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed C →
well_formed D →
Γ ⊢i (A ---> B ---> C) using i →
Γ ⊢i (C ---> D) using i →
Γ ⊢i (A ---> B ---> D) using i.
Lemma bot_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (⊥ ---> A)
using BasicReasoning.
Lemma modus_ponens' {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (!B ---> !A) ---> B)
using BasicReasoning.
Lemma disj_right_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (B ---> (A or B))
using BasicReasoning.
Lemma disj_left_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (A or B))
using BasicReasoning.
Lemma disj_right_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i B using i →
Γ ⊢i (A or B) using i.
Lemma disj_left_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A using i →
Γ ⊢i (A or B) using i.
Lemma not_not_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (!(!A) ---> A)
using BasicReasoning.
Lemma not_not_elim_meta {Σ : Signature} Γ A (i : ProofInfo) :
well_formed A →
Γ ⊢i (! ! A) using i →
Γ ⊢i A using i.
Lemma double_neg_elim {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (((!(!A)) ---> (!(!B))) ---> (A ---> B))
using BasicReasoning.
Lemma double_neg_elim_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i ((!(!A)) ---> (!(!B))) using i →
Γ ⊢i (A ---> B) using i.
Lemma not_not_impl_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((! ! A) ---> (! ! B)))
using BasicReasoning.
Lemma contraposition {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((! B) ---> (! A)))
using BasicReasoning.
Lemma or_comm_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo):
well_formed A →
well_formed B →
Γ ⊢i (A or B) using i →
Γ ⊢i (B or A) using i.
Lemma A_implies_not_not_A_alt {Σ : Signature} (Γ : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (!( !A )) using i.
Lemma P5i {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (! A ---> (A ---> B))
using BasicReasoning.
Lemma A_implies_not_not_A_alt_Γ {Σ : Signature} (Γ : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (!( !A )) using i.
Lemma exclusion {Σ : Signature} (G : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
G ⊢i A using i →
G ⊢i (A ---> ⊥) using i →
G ⊢i ⊥ using i.
Lemma modus_tollens {Σ : Signature} Γ A B (i : ProofInfo) :
Γ ⊢i (A ---> B) using i →
Γ ⊢i (!B ---> !A) using i.
Lemma A_impl_not_not_B {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> ! !B) ---> (A ---> B))
using BasicReasoning.
Lemma prf_weaken_conclusion {Σ : Signature} Γ A B B' :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i ((B ---> B') ---> ((A ---> B) ---> (A ---> B')))
using BasicReasoning.
Lemma prf_weaken_conclusion_meta {Σ : Signature} Γ A B B' (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i (B ---> B') using i →
Γ ⊢i ((A ---> B) ---> (A ---> B')) using i.
Lemma prf_weaken_conclusion_iter {Σ : Signature} Γ l g g'
(wfl : Pattern.wf l) (wfg : well_formed g) (wfg' : well_formed g') :
Γ ⊢i ((g ---> g') ---> (fold_right patt_imp g l ---> fold_right patt_imp g' l))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (g ---> g') using i →
Γ ⊢i ((fold_right patt_imp g l) ---> (fold_right patt_imp g' l)) using i.
Lemma prf_weaken_conclusion_iter_meta_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (g ---> g') using i →
Γ ⊢i (fold_right patt_imp g l) using i →
Γ ⊢i (fold_right patt_imp g' l) using i.
Lemma prf_weaken_conclusion_meta_meta {Σ : Signature} Γ A B B' (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i (B ---> B') using i →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (A ---> B') using i.
Lemma prf_strenghten_premise {Σ : Signature} Γ A A' B :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i ((A' ---> A) ---> ((A ---> B) ---> (A' ---> B))) using BasicReasoning.
Lemma prf_strenghten_premise_iter {Σ : Signature} Γ l₁ l₂ h h' g :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) --->
foldr patt_imp g (l₁ ++ h::l₂) --->
foldr patt_imp g (l₁ ++ h'::l₂)
using BasicReasoning.
Lemma prf_strenghten_premise_meta {Σ : Signature} Γ A A' B (i : ProofInfo) :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i (A' ---> A) using i →
Γ ⊢i ((A ---> B) ---> (A' ---> B)) using i.
Lemma prf_strenghten_premise_meta_meta {Σ : Signature} Γ A A' B (i : ProofInfo) :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i (A' ---> A) using i →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (A' ---> B) using i.
Lemma prf_strenghten_premise_iter_meta {Σ : Signature} Γ l₁ l₂ h h' g (i : ProofInfo) :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h::l₂) --->
foldr patt_imp g (l₁ ++ h'::l₂)
using i.
Lemma prf_strenghten_premise_iter_meta_meta {Σ : Signature} Γ l₁ l₂ h h' g (i : ProofInfo) :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h::l₂) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h'::l₂) using i.
Local Example example_nested_const {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
(* like P2 but nested a bit *)
Γ ⊢i (a ---> (b ---> (c ---> a)))
using BasicReasoning.
(* This will form a base for the tactic 'exact 0' *)
Lemma nested_const {Σ : Signature} Γ a l:
well_formed a →
Pattern.wf l →
Γ ⊢i (a ---> (fold_right patt_imp a l))
using BasicReasoning.
Lemma nested_const_middle {Σ : Signature} Γ a l₁ l₂:
well_formed a →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i (fold_right patt_imp a (l₁ ++ a :: l₂))
using BasicReasoning.
Lemma prf_reorder_iter {Σ : Signature} Γ a b g l₁ l₂:
well_formed a →
well_formed b →
well_formed g →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i ((fold_right patt_imp g (l₁ ++ [a;b] ++ l₂)) --->
(fold_right patt_imp g (l₁ ++ [b;a] ++ l₂)))
using BasicReasoning.
Lemma prf_reorder_iter_meta {Σ : Signature} Γ a b g l₁ l₂ (i : ProofInfo):
well_formed a →
well_formed b →
well_formed g →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i (fold_right patt_imp g (l₁ ++ [a;b] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp g (l₁ ++ [b;a] ++ l₂)) using i.
(* NOTE: this should hold, but because of the proof system being in Set,
it is not straightforward to prove. *)
Lemma reorder_iter_perm {Σ : Signature} Γ ϕ l₁ l₂:
well_formed ϕ → Pattern.wf l₁ → Pattern.wf l₂ →
l₁ ⊆ l₂ →
Γ ⊢i foldr patt_imp ϕ l₁ ---> foldr patt_imp ϕ l₂ using BasicReasoning.
Lemma reorder_head_to_middle {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x :: l2) ---> foldr patt_imp g (x :: l1 ++ l2)
using BasicReasoning.
Lemma reorder_head_to_middle_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x :: l2) using i →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) using i.
Lemma reorder_middle_to_head {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) ---> foldr patt_imp g (l1 ++ x::l2)
using BasicReasoning.
Corollary reorder_middle_to_head_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) using i →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i.
Corollary reorder_last_to_middle {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) ---> foldr patt_imp g (l1 ++ l2 ++ [x])
using BasicReasoning.
Corollary reorder_last_to_middle_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) using i.
Corollary reorder_middle_to_last {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) ---> foldr patt_imp g (l1 ++ x::l2)
using BasicReasoning.
Corollary reorder_middle_to_last_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) using i →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i.
Corollary reorder_head_to_last {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (g x : Pattern) ,
Pattern.wf l → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l ++ [x]) ---> foldr patt_imp g (x :: l)
using BasicReasoning.
Corollary reorder_head_to_last_meta {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (g x : Pattern) i,
Pattern.wf l → well_formed g → well_formed x
→ Γ ⊢i foldr patt_imp g (l ++ [x]) using i
→ Γ ⊢i foldr patt_imp g (x :: l) using i.
Lemma A_impl_not_not_B_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A ---> ! !B using i →
Γ ⊢i A ---> B using i.
Lemma pf_conj_elim_l {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i A and B ---> A using BasicReasoning.
Lemma pf_conj_elim_r {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i A and B ---> B using BasicReasoning.
Lemma pf_conj_elim_l_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A and B using i →
Γ ⊢i A using i.
Lemma pf_conj_elim_r_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A and B using i →
Γ ⊢i B using i.
Lemma A_or_notA {Σ : Signature} Γ A :
well_formed A →
Γ ⊢i A or ! A using BasicReasoning.
Lemma P4m_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A ---> B using i →
Γ ⊢i A ---> !B using i →
Γ ⊢i !A using i.
(*
Γ ⊢ φ₁ → φ₂
-------------------- (x ∉ FV(φ₂))
Γ ⊢ (∃x. φ₁) → φ₂
*)
Lemma Ex_gen {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ : Pattern) (x : evar) (i : ProofInfo)
{pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i} :
x ∉ free_evars ϕ₂ →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁ ---> ϕ₂) using i.
(*
Γ ⊢ φy/x → ∃x. φ
*)
Lemma Ex_quan {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (y : evar) :
well_formed (patt_exists ϕ) →
Γ ⊢i (instantiate (patt_exists ϕ) (patt_free_evar y) ---> (patt_exists ϕ))
using BasicReasoning.
(*
Γ ⊢ φ
--------------
Γ ⊢ ∀x. φ
*)
Lemma universal_generalization {Σ : Signature} Γ ϕ 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.
Lemma ex_quan_monotone {Σ : Signature} Γ 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.
Definition forall_quantify {Σ : Signature} x p : Pattern
:= all, p^{{evar:x↦0}}.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∀x. φ₁) → (∀x. φ₂)
*)
Lemma all_quan_monotone {Σ : Signature} Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i) :
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (forall_quantify x ϕ₁) ---> (forall_quantify x ϕ₂) using i.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∀x. φ₁) → (∀x. φ₂)
*)
Lemma forall_monotone {Σ : Signature} Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i) :
x ∉ free_evars ϕ₁ →
x ∉ free_evars ϕ₂ →
Γ ⊢i (evar_open x 0 ϕ₁) ---> (evar_open x 0 ϕ₂) using i →
Γ ⊢i (patt_forall ϕ₁) ---> (patt_forall ϕ₂) using i.
(*
This is basically universal_generalization
but under an implication.
Γ ⊢ φ → ψ
-------------
Γ ⊢ φ → ∀x. ψ
I wonder if we could get an iterative version forall_gen_iter?
Like,
Γ ⊢ φ₁ → ... → φₖ → ψ
----------------------------
Γ ⊢ φ₁ → ... → φₖ → ∀x. ψ
*)
Lemma forall_gen {Σ : Signature} Γ ϕ₁ ϕ₂ x (i : ProofInfo):
evar_is_fresh_in x ϕ₁ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ---> forall_quantify x ϕ₂ using i.
Lemma Framing_left {Σ : Signature}(Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) (i : ProofInfo)
(wfψ : well_formed ψ)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ⋅ ψ ---> ϕ₂ ⋅ ψ using i.
Lemma Framing_right {Σ : Signature}(Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) (i : ProofInfo)
(wfψ : well_formed ψ)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ψ ⋅ ϕ₁ ---> ψ ⋅ ϕ₂ using i.
Lemma Knaster_tarski {Σ : Signature}
(Γ : Theory) (ϕ ψ : Pattern) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := ∅;
pi_substituted_svars := ∅;
pi_uses_kt := true ;
pi_uses_advanced_kt := ~~ bound_svar_is_banned_under_mus ϕ 0 0 ; (* TODO depends on ϕ*)
|}) i} :
well_formed (mu, ϕ) →
Γ ⊢i (instantiate (mu, ϕ) ψ) ---> ψ using i →
Γ ⊢i (mu, ϕ) ---> ψ using i.
Lemma Svar_subst {Σ : Signature}
(Γ : Theory) (ϕ ψ : Pattern) (X : svar) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := ∅;
pi_substituted_svars := {[X]};
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}) i} :
well_formed ψ →
Γ ⊢i ϕ using i →
Γ ⊢i (ϕ^[[svar: X ↦ ψ]]) using i.
Lemma Pre_fixp {Σ : Signature}
(Γ : Theory) (ϕ : Pattern) :
well_formed (patt_mu ϕ) →
Γ ⊢i (instantiate (patt_mu ϕ) (patt_mu ϕ) ---> (patt_mu ϕ))
using BasicReasoning.
Lemma extend_theory {Σ : Signature} (Γ Γ' : Theory) φ i:
Γ ⊆ Γ' →
Γ ⊢i φ using i →
Γ' ⊢i φ using i.
Import Logic.Notations.
Lemma MP {Σ : Signature} {Γ : Theory} {ϕ₁ ϕ₂ : Pattern} {i : ProofInfo} :
Γ ⊢i ϕ₁ using i →
Γ ⊢i (ϕ₁ ---> ϕ₂) using i →
Γ ⊢i ϕ₂ using i.
Lemma P1 {Σ : Signature} (Γ : Theory) (ϕ ψ : Pattern) :
well_formed ϕ →
well_formed ψ →
Γ ⊢i ϕ ---> ψ ---> ϕ
using BasicReasoning.
Lemma P2 {Σ : Signature} (Γ : Theory) (ϕ ψ ξ : Pattern) :
well_formed ϕ →
well_formed ψ →
well_formed ξ →
Γ ⊢i (ϕ ---> ψ ---> ξ) ---> (ϕ ---> ψ) ---> (ϕ ---> ξ)
using BasicReasoning.
Lemma P3 {Σ : Signature} (Γ : Theory) (ϕ : Pattern) :
well_formed ϕ →
Γ ⊢i (((ϕ ---> ⊥) ---> ⊥) ---> ϕ)
using BasicReasoning.
Lemma A_impl_A {Σ : Signature} (Γ : Theory) (A : Pattern) :
(well_formed A) →
Γ ⊢i (A ---> A)
using BasicReasoning.
Lemma prf_add_assumption {Σ : Signature} Γ a b i :
well_formed a →
well_formed b →
Γ ⊢i b using i →
Γ ⊢i (a ---> b) using i.
Lemma hypothesis {Σ : Signature} (Γ : Theory) (axiom : Pattern) :
well_formed axiom →
(axiom ∈ Γ) →
Γ ⊢i axiom
using BasicReasoning.
Arguments P1 {Σ} _ (_%_ml) (_%_ml) _ _ .
Arguments P2 {Σ} _ (_%_ml) (_%_ml) (_%_ml) _ _ _.
Arguments P3 {Σ} _ (_%_ml) _.
Lemma P4m {Σ : Signature}(Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((A ---> !B) ---> !A))
using BasicReasoning.
Lemma P4i {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i ((A ---> !A) ---> !A)
using BasicReasoning.
Lemma reorder {Σ : Signature} (Γ : Theory) (A B C : Pattern) :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i ((A ---> B ---> C) ---> ( B ---> A ---> C))
using BasicReasoning.
Lemma reorder_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A ---> B ---> C) using i →
Γ ⊢i (B ---> A ---> C) using i.
Lemma syllogism {Σ : Signature} (Γ : Theory) (A B C : Pattern) :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i ((A ---> B) ---> (B ---> C) ---> (A ---> C))
using BasicReasoning.
Lemma syllogism_meta {Σ : Signature} {Γ : Theory} {A B C : Pattern} {i : ProofInfo} :
well_formed A →
well_formed B →
well_formed C →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (B ---> C) using i →
Γ ⊢i (A ---> C) using i.
Lemma modus_ponens {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (A ---> B) ---> B)
using BasicReasoning.
Lemma not_not_intro {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (A ---> !(!A))
using BasicReasoning.
Lemma P4 {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (((! A) ---> (! B)) ---> (B ---> A))
using BasicReasoning.
Lemma conj_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> B ---> (A and B))
using BasicReasoning.
Lemma conj_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A using i →
Γ ⊢i B using i →
Γ ⊢i (A and B) using i.
Lemma syllogism_4_meta {Σ : Signature} (Γ : Theory) (A B C D : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed C →
well_formed D →
Γ ⊢i (A ---> B ---> C) using i →
Γ ⊢i (C ---> D) using i →
Γ ⊢i (A ---> B ---> D) using i.
Lemma bot_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (⊥ ---> A)
using BasicReasoning.
Lemma modus_ponens' {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (!B ---> !A) ---> B)
using BasicReasoning.
Lemma disj_right_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (B ---> (A or B))
using BasicReasoning.
Lemma disj_left_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (A ---> (A or B))
using BasicReasoning.
Lemma disj_right_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i B using i →
Γ ⊢i (A or B) using i.
Lemma disj_left_intro_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A using i →
Γ ⊢i (A or B) using i.
Lemma not_not_elim {Σ : Signature} (Γ : Theory) (A : Pattern) :
well_formed A →
Γ ⊢i (!(!A) ---> A)
using BasicReasoning.
Lemma not_not_elim_meta {Σ : Signature} Γ A (i : ProofInfo) :
well_formed A →
Γ ⊢i (! ! A) using i →
Γ ⊢i A using i.
Lemma double_neg_elim {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (((!(!A)) ---> (!(!B))) ---> (A ---> B))
using BasicReasoning.
Lemma double_neg_elim_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i ((!(!A)) ---> (!(!B))) using i →
Γ ⊢i (A ---> B) using i.
Lemma not_not_impl_intro {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((! ! A) ---> (! ! B)))
using BasicReasoning.
Lemma contraposition {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> B) ---> ((! B) ---> (! A)))
using BasicReasoning.
Lemma or_comm_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo):
well_formed A →
well_formed B →
Γ ⊢i (A or B) using i →
Γ ⊢i (B or A) using i.
Lemma A_implies_not_not_A_alt {Σ : Signature} (Γ : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (!( !A )) using i.
Lemma P5i {Σ : Signature} (Γ : Theory) (A B : Pattern) :
well_formed A →
well_formed B →
Γ ⊢i (! A ---> (A ---> B))
using BasicReasoning.
Lemma A_implies_not_not_A_alt_Γ {Σ : Signature} (Γ : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
Γ ⊢i A using i →
Γ ⊢i (!( !A )) using i.
Lemma exclusion {Σ : Signature} (G : Theory) (A : Pattern) (i : ProofInfo) :
well_formed A →
G ⊢i A using i →
G ⊢i (A ---> ⊥) using i →
G ⊢i ⊥ using i.
Lemma modus_tollens {Σ : Signature} Γ A B (i : ProofInfo) :
Γ ⊢i (A ---> B) using i →
Γ ⊢i (!B ---> !A) using i.
Lemma A_impl_not_not_B {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i ((A ---> ! !B) ---> (A ---> B))
using BasicReasoning.
Lemma prf_weaken_conclusion {Σ : Signature} Γ A B B' :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i ((B ---> B') ---> ((A ---> B) ---> (A ---> B')))
using BasicReasoning.
Lemma prf_weaken_conclusion_meta {Σ : Signature} Γ A B B' (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i (B ---> B') using i →
Γ ⊢i ((A ---> B) ---> (A ---> B')) using i.
Lemma prf_weaken_conclusion_iter {Σ : Signature} Γ l g g'
(wfl : Pattern.wf l) (wfg : well_formed g) (wfg' : well_formed g') :
Γ ⊢i ((g ---> g') ---> (fold_right patt_imp g l ---> fold_right patt_imp g' l))
using BasicReasoning.
Lemma prf_weaken_conclusion_iter_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (g ---> g') using i →
Γ ⊢i ((fold_right patt_imp g l) ---> (fold_right patt_imp g' l)) using i.
Lemma prf_weaken_conclusion_iter_meta_meta {Σ : Signature} Γ l g g' (i : ProofInfo):
Pattern.wf l →
well_formed g →
well_formed g' →
Γ ⊢i (g ---> g') using i →
Γ ⊢i (fold_right patt_imp g l) using i →
Γ ⊢i (fold_right patt_imp g' l) using i.
Lemma prf_weaken_conclusion_meta_meta {Σ : Signature} Γ A B B' (i : ProofInfo) :
well_formed A →
well_formed B →
well_formed B' →
Γ ⊢i (B ---> B') using i →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (A ---> B') using i.
Lemma prf_strenghten_premise {Σ : Signature} Γ A A' B :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i ((A' ---> A) ---> ((A ---> B) ---> (A' ---> B))) using BasicReasoning.
Lemma prf_strenghten_premise_iter {Σ : Signature} Γ l₁ l₂ h h' g :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) --->
foldr patt_imp g (l₁ ++ h::l₂) --->
foldr patt_imp g (l₁ ++ h'::l₂)
using BasicReasoning.
Lemma prf_strenghten_premise_meta {Σ : Signature} Γ A A' B (i : ProofInfo) :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i (A' ---> A) using i →
Γ ⊢i ((A ---> B) ---> (A' ---> B)) using i.
Lemma prf_strenghten_premise_meta_meta {Σ : Signature} Γ A A' B (i : ProofInfo) :
well_formed A →
well_formed A' →
well_formed B →
Γ ⊢i (A' ---> A) using i →
Γ ⊢i (A ---> B) using i →
Γ ⊢i (A' ---> B) using i.
Lemma prf_strenghten_premise_iter_meta {Σ : Signature} Γ l₁ l₂ h h' g (i : ProofInfo) :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h::l₂) --->
foldr patt_imp g (l₁ ++ h'::l₂)
using i.
Lemma prf_strenghten_premise_iter_meta_meta {Σ : Signature} Γ l₁ l₂ h h' g (i : ProofInfo) :
Pattern.wf l₁ → Pattern.wf l₂ →
well_formed h →
well_formed h' →
well_formed g →
Γ ⊢i (h' ---> h) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h::l₂) using i →
Γ ⊢i foldr patt_imp g (l₁ ++ h'::l₂) using i.
Local Example example_nested_const {Σ : Signature} Γ a b c:
well_formed a →
well_formed b →
well_formed c →
(* like P2 but nested a bit *)
Γ ⊢i (a ---> (b ---> (c ---> a)))
using BasicReasoning.
(* This will form a base for the tactic 'exact 0' *)
Lemma nested_const {Σ : Signature} Γ a l:
well_formed a →
Pattern.wf l →
Γ ⊢i (a ---> (fold_right patt_imp a l))
using BasicReasoning.
Lemma nested_const_middle {Σ : Signature} Γ a l₁ l₂:
well_formed a →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i (fold_right patt_imp a (l₁ ++ a :: l₂))
using BasicReasoning.
Lemma prf_reorder_iter {Σ : Signature} Γ a b g l₁ l₂:
well_formed a →
well_formed b →
well_formed g →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i ((fold_right patt_imp g (l₁ ++ [a;b] ++ l₂)) --->
(fold_right patt_imp g (l₁ ++ [b;a] ++ l₂)))
using BasicReasoning.
Lemma prf_reorder_iter_meta {Σ : Signature} Γ a b g l₁ l₂ (i : ProofInfo):
well_formed a →
well_formed b →
well_formed g →
Pattern.wf l₁ →
Pattern.wf l₂ →
Γ ⊢i (fold_right patt_imp g (l₁ ++ [a;b] ++ l₂)) using i →
Γ ⊢i (fold_right patt_imp g (l₁ ++ [b;a] ++ l₂)) using i.
(* NOTE: this should hold, but because of the proof system being in Set,
it is not straightforward to prove. *)
Lemma reorder_iter_perm {Σ : Signature} Γ ϕ l₁ l₂:
well_formed ϕ → Pattern.wf l₁ → Pattern.wf l₂ →
l₁ ⊆ l₂ →
Γ ⊢i foldr patt_imp ϕ l₁ ---> foldr patt_imp ϕ l₂ using BasicReasoning.
Lemma reorder_head_to_middle {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x :: l2) ---> foldr patt_imp g (x :: l1 ++ l2)
using BasicReasoning.
Lemma reorder_head_to_middle_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x :: l2) using i →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) using i.
Lemma reorder_middle_to_head {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) ---> foldr patt_imp g (l1 ++ x::l2)
using BasicReasoning.
Corollary reorder_middle_to_head_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (x :: l1 ++ l2) using i →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i.
Corollary reorder_last_to_middle {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) ---> foldr patt_imp g (l1 ++ l2 ++ [x])
using BasicReasoning.
Corollary reorder_last_to_middle_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) using i.
Corollary reorder_middle_to_last {Σ : Signature} (Γ : Theory) :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) ---> foldr patt_imp g (l1 ++ x::l2)
using BasicReasoning.
Corollary reorder_middle_to_last_meta {Σ : Signature} (Γ : Theory) i :
∀ (l1 l2 : list Pattern) (g x : Pattern) ,
Pattern.wf l1 → Pattern.wf l2 → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l1 ++ l2 ++ [x]) using i →
Γ ⊢i foldr patt_imp g (l1 ++ x::l2) using i.
Corollary reorder_head_to_last {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (g x : Pattern) ,
Pattern.wf l → well_formed g → well_formed x →
Γ ⊢i foldr patt_imp g (l ++ [x]) ---> foldr patt_imp g (x :: l)
using BasicReasoning.
Corollary reorder_head_to_last_meta {Σ : Signature} (Γ : Theory) :
∀ (l : list Pattern) (g x : Pattern) i,
Pattern.wf l → well_formed g → well_formed x
→ Γ ⊢i foldr patt_imp g (l ++ [x]) using i
→ Γ ⊢i foldr patt_imp g (x :: l) using i.
Lemma A_impl_not_not_B_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A ---> ! !B using i →
Γ ⊢i A ---> B using i.
Lemma pf_conj_elim_l {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i A and B ---> A using BasicReasoning.
Lemma pf_conj_elim_r {Σ : Signature} Γ A B :
well_formed A →
well_formed B →
Γ ⊢i A and B ---> B using BasicReasoning.
Lemma pf_conj_elim_l_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A and B using i →
Γ ⊢i A using i.
Lemma pf_conj_elim_r_meta {Σ : Signature} Γ A B (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A and B using i →
Γ ⊢i B using i.
Lemma A_or_notA {Σ : Signature} Γ A :
well_formed A →
Γ ⊢i A or ! A using BasicReasoning.
Lemma P4m_meta {Σ : Signature} (Γ : Theory) (A B : Pattern) (i : ProofInfo) :
well_formed A →
well_formed B →
Γ ⊢i A ---> B using i →
Γ ⊢i A ---> !B using i →
Γ ⊢i !A using i.
(*
Γ ⊢ φ₁ → φ₂
-------------------- (x ∉ FV(φ₂))
Γ ⊢ (∃x. φ₁) → φ₂
*)
Lemma Ex_gen {Σ : Signature} (Γ : Theory) (ϕ₁ ϕ₂ : Pattern) (x : evar) (i : ProofInfo)
{pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i} :
x ∉ free_evars ϕ₂ →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (exists_quantify x ϕ₁ ---> ϕ₂) using i.
(*
Γ ⊢ φy/x → ∃x. φ
*)
Lemma Ex_quan {Σ : Signature} (Γ : Theory) (ϕ : Pattern) (y : evar) :
well_formed (patt_exists ϕ) →
Γ ⊢i (instantiate (patt_exists ϕ) (patt_free_evar y) ---> (patt_exists ϕ))
using BasicReasoning.
(*
Γ ⊢ φ
--------------
Γ ⊢ ∀x. φ
*)
Lemma universal_generalization {Σ : Signature} Γ ϕ 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.
Lemma ex_quan_monotone {Σ : Signature} Γ 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.
Definition forall_quantify {Σ : Signature} x p : Pattern
:= all, p^{{evar:x↦0}}.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∀x. φ₁) → (∀x. φ₂)
*)
Lemma all_quan_monotone {Σ : Signature} Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i) :
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i (forall_quantify x ϕ₁) ---> (forall_quantify x ϕ₂) using i.
(*
Γ ⊢ φ₁ → φ₂
-----------------------
Γ ⊢ (∀x. φ₁) → (∀x. φ₂)
*)
Lemma forall_monotone {Σ : Signature} Γ x ϕ₁ ϕ₂ (i : ProofInfo)
(pile : ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i) :
x ∉ free_evars ϕ₁ →
x ∉ free_evars ϕ₂ →
Γ ⊢i (evar_open x 0 ϕ₁) ---> (evar_open x 0 ϕ₂) using i →
Γ ⊢i (patt_forall ϕ₁) ---> (patt_forall ϕ₂) using i.
(*
This is basically universal_generalization
but under an implication.
Γ ⊢ φ → ψ
-------------
Γ ⊢ φ → ∀x. ψ
I wonder if we could get an iterative version forall_gen_iter?
Like,
Γ ⊢ φ₁ → ... → φₖ → ψ
----------------------------
Γ ⊢ φ₁ → ... → φₖ → ∀x. ψ
*)
Lemma forall_gen {Σ : Signature} Γ ϕ₁ ϕ₂ x (i : ProofInfo):
evar_is_fresh_in x ϕ₁ →
ProofInfoLe (ExGen := {[x]}, SVSubst := ∅, KT := false, AKT := false) i →
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ---> forall_quantify x ϕ₂ using i.
Lemma Framing_left {Σ : Signature}(Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) (i : ProofInfo)
(wfψ : well_formed ψ)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ϕ₁ ⋅ ψ ---> ϕ₂ ⋅ ψ using i.
Lemma Framing_right {Σ : Signature}(Γ : Theory) (ϕ₁ ϕ₂ ψ : Pattern) (i : ProofInfo)
(wfψ : well_formed ψ)
{pile : ProofInfoLe ((ExGen := ∅, SVSubst := ∅, KT := false, AKT := false)) i}
:
Γ ⊢i ϕ₁ ---> ϕ₂ using i →
Γ ⊢i ψ ⋅ ϕ₁ ---> ψ ⋅ ϕ₂ using i.
Lemma Knaster_tarski {Σ : Signature}
(Γ : Theory) (ϕ ψ : Pattern) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := ∅;
pi_substituted_svars := ∅;
pi_uses_kt := true ;
pi_uses_advanced_kt := ~~ bound_svar_is_banned_under_mus ϕ 0 0 ; (* TODO depends on ϕ*)
|}) i} :
well_formed (mu, ϕ) →
Γ ⊢i (instantiate (mu, ϕ) ψ) ---> ψ using i →
Γ ⊢i (mu, ϕ) ---> ψ using i.
Lemma Svar_subst {Σ : Signature}
(Γ : Theory) (ϕ ψ : Pattern) (X : svar) (i : ProofInfo)
{pile : ProofInfoLe (
{| pi_generalized_evars := ∅;
pi_substituted_svars := {[X]};
pi_uses_kt := false ;
pi_uses_advanced_kt := false ;
|}) i} :
well_formed ψ →
Γ ⊢i ϕ using i →
Γ ⊢i (ϕ^[[svar: X ↦ ψ]]) using i.
Lemma Pre_fixp {Σ : Signature}
(Γ : Theory) (ϕ : Pattern) :
well_formed (patt_mu ϕ) →
Γ ⊢i (instantiate (patt_mu ϕ) (patt_mu ϕ) ---> (patt_mu ϕ))
using BasicReasoning.
Lemma extend_theory {Σ : Signature} (Γ Γ' : Theory) φ i:
Γ ⊆ Γ' →
Γ ⊢i φ using i →
Γ' ⊢i φ using i.
This page has been generated by coqdoc