File PrePredicate
From MatchingLogic Require Export Semantics.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Inductive closure_increasing : (list (prod db_index evar)) → Prop :=
| ci_nil : closure_increasing []
| ci_single
(k0 : db_index)
(x0 : evar) :
closure_increasing [(k0,x0)]
| ci_cons
(k0 k1 : db_index)
(x0 x1 : evar)
(l : list (prod db_index evar)) :
k0 ≤ k1 →
closure_increasing ((k1,x1)::l) →
closure_increasing ((k0,x0)::(k1,x1)::l)
.
Definition M_pre_pre_predicate (k : db_index) (M : Model) (ϕ : Pattern) : Prop :=
∀ (l : list (prod db_index evar)),
Forall (λ p, p.1 ≤ k) l →
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
M_predicate M (bcmcloseex l ϕ).
Lemma pre_predicate_S (k : db_index) (M : Model) (ϕ : Pattern) :
M_pre_pre_predicate (S k) M ϕ →
M_pre_pre_predicate k M ϕ.
Definition closing_list_weight (l : list (prod db_index evar)) : nat :=
sum_list_with fst l.
Lemma drop_weight (dummy_x : evar) (idx : nat) (l : list (prod db_index evar)) :
closing_list_weight l ≥ closing_list_weight (drop idx l).
Lemma closure_increasing_map_pred
(l : list (prod db_index evar))
:
Forall (λ p, p.1 > 0) l →
closure_increasing l →
closure_increasing (map (λ p, (Nat.pred p.1, p.2)) l).
Lemma closure_increasing_map_S
(l : list (prod db_index evar))
:
closure_increasing l →
closure_increasing (map (λ p, (S p.1, p.2)) l).
Definition lower_closing_list (x : evar) (l : list (prod db_index evar))
:= (0,x)::(map (λ p, (Nat.pred p.1, p.2)) l).
Lemma closure_increasing_lower_closing_list
(dummy_x : evar)
(l : list (prod db_index evar))
:
closure_increasing l →
closure_increasing (lower_closing_list dummy_x l).
Lemma lower_closing_list_weight (x : evar) (l : list (prod db_index evar)) :
closing_list_weight l ≥ closing_list_weight (lower_closing_list x l).
Lemma lower_closing_list_same
(x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
bevar_occur ϕ 0 = false →
Forall (λ p, p.1 > 0) l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
bcmcloseex (lower_closing_list x l) ϕ = bcmcloseex l ϕ.
(*
Fixpoint lower_closing_list_iter (k : nat) (x : evar) (l : list (prod db_index evar))
:=
match k with
| 0 => l
| (S k') => lower_closing_list_iter k' x (lower_closing_list x l)
end.
Lemma lower_closing_list_iter_same
{Σ : Signature}
(k : nat)
(x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
bcmcloseex (lower_closing_list_iter k x l) ϕ = bcmcloseex l ϕ.
Proof. Abort.
*)
Lemma list_find_dep {A} P `{∀ x, Decision (P x)} (l : list A) :
({p : (nat×A)%type & (l !! p.1 = Some p.2 ∧ P p.2 ∧ ∀ j y, l !! j = Some y → j < p.1 → ¬P y) }
+ (Forall (λ x, ¬P x) l))%type.
Equations? make_zero_list
(dummy_x : evar)
(l : list (prod db_index evar))
: (list (prod db_index evar))
by wf (closing_list_weight l) lt
:=
make_zero_list dummy_x l
with (@list_find_dep _ (λ p, p.1 ≠ 0) _ l) ⇒ {
| inr _ ⇒ l
| inl (existT p pf) ⇒
let idx := p.1 in
(firstn idx l) ++ (make_zero_list dummy_x (lower_closing_list dummy_x (skipn idx l)))
}.
Lemma make_zero_list_zeroes (dummy_x : evar) (l : list (prod db_index evar)) :
(Forall (λ p, p.1 = 0) (make_zero_list dummy_x l)).
Lemma closure_increasing_app_proj1
(l₁ l₂ : list (prod db_index evar))
:
closure_increasing (l₁ ++ l₂) →
closure_increasing l₁.
Lemma closure_increasing_app_proj2
(l₁ l₂ : list (prod db_index evar))
:
closure_increasing (l₁ ++ l₂) →
closure_increasing l₂.
Lemma wfc_ex_aux_evar_open_change_evar x x' dbi ϕ:
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) dbi =
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x'}) dbi.
Lemma wfcexaux_bcmcloseex_evar_open_change_evar l x x' dbi dbi' ϕ:
well_formed_closed_ex_aux (bcmcloseex l (ϕ^{evar: dbi ↦ x})) dbi'
= well_formed_closed_ex_aux (bcmcloseex l (ϕ^{evar: dbi ↦ x'})) dbi'.
Lemma wfcexaux_bcmcloseex_lower_closing_list
(dummy_x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 = true →
well_formed_closed_ex_aux (bcmcloseex (lower_closing_list dummy_x l) ϕ) 0 = true.
Lemma wfcexaux_bcmcloseex_evar_open_change_evar_2
l ϕ dbi (f : prod db_index evar → evar):
well_formed_closed_ex_aux (bcmcloseex (map (λ p, (p.1, (f p))) l) ϕ) dbi
= well_formed_closed_ex_aux (bcmcloseex l ϕ) dbi.
Lemma wfcex_and_increasing_first_not_k_impl_wfcex
(l : list (prod db_index evar))
(k : db_index)
(ϕ : Pattern)
:
closure_increasing l →
(∀ p, l !! 0 = Some p → p.1 > k) →
well_formed_closed_ex_aux (bcmcloseex l ϕ) k = true →
bevar_occur ϕ k = false.
Lemma wfcexaux_bcmcloseex_take_lower_drop
(dummy_x : evar)
(l : list (db_index × evar))
(idx : nat)
(ϕ : Pattern) :
(∀ (j : nat) (y : nat × evar), l !! j = Some y → j < idx → ¬ y.1 ≠ 0) →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
well_formed_closed_ex_aux
(bcmcloseex (take idx l ++ lower_closing_list dummy_x (drop idx l)) ϕ) 0.
Lemma closure_increasing_tail
p l
:
closure_increasing (p :: l) →
closure_increasing l.
Lemma bcmcloseex_take_lower_drop
(dummy_x : evar)
(l : list (db_index × evar))
(idx : nat)
(ϕ : Pattern)
(x : nat × evar)
:
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 = true →
l !! idx = Some x →
x.1 ≠ 0 →
(∀ (j : nat) (y : nat × evar), l !! j = Some y → j < idx → ¬ y.1 ≠ 0) →
(bcmcloseex (take idx l ++ lower_closing_list dummy_x (drop idx l)) ϕ) = (bcmcloseex l ϕ).
Lemma make_zero_list_equiv (dummy_x : evar) (l : list (prod db_index evar)) ϕ:
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
bcmcloseex (make_zero_list dummy_x l) ϕ = bcmcloseex l ϕ.
Lemma pre_predicate_0 (k : db_index) (M : Model) (ϕ : Pattern) :
M_pre_pre_predicate 0 M ϕ →
M_pre_pre_predicate k M ϕ.
Lemma closed_M_pre_pre_predicate_is_M_predicate (k : db_index) (M : Model) (ϕ : Pattern) :
well_formed_closed_ex_aux ϕ 0 →
M_pre_pre_predicate k M ϕ →
M_predicate M ϕ.
Lemma M_pre_pre_predicate_bott (k : db_index) (M : Model) :
M_pre_pre_predicate k M patt_bott.
Lemma M_pre_pre_predicate_imp
(k : db_index) (M : Model) (p q : Pattern) :
M_pre_pre_predicate k M p →
M_pre_pre_predicate k M q →
M_pre_pre_predicate k M (patt_imp p q).
Lemma bcmcloseex_propagate_last_zero
l x ϕ
:
bcmcloseex (map (λ p : nat × evar, (S p.1, p.2)) l ++ [(0, x)]) ϕ
= bcmcloseex ((0,x)::l) ϕ.
(*
Lemma M_predicate_evar_open (k : db_index) M ϕ x :
M_predicate M (evar_open 0 x)
*)
Lemma M_pre_pre_predicate_exists (k : db_index) M ϕ :
M_pre_pre_predicate (S k) M ϕ →
M_pre_pre_predicate k M (patt_exists ϕ).
Definition M_pre_predicate (M : Model) (ϕ : Pattern) : Prop
:= ∀ k, M_pre_pre_predicate k M ϕ.
Lemma M_pre_pre_predicate_impl_M_pre_predicate
(k : nat) (M : Model) (ϕ : Pattern)
:
M_pre_pre_predicate k M ϕ →
M_pre_predicate M ϕ.
Definition T_pre_pre_predicate k Γ ϕ :=
∀ M, satisfies_theory M Γ → M_pre_pre_predicate k M ϕ.
Definition T_pre_predicate Γ ϕ :=
∀ M, satisfies_theory M Γ → M_pre_predicate M ϕ.
Lemma T_pre_pre_predicate_impl_T_pre_predicate
k Γ ϕ:
T_pre_pre_predicate k Γ ϕ →
T_pre_predicate Γ ϕ.
Lemma M_pre_predicate_imp
(M : Model) (p q : Pattern) :
M_pre_predicate M p →
M_pre_predicate M q →
M_pre_predicate M (patt_imp p q).
Lemma M_pre_predicate_bott
(M : Model) :
M_pre_predicate M patt_bott.
Lemma M_pre_predicate_exists
(M : Model) (p : Pattern) :
M_pre_predicate M p →
M_pre_predicate M (patt_exists p).
Lemma M_pre_predicate_evar_open
(M : Model) (ϕ : Pattern) (x : evar) :
M_pre_predicate M ϕ →
M_pre_predicate M (ϕ^{evar: 0 ↦ x}).
End with_signature.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Inductive closure_increasing : (list (prod db_index evar)) → Prop :=
| ci_nil : closure_increasing []
| ci_single
(k0 : db_index)
(x0 : evar) :
closure_increasing [(k0,x0)]
| ci_cons
(k0 k1 : db_index)
(x0 x1 : evar)
(l : list (prod db_index evar)) :
k0 ≤ k1 →
closure_increasing ((k1,x1)::l) →
closure_increasing ((k0,x0)::(k1,x1)::l)
.
Definition M_pre_pre_predicate (k : db_index) (M : Model) (ϕ : Pattern) : Prop :=
∀ (l : list (prod db_index evar)),
Forall (λ p, p.1 ≤ k) l →
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
M_predicate M (bcmcloseex l ϕ).
Lemma pre_predicate_S (k : db_index) (M : Model) (ϕ : Pattern) :
M_pre_pre_predicate (S k) M ϕ →
M_pre_pre_predicate k M ϕ.
Definition closing_list_weight (l : list (prod db_index evar)) : nat :=
sum_list_with fst l.
Lemma drop_weight (dummy_x : evar) (idx : nat) (l : list (prod db_index evar)) :
closing_list_weight l ≥ closing_list_weight (drop idx l).
Lemma closure_increasing_map_pred
(l : list (prod db_index evar))
:
Forall (λ p, p.1 > 0) l →
closure_increasing l →
closure_increasing (map (λ p, (Nat.pred p.1, p.2)) l).
Lemma closure_increasing_map_S
(l : list (prod db_index evar))
:
closure_increasing l →
closure_increasing (map (λ p, (S p.1, p.2)) l).
Definition lower_closing_list (x : evar) (l : list (prod db_index evar))
:= (0,x)::(map (λ p, (Nat.pred p.1, p.2)) l).
Lemma closure_increasing_lower_closing_list
(dummy_x : evar)
(l : list (prod db_index evar))
:
closure_increasing l →
closure_increasing (lower_closing_list dummy_x l).
Lemma lower_closing_list_weight (x : evar) (l : list (prod db_index evar)) :
closing_list_weight l ≥ closing_list_weight (lower_closing_list x l).
Lemma lower_closing_list_same
(x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
bevar_occur ϕ 0 = false →
Forall (λ p, p.1 > 0) l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
bcmcloseex (lower_closing_list x l) ϕ = bcmcloseex l ϕ.
(*
Fixpoint lower_closing_list_iter (k : nat) (x : evar) (l : list (prod db_index evar))
:=
match k with
| 0 => l
| (S k') => lower_closing_list_iter k' x (lower_closing_list x l)
end.
Lemma lower_closing_list_iter_same
{Σ : Signature}
(k : nat)
(x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
bcmcloseex (lower_closing_list_iter k x l) ϕ = bcmcloseex l ϕ.
Proof. Abort.
*)
Lemma list_find_dep {A} P `{∀ x, Decision (P x)} (l : list A) :
({p : (nat×A)%type & (l !! p.1 = Some p.2 ∧ P p.2 ∧ ∀ j y, l !! j = Some y → j < p.1 → ¬P y) }
+ (Forall (λ x, ¬P x) l))%type.
Equations? make_zero_list
(dummy_x : evar)
(l : list (prod db_index evar))
: (list (prod db_index evar))
by wf (closing_list_weight l) lt
:=
make_zero_list dummy_x l
with (@list_find_dep _ (λ p, p.1 ≠ 0) _ l) ⇒ {
| inr _ ⇒ l
| inl (existT p pf) ⇒
let idx := p.1 in
(firstn idx l) ++ (make_zero_list dummy_x (lower_closing_list dummy_x (skipn idx l)))
}.
Lemma make_zero_list_zeroes (dummy_x : evar) (l : list (prod db_index evar)) :
(Forall (λ p, p.1 = 0) (make_zero_list dummy_x l)).
Lemma closure_increasing_app_proj1
(l₁ l₂ : list (prod db_index evar))
:
closure_increasing (l₁ ++ l₂) →
closure_increasing l₁.
Lemma closure_increasing_app_proj2
(l₁ l₂ : list (prod db_index evar))
:
closure_increasing (l₁ ++ l₂) →
closure_increasing l₂.
Lemma wfc_ex_aux_evar_open_change_evar x x' dbi ϕ:
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x}) dbi =
well_formed_closed_ex_aux (ϕ^{evar: dbi ↦ x'}) dbi.
Lemma wfcexaux_bcmcloseex_evar_open_change_evar l x x' dbi dbi' ϕ:
well_formed_closed_ex_aux (bcmcloseex l (ϕ^{evar: dbi ↦ x})) dbi'
= well_formed_closed_ex_aux (bcmcloseex l (ϕ^{evar: dbi ↦ x'})) dbi'.
Lemma wfcexaux_bcmcloseex_lower_closing_list
(dummy_x : evar)
(l : list (prod db_index evar))
(ϕ : Pattern)
:
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 = true →
well_formed_closed_ex_aux (bcmcloseex (lower_closing_list dummy_x l) ϕ) 0 = true.
Lemma wfcexaux_bcmcloseex_evar_open_change_evar_2
l ϕ dbi (f : prod db_index evar → evar):
well_formed_closed_ex_aux (bcmcloseex (map (λ p, (p.1, (f p))) l) ϕ) dbi
= well_formed_closed_ex_aux (bcmcloseex l ϕ) dbi.
Lemma wfcex_and_increasing_first_not_k_impl_wfcex
(l : list (prod db_index evar))
(k : db_index)
(ϕ : Pattern)
:
closure_increasing l →
(∀ p, l !! 0 = Some p → p.1 > k) →
well_formed_closed_ex_aux (bcmcloseex l ϕ) k = true →
bevar_occur ϕ k = false.
Lemma wfcexaux_bcmcloseex_take_lower_drop
(dummy_x : evar)
(l : list (db_index × evar))
(idx : nat)
(ϕ : Pattern) :
(∀ (j : nat) (y : nat × evar), l !! j = Some y → j < idx → ¬ y.1 ≠ 0) →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
well_formed_closed_ex_aux
(bcmcloseex (take idx l ++ lower_closing_list dummy_x (drop idx l)) ϕ) 0.
Lemma closure_increasing_tail
p l
:
closure_increasing (p :: l) →
closure_increasing l.
Lemma bcmcloseex_take_lower_drop
(dummy_x : evar)
(l : list (db_index × evar))
(idx : nat)
(ϕ : Pattern)
(x : nat × evar)
:
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 = true →
l !! idx = Some x →
x.1 ≠ 0 →
(∀ (j : nat) (y : nat × evar), l !! j = Some y → j < idx → ¬ y.1 ≠ 0) →
(bcmcloseex (take idx l ++ lower_closing_list dummy_x (drop idx l)) ϕ) = (bcmcloseex l ϕ).
Lemma make_zero_list_equiv (dummy_x : evar) (l : list (prod db_index evar)) ϕ:
closure_increasing l →
well_formed_closed_ex_aux (bcmcloseex l ϕ) 0 →
bcmcloseex (make_zero_list dummy_x l) ϕ = bcmcloseex l ϕ.
Lemma pre_predicate_0 (k : db_index) (M : Model) (ϕ : Pattern) :
M_pre_pre_predicate 0 M ϕ →
M_pre_pre_predicate k M ϕ.
Lemma closed_M_pre_pre_predicate_is_M_predicate (k : db_index) (M : Model) (ϕ : Pattern) :
well_formed_closed_ex_aux ϕ 0 →
M_pre_pre_predicate k M ϕ →
M_predicate M ϕ.
Lemma M_pre_pre_predicate_bott (k : db_index) (M : Model) :
M_pre_pre_predicate k M patt_bott.
Lemma M_pre_pre_predicate_imp
(k : db_index) (M : Model) (p q : Pattern) :
M_pre_pre_predicate k M p →
M_pre_pre_predicate k M q →
M_pre_pre_predicate k M (patt_imp p q).
Lemma bcmcloseex_propagate_last_zero
l x ϕ
:
bcmcloseex (map (λ p : nat × evar, (S p.1, p.2)) l ++ [(0, x)]) ϕ
= bcmcloseex ((0,x)::l) ϕ.
(*
Lemma M_predicate_evar_open (k : db_index) M ϕ x :
M_predicate M (evar_open 0 x)
*)
Lemma M_pre_pre_predicate_exists (k : db_index) M ϕ :
M_pre_pre_predicate (S k) M ϕ →
M_pre_pre_predicate k M (patt_exists ϕ).
Definition M_pre_predicate (M : Model) (ϕ : Pattern) : Prop
:= ∀ k, M_pre_pre_predicate k M ϕ.
Lemma M_pre_pre_predicate_impl_M_pre_predicate
(k : nat) (M : Model) (ϕ : Pattern)
:
M_pre_pre_predicate k M ϕ →
M_pre_predicate M ϕ.
Definition T_pre_pre_predicate k Γ ϕ :=
∀ M, satisfies_theory M Γ → M_pre_pre_predicate k M ϕ.
Definition T_pre_predicate Γ ϕ :=
∀ M, satisfies_theory M Γ → M_pre_predicate M ϕ.
Lemma T_pre_pre_predicate_impl_T_pre_predicate
k Γ ϕ:
T_pre_pre_predicate k Γ ϕ →
T_pre_predicate Γ ϕ.
Lemma M_pre_predicate_imp
(M : Model) (p q : Pattern) :
M_pre_predicate M p →
M_pre_predicate M q →
M_pre_predicate M (patt_imp p q).
Lemma M_pre_predicate_bott
(M : Model) :
M_pre_predicate M patt_bott.
Lemma M_pre_predicate_exists
(M : Model) (p : Pattern) :
M_pre_predicate M p →
M_pre_predicate M (patt_exists p).
Lemma M_pre_predicate_evar_open
(M : Model) (ϕ : Pattern) (x : evar) :
M_pre_predicate M ϕ →
M_pre_predicate M (ϕ^{evar: 0 ↦ x}).
End with_signature.
This page has been generated by coqdoc