octalgo.octalgo.projection
Require Import syntax.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.
Require Import soundness.
Require Import fixpoint.
Require Import completeness.
Require Import bigop_aux.
Require Import utils.
Require Import finseqs.
Set Implicit Arguments.
Variable p : program.
Hypothesis psafe : prog_safe p.
Variable i : interp.
Hypothesis isafe : safe_edb i.
Variable def : syntax.constant.
Hypothesis psafe : prog_safe p.
Variable i : interp.
Hypothesis isafe : safe_edb i.
Variable def : syntax.constant.
Hypothesis always_cons :
[∀ cl in p, ((hsym_cl cl) == f) ==>
[∃ c:syntax.constant, nth_error (arg_atom (head_cl cl)) ind == (Some (Val c))]].
[∀ cl in p, ((hsym_cl cl) == f) ==>
[∃ c:syntax.constant, nth_error (arg_atom (head_cl cl)) ind == (Some (Val c))]].
the cloned predicates are not f, different from one another and
have the right arity
Hypothesis pnotf : [∀ c, pclone c != f].
Hypothesis pinj : injective pclone.
Hypothesis parity : [∀ c, arity f == (arity (pclone c)).+1].
Hypothesis pinj : injective pclone.
Hypothesis parity : [∀ c, arity f == (arity (pclone c)).+1].
There are enough variables for the P(..,c,..) :- P_c(...) rules
Rule can have at least one element in their bodies
Definition is_clone_pred (g : symtype) : bool :=
[∃ c, g == pclone c].
Lemma is_clone_clone_pred c :
is_clone_pred (pclone c).
Definition is_clone_ga (ga : gatom) : bool :=
is_clone_pred (sym_gatom ga).
[∃ c, g == pclone c].
Lemma is_clone_clone_pred c :
is_clone_pred (pclone c).
Definition is_clone_ga (ga : gatom) : bool :=
is_clone_pred (sym_gatom ga).
Hypotheses: no clone in the original program or the EDB
Hypothesis pfresh : [∀ c, pclone c \notin sym_prog p].
Hypothesis ifresh : ~~ [∃ x in i, is_clone_ga x].
Hypothesis ifresh : ~~ [∃ x in i, is_clone_ga x].
more usable version of pfresh
Lemma Hclp_not_cloned (cl : clause) :
cl \in p → [∀ x in wlist_to_seq_co (body_cl cl), ~~ is_clone_pred (sym_atom x)].
cl \in p → [∀ x in wlist_to_seq_co (body_cl cl), ~~ is_clone_pred (sym_atom x)].
no clone in the original semantic
Definition ind_terms :=
pmap (fun cl ⇒ nth_error (arg_atom (head_cl cl)) ind) [seq cl <- p | hsym_cl cl == f].
Definition ind_vals :=
pmap (fun t ⇒ if t is Val c then Some c else None) ind_terms.
Lemma always_cons_in_vals :
[∀ cl in p, ((hsym_cl cl) == f)
==> [∃ c in ind_vals, nth_error (arg_atom (head_cl cl)) ind == (Some (Val c))]].
pmap (fun cl ⇒ nth_error (arg_atom (head_cl cl)) ind) [seq cl <- p | hsym_cl cl == f].
Definition ind_vals :=
pmap (fun t ⇒ if t is Val c then Some c else None) ind_terms.
Lemma always_cons_in_vals :
[∀ cl in p, ((hsym_cl cl) == f)
==> [∃ c in ind_vals, nth_error (arg_atom (head_cl cl)) ind == (Some (Val c))]].
Definition raw_atom_clone (j : 'I_(arity f)) (a : raw_atom) : raw_atom :=
match a with
| RawAtom pr args ⇒
if (pr == f) then
match nth_error args j with
| Some (Val c) ⇒ RawAtom (pclone c) (sremove args j)
| _ ⇒ RawAtom pr args end
else RawAtom pr args end.
Lemma wf_clone (j : 'I_(arity f)) (a : atom) : wf_atom (raw_atom_clone j a).
Definition atom_clone (j : 'I_(arity f)) (a : atom) : atom :=
Atom (wf_clone j a).
match a with
| RawAtom pr args ⇒
if (pr == f) then
match nth_error args j with
| Some (Val c) ⇒ RawAtom (pclone c) (sremove args j)
| _ ⇒ RawAtom pr args end
else RawAtom pr args end.
Lemma wf_clone (j : 'I_(arity f)) (a : atom) : wf_atom (raw_atom_clone j a).
Definition atom_clone (j : 'I_(arity f)) (a : atom) : atom :=
Atom (wf_clone j a).
Definition raw_gatom_clone (j : 'I_(arity f)) (a : raw_gatom) : raw_gatom :=
match a with
| RawGAtom pr args ⇒
if (pr == f) then
match nth_error args j with
| Some c ⇒ RawGAtom (pclone c) (sremove args j)
| None ⇒ RawGAtom pr args end
else RawGAtom pr args end.
Lemma wf_gclone (j : 'I_(arity f)) (ga : gatom) : wf_gatom (raw_gatom_clone j ga).
Definition gatom_clone (j : 'I_(arity f)) (ga : gatom) : gatom :=
GAtom (wf_gclone j ga).
match a with
| RawGAtom pr args ⇒
if (pr == f) then
match nth_error args j with
| Some c ⇒ RawGAtom (pclone c) (sremove args j)
| None ⇒ RawGAtom pr args end
else RawGAtom pr args end.
Lemma wf_gclone (j : 'I_(arity f)) (ga : gatom) : wf_gatom (raw_gatom_clone j ga).
Definition gatom_clone (j : 'I_(arity f)) (ga : gatom) : gatom :=
GAtom (wf_gclone j ga).
Definition tail_clone (j : 'I_(arity f)) (tl : tail) : tail :=
wmap (atom_clone j) tl.
Definition cl_clone (j : 'I_(arity f)) (cl : clause) : clause :=
match cl with Clause h tl ⇒ Clause (atom_clone j h) (tail_clone j tl) end.
wmap (atom_clone j) tl.
Definition cl_clone (j : 'I_(arity f)) (cl : clause) : clause :=
match cl with Clause h tl ⇒ Clause (atom_clone j h) (tail_clone j tl) end.
Lemma atom_clone_not_f (j : 'I_(arity f)) (a : atom) :
sym_atom a != f → atom_clone j a = a.
Lemma gatom_clone_not_f (j : 'I_(arity f)) (ga : gatom) :
sym_gatom ga != f → gatom_clone j ga = ga.
Lemma gatom_clone_f (j : 'I_(arity f)) (a : atom) c (s : sub) :
sym_atom a = f →
nth_error (arg_atom a) j = Some (Val c) →
gatom_clone j (gr_atom_def def s a)
= gr_atom_def def s (atom_clone j a).
Lemma is_clone_ga_f (ga : gatom) :
sym_gatom ga = f
→ is_clone_ga (gatom_clone ind ga).
Lemma clone_oob (j : 'I_(arity f)) (a : atom) :
nth_error (arg_atom a) j = None → (atom_clone j a) = a.
Lemma clone_v (j : 'I_(arity f)) v (a : atom) :
nth_error (arg_atom a) j = Some (Var v) → (atom_clone j a) = a.
Lemma pred_clone_c (j : 'I_(arity f)) c (a : atom) :
nth_error (arg_atom a) j = Some (Val c)
→ sym_atom a = f
→ sym_atom (atom_clone j a) = pclone c.
Definition gen_vars_j (j : 'I_n.+1): seq term :=
map (fun x ⇒ Var x) (map (fun x : 'I_j ⇒ @widen_ord j n (ltn_ord j) x) (dep_iota 0 j)).
map (fun x ⇒ Var x) (map (fun x : 'I_j ⇒ @widen_ord j n (ltn_ord j) x) (dep_iota 0 j)).
Definition gen_vars : seq term :=
gen_vars_j (Ordinal arity_vars).
Definition gen_vars_rem_j (j : 'I_n.+1) (k : 'I_n) : seq term :=
rem (Var k) (gen_vars_j j).
Definition gen_vars_rem (j : 'I_(arity f)) : seq term :=
gen_vars_rem_j (Ordinal arity_vars) (@widen_ord (arity f) n arity_vars j).
Definition gen_vars_c_f (j : 'I_(arity f)) (c : syntax.constant) :=
set_nth (Val c) gen_vars j (Val c).
Lemma ind_in_gen_vars_j (j : 'I_n.+1) (k : 'I_n) :
k < j →
Var k \in gen_vars_j j.
Lemma ind_in_gen_vars (j : 'I_(arity f)) :
Var (widen_ord (m:=n) arity_vars j) \in gen_vars.
Lemma size_gen_vars_j (j : 'I_n.+1) :
size (gen_vars_j j) = j.
Lemma size_gen_vars : size gen_vars = arity f.
Lemma gen_vars_j_find (j : 'I_n.+1) (k : 'I_n) :
k < j
→ find (eq_op^~ (Var k)) (gen_vars_j j) = k.
Lemma gen_vars_j_uniq (j : 'I_n.+1) : uniq (gen_vars_j j).
Lemma gen_vars_rem_uniq (j : 'I_(arity f)) : uniq (gen_vars_rem j).
Lemma gen_vars_j_all_v (j : 'I_n.+1) :
[∀ t in gen_vars_j j, ∃ v, t == Var v].
Lemma gen_vars_rem_all_v (j : 'I_(arity f)) :
[∀ t in gen_vars_rem j, ∃ v, t == Var v].
gen_vars_j (Ordinal arity_vars).
Definition gen_vars_rem_j (j : 'I_n.+1) (k : 'I_n) : seq term :=
rem (Var k) (gen_vars_j j).
Definition gen_vars_rem (j : 'I_(arity f)) : seq term :=
gen_vars_rem_j (Ordinal arity_vars) (@widen_ord (arity f) n arity_vars j).
Definition gen_vars_c_f (j : 'I_(arity f)) (c : syntax.constant) :=
set_nth (Val c) gen_vars j (Val c).
Lemma ind_in_gen_vars_j (j : 'I_n.+1) (k : 'I_n) :
k < j →
Var k \in gen_vars_j j.
Lemma ind_in_gen_vars (j : 'I_(arity f)) :
Var (widen_ord (m:=n) arity_vars j) \in gen_vars.
Lemma size_gen_vars_j (j : 'I_n.+1) :
size (gen_vars_j j) = j.
Lemma size_gen_vars : size gen_vars = arity f.
Lemma gen_vars_j_find (j : 'I_n.+1) (k : 'I_n) :
k < j
→ find (eq_op^~ (Var k)) (gen_vars_j j) = k.
Lemma gen_vars_j_uniq (j : 'I_n.+1) : uniq (gen_vars_j j).
Lemma gen_vars_rem_uniq (j : 'I_(arity f)) : uniq (gen_vars_rem j).
Lemma gen_vars_j_all_v (j : 'I_n.+1) :
[∀ t in gen_vars_j j, ∃ v, t == Var v].
Lemma gen_vars_rem_all_v (j : 'I_(arity f)) :
[∀ t in gen_vars_rem j, ∃ v, t == Var v].
Definition raw_gen_c_f (j : 'I_(arity f)) (c : syntax.constant) : raw_atom :=
RawAtom f (gen_vars_c_f j c).
Lemma raw_gen_f_c_wf (j : 'I_(arity f)) (c : syntax.constant) :
wf_atom (raw_gen_c_f j c).
Definition gen_f_c (j : 'I_(arity f)) (c : syntax.constant) : atom :=
Atom (raw_gen_f_c_wf j c).
Definition raw_gen_f_c (j : 'I_(arity f)) (c : syntax.constant) : raw_atom :=
RawAtom (pclone c) (gen_vars_rem j).
Lemma raw_gen_c_f_c_wf (j : 'I_(arity f)) (c : syntax.constant) :
wf_atom (raw_gen_f_c j c).
Definition gen_c_f_c (j : 'I_(arity f)) (c : syntax.constant) : atom :=
Atom (raw_gen_c_f_c_wf j c).
Lemma gen_c_f_c_size (j : 'I_(arity f)) (c : syntax.constant) :
size [:: gen_c_f_c j c] ≤ bn.
Definition c_to_gen (j : 'I_(arity f)) (c : syntax.constant) :=
Clause (gen_f_c ind c) (seq_to_wlist_uncut (gen_c_f_c_size j c)).
size [:: gen_c_f_c j c] ≤ bn.
Definition c_to_gen (j : 'I_(arity f)) (c : syntax.constant) :=
Clause (gen_f_c ind c) (seq_to_wlist_uncut (gen_c_f_c_size j c)).
Definition proj_prog :=
(map (cl_clone ind) p) ++ [seq c_to_gen ind c | c in ind_vals].
Lemma clone_in (cl : clause) :
cl \in p → cl_clone ind cl \in proj_prog.
(map (cl_clone ind) p) ++ [seq c_to_gen ind c | c in ind_vals].
Lemma clone_in (cl : clause) :
cl \in p → cl_clone ind cl \in proj_prog.
Extracting substitutions for P <- P_c rules
Fixpoint extract_sub_seq_c (args : seq term) (gargs : seq syntax.constant)
(s : sub) : sub :=
match gargs with
[::] ⇒ s
| x::l ⇒
match args with
[::] ⇒ s | Val x'::l' ⇒ (extract_sub_seq_c l' l s)
| Var x'::l' ⇒ add (extract_sub_seq_c l' l s) x' x end end.
Lemma v_in_extract_c (args : seq term) (gargs : seq syntax.constant)
(s : sub) (v : 'I_n) :
size args ≤ size gargs
→ v \in \big[setU (T:=ordinal_finType n)/set0]_(t <- args) term_vars t
→ v \in dom (extract_sub_seq_c args gargs s).
Lemma in_extract_c_v (args : seq term) (gargs : seq syntax.constant)
(v : 'I_n) :
size args ≤ size gargs
→ (extract_sub_seq_c args gargs emptysub) v
→ Var v \in args.
Definition extract_sub_ga (a : atom) (ga : gatom) :=
extract_sub_seq_c (arg_atom a) (arg_gatom ga) emptysub.
Lemma v_in_extract (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ atom_vars a \subset dom (extract_sub_ga a ga).
Lemma extract_in_v (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ dom (extract_sub_ga a ga) \subset atom_vars a .
Lemma extract_dom (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ dom (extract_sub_ga a ga) = atom_vars a.
Lemma var_neq v vb : ((v == vb) = false) → ((Var v == Var vb) = false).
Lemma add_seq_gr_def (s : sub) v c (lt : seq term) :
Var v \notin lt →
[seq gr_term_def def s i0 | i0 <- lt] = [seq gr_term_def def (add s v c) i0 | i0 <- lt].
Lemma extract_sub_seq_map (lt : seq term) (lc : seq syntax.constant) :
uniq lt
→ size lt = size lc
→ [∀ t in lt, ∃ v, t == Var v]
→ lc = [seq gr_term_def def (extract_sub_seq_c lt lc emptysub) i0 | i0 <- lt].
Lemma extract_sub_seq_rem_map (lt : seq term) v (lc : seq syntax.constant) (j : 'I_n) c:
j < size lt →
size lt = size lc →
uniq lt →
[∀ t in lt, ∃ vb, t == Var vb] →
find (fun y ⇒ y == Var v) lt = j →
nth_error lc j = Some c →
lc = [seq gr_term_def def
(extract_sub_seq_c (rem (Var v) lt) (sremove lc j) emptysub) i
| i <- set_nth (Val c) lt j (Val c)].
Lemma gr_term_def_seq_add_notin (l : seq term) v c (s:sub) :
Var v \notin l
→ [seq gr_term_def def (add s v c) i | i <- l] = [seq gr_term_def def s i | i <- l].
Lemma extract_gr_v (s : sub) (a1 a2 : atom) :
sym_atom a1 = sym_atom a2
→ [∀ t in (arg_atom a1), ∃ v:'I_n, t == Var v]
→ uniq (arg_atom a1)
→ gr_atom_def def s a2 =
gr_atom_def def (extract_sub_ga a1 (gr_atom_def def s a2)) a1.
(s : sub) : sub :=
match gargs with
[::] ⇒ s
| x::l ⇒
match args with
[::] ⇒ s | Val x'::l' ⇒ (extract_sub_seq_c l' l s)
| Var x'::l' ⇒ add (extract_sub_seq_c l' l s) x' x end end.
Lemma v_in_extract_c (args : seq term) (gargs : seq syntax.constant)
(s : sub) (v : 'I_n) :
size args ≤ size gargs
→ v \in \big[setU (T:=ordinal_finType n)/set0]_(t <- args) term_vars t
→ v \in dom (extract_sub_seq_c args gargs s).
Lemma in_extract_c_v (args : seq term) (gargs : seq syntax.constant)
(v : 'I_n) :
size args ≤ size gargs
→ (extract_sub_seq_c args gargs emptysub) v
→ Var v \in args.
Definition extract_sub_ga (a : atom) (ga : gatom) :=
extract_sub_seq_c (arg_atom a) (arg_gatom ga) emptysub.
Lemma v_in_extract (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ atom_vars a \subset dom (extract_sub_ga a ga).
Lemma extract_in_v (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ dom (extract_sub_ga a ga) \subset atom_vars a .
Lemma extract_dom (a : atom) (ga : gatom) :
arity (sym_atom a) ≤ arity (sym_gatom ga)
→ dom (extract_sub_ga a ga) = atom_vars a.
Lemma var_neq v vb : ((v == vb) = false) → ((Var v == Var vb) = false).
Lemma add_seq_gr_def (s : sub) v c (lt : seq term) :
Var v \notin lt →
[seq gr_term_def def s i0 | i0 <- lt] = [seq gr_term_def def (add s v c) i0 | i0 <- lt].
Lemma extract_sub_seq_map (lt : seq term) (lc : seq syntax.constant) :
uniq lt
→ size lt = size lc
→ [∀ t in lt, ∃ v, t == Var v]
→ lc = [seq gr_term_def def (extract_sub_seq_c lt lc emptysub) i0 | i0 <- lt].
Lemma extract_sub_seq_rem_map (lt : seq term) v (lc : seq syntax.constant) (j : 'I_n) c:
j < size lt →
size lt = size lc →
uniq lt →
[∀ t in lt, ∃ vb, t == Var vb] →
find (fun y ⇒ y == Var v) lt = j →
nth_error lc j = Some c →
lc = [seq gr_term_def def
(extract_sub_seq_c (rem (Var v) lt) (sremove lc j) emptysub) i
| i <- set_nth (Val c) lt j (Val c)].
Lemma gr_term_def_seq_add_notin (l : seq term) v c (s:sub) :
Var v \notin l
→ [seq gr_term_def def (add s v c) i | i <- l] = [seq gr_term_def def s i | i <- l].
Lemma extract_gr_v (s : sub) (a1 a2 : atom) :
sym_atom a1 = sym_atom a2
→ [∀ t in (arg_atom a1), ∃ v:'I_n, t == Var v]
→ uniq (arg_atom a1)
→ gr_atom_def def s a2 =
gr_atom_def def (extract_sub_ga a1 (gr_atom_def def s a2)) a1.
Lemma match_fold_clone (args : seq term) (gargs : seq syntax.constant) (j : nat) c s :
nth_error args j = Some (Val c) → nth_error gargs j = Some c →
foldl
(fun (acc : option {ffun 'I_n → option syntax.constant})
(p0 : syntax.constant × term) ⇒ obind (match_term p0.1 p0.2) acc)
(Some s) (zip gargs args) =
foldl
(fun (acc : option {ffun 'I_n → option syntax.constant})
(p0 : syntax.constant × term) ⇒ obind (match_term p0.1 p0.2) acc)
(Some s) (zip (sremove gargs j) (sremove args j)).
Lemma match_atom_clone_cnone (j : 'I_(arity f)) (s : sub) (a : atom) c (ga : gatom) :
nth_error (arg_atom a) j = None ∨
nth_error (arg_atom a) j = Some (Val c) →
sym_atom a = sym_gatom ga →
match_atom s a ga = match_atom s (atom_clone j a) (gatom_clone j ga).
Lemma match_atom_clone_v (j : 'I_(arity f)) (s : sub) (a : atom) (ga : gatom) v :
nth_error (arg_atom a) j = Some (Var v) →
sym_atom a = sym_gatom ga →
match_atom s a ga = match_atom s (atom_clone j a) ga.
Lemma sym_satom_gatom (a : atom) (ga : gatom) (s : sub) :
satom a s = to_atom ga → sym_atom a = sym_gatom ga.
Lemma match_atom_all_clone_cnone (j : 'I_(arity f)) (k1 k2 : interp) (a : atom) (s : sub) (c : syntax.constant) :
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
nth_error (arg_atom a) j = None ∨ nth_error (arg_atom a) j = Some (Val c) →
match_atom_all k1 a s \subset match_atom_all k2 (atom_clone j a) s.
Lemma match_atom_all_clone_v (j : 'I_(arity f)) (k1 k2 : interp) (a : atom) (s : sub) v :
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
nth_error (arg_atom a) j = Some (Var v) →
match_atom_all k1 a s \subset match_atom_all k2 (atom_clone j a) s.
Lemma pmatch_clone (j : 'I_(arity f)) (s : sub) (k1 k2 : interp) c (cl : clause) (ss : {set sub}) :
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
nth_error (arg_atom (head_cl cl)) j = Some (Val c) →
s \in match_pbody (body_cl cl) k1 ss →
exists2 s' : sub, s' \in match_pbody (body_cl (cl_clone j cl)) k2 ss &
(((hsym_cl cl != f) → gr_atom_def def s (head_cl cl) =
gr_atom_def def s' (head_cl (cl_clone j cl)))
∧ ((hsym_cl cl = f) → gatom_clone j (gr_atom_def def s (head_cl cl)) =
gr_atom_def def s' (head_cl (cl_clone j cl)))).
Lemma match_clone (j : 'I_(arity f)) (s : sub) (k1 k2 : interp) c (cl : clause) :
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
nth_error (arg_atom (head_cl cl)) j = Some (Val c) →
s \in match_body k1 (body_cl cl) →
exists2 s' : sub, s' \in match_body k2 (body_cl (cl_clone j cl)) &
(((hsym_cl cl != f) → gr_atom_def def s (head_cl cl) =
gr_atom_def def s' (head_cl (cl_clone j cl)))
∧ ((hsym_cl cl = f) → gatom_clone j (gr_atom_def def s (head_cl cl)) =
gr_atom_def def s' (head_cl (cl_clone j cl)))).
Lemma pmatch_clone_not_f (j : 'I_(arity f)) (s : sub) (k1 k2 : interp) (cl : clause) (ss : {set sub}) :
(hsym_cl cl != f) →
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
s \in match_pbody (body_cl cl) k1 ss →
exists2 s' : sub, s' \in match_pbody (body_cl (cl_clone j cl)) k2 ss &
gr_atom_def def s (head_cl cl) =
gr_atom_def def s' (head_cl (cl_clone j cl)).
Lemma match_clone_not_f (j : 'I_(arity f)) (s : sub) (k1 k2: interp) (cl : clause) :
(hsym_cl cl != f) →
k1 :|: [set gatom_clone j ga | ga in k1] \subset k2 →
s \in match_body k1 (body_cl cl) →
exists2 s' : sub, s' \in match_body k2 (body_cl (cl_clone j cl)) &
gr_atom_def def s (head_cl cl) =
gr_atom_def def s' (head_cl (cl_clone j cl)).
Lemma atom_vars_clone_c (a : atom) (j : 'I_(arity f)) c :
nth_error (arg_atom a) j = Some (Val c)
→ atom_vars a = atom_vars (atom_clone j a).
Lemma clone_bmatch (j : 'I_(arity f)) (s : sub) (k1 k2 : interp) (cl : clause) :
[∀ x in k2, ~~ is_clone_ga x]
→ k1 \subset k2 :|: [set gatom_clone j ga | ga in k2 & sym_gatom ga == f]
→ s \in match_body k1 (body_cl (cl_clone j cl))
→ cl \in p
→ exists2 s' : sub, bmatch def k2 cl s' & ((s \sub s') &&
(gr_atom_def def s (head_cl cl) == gr_atom_def def s' (head_cl cl))).
Lemma ga_a_ex_sym_eq (j : 'I_(arity f)) c (a : atom) (k : interp) s :
nth_error (arg_atom a) j = Some (Val c)
→ sym_atom a = f
→ (gr_atom_def def s (atom_clone j a)) \in k
→ exists2 s', s' \in match_body k (body_cl (c_to_gen j c))
& val (gr_atom_def def s a) = val (gr_atom_def def s' (gen_f_c j c)).
If we deduced s(f_c(t1,..,t(ind-1),t(ind+1),...,tn)),
we can fire f(...,c,...) <-- f_c(....)
to deduce s(f(t1,...,t(ind-1),c,t(ind+1),...,tn))
Lemma deducing_c_to_gen (s : sub) (a : atom) (c : syntax.constant) (k: interp) :
sym_atom a = f
→ gr_atom_def def s (atom_clone ind a) \in k
→ nth_error (arg_atom a) ind = Some (Val c)
→ gr_atom_def def s a
\in cons_clause def (c_to_gen ind c) k.
sym_atom a = f
→ gr_atom_def def s (atom_clone ind a) \in k
→ nth_error (arg_atom a) ind = Some (Val c)
→ gr_atom_def def s a
\in cons_clause def (c_to_gen ind c) k.
Lemma proj_completeness_u (m : nat) :
sem p def m i :|: [set gatom_clone ind ga | ga in sem p def m i]
\subset sem proj_prog def m.*2 i.
Theorem proj_completeness (m : nat) :
sem p def m i \subset sem proj_prog def m.*2 i.
Lemma gr_atom_def_clone_eq (j : 'I_(arity f)) a s sb :
gr_atom_def def s (atom_clone j a) = gr_atom_def def sb (atom_clone j a)
→ gr_atom_def def s a = gr_atom_def def sb a.
Lemma proj_soundness_u (m : nat) :
sem proj_prog def m i \subset
sem p def m i :|: [set gatom_clone ind ga | ga in sem p def m i & sym_gatom ga == f].
Theorem proj_soundness (m : nat) :
[set x in sem proj_prog def m i | ~~ is_clone_ga x ] \subset sem p def m i.
End Projection.