octalgo.datalogcert.soundness

This is the sixth part of the original file "pengine.v" with modifications

Require Import syntax.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.

Require Import bigop_aux.
Require Import utils.
Require Import finseqs.

Set Implicit Arguments.

Implicit Types (s r : sub) (d def : syntax.constant) (t : term) (a : atom)
(ga : gatom) (tl : list atom) (cl : clause) (i : interp).

Soundness of the standard semantics

Section Soundness.

Term Matching Soundness:

Let t be a term, d a constant and s an arbitrary substitution. If term matching outputs a substitution r, extending s with the matching of t against d, then r is indeed a solution, i.e, the instantiation of t with r equals d.

Lemma match_term_sound d t s r : match_term d t s = Some r → sterm r t = Val d.

List Fold Soundness f takes a substitution and may give back a substitution (option) and is increaising in that case. If we iterate f over l starting from u with foldl, if we get a result, it is greater than the original u (which could not be None). Reminder: obind f (Some x) = f x and obind f None = None

Lemma foldl_0_gen {A} u l r
     (f : A → sub → option sub)
     (f_pmon : ∀ x s r, f x s = Some r → s \sub r)
: foldl (fun acc p ⇒ obind (f p) acc) u l = Some r →
   exists2 s, u = Some s & s \sub r.

If iterating match_term over lists of atoms and ground atoms starting from u, we obtain a substitution r, then u was a substitution s (not None) and r greater than s

Lemma foldl_0 gar ar u r :
foldl (fun acc p ⇒ obind [eta match_term p .1 p .2 ] acc) u (zip gar ar) = Some r →
exists2 s, u = Some s & s \sub r.

Atom Matching Soundness:

Let a be an atom, ga a ground atom and s, an arbitrary substitution. If atom matching outputs a substitution r, extending s with the matching of a against ga, then r is indeed a solution, i.e, the instantiation of a with r equals ga.

Lemma match_atom_sound a ga s r :
match_atom s a ga = Some r → satom a r = to_atom ga.

Atom Matching Substitution Lemma:

If s2 is the result of matching an atom a against a ground atom ga, starting from an initial substitution s1, then s2 is the extension of s1.

Lemma match_atom_sub s1 s2 a ga :
match_atom s1 a ga = Some s2 → sub_st s1 s2.

substitution domain: set of all variables it binds

Lemma match_atoms_sub s1 i a :
[∀ s2 in (match_atom_all i a s1 ), s1 \sub s2 ].

For a grounding, no need of def. translation through the grounding or through the coresponding sub coincide.

Lemma to_sub_grt def t nu :
gr_term_def def (to_sub nu) t = gr_term nu t.

Same as above but for atom instead of terms.

Lemma to_sub_gra def a nu :
gr_atom_def def (to_sub nu) a = gr_atom nu a.

If all vars of a term t (0 or 1) are in s, then applying s on t gives a value

Lemma sub_dom_grt t s :
term_vars t \subset dom s ↔ ∃ c, sterm s t = Val c.

Reflection view for the fact that the vars of a raw atom ra are in the domain of substitution s

Lemma sub_dom_gra (ra : raw_atom) s :
reflect (∃ gra, sraw_atom ra s = to_raw_atom gra)
(raw_atom_vars ra \subset dom s).

If applying s on a gives a ground atom gra at the level of raw atoms, it also gives a raw atom ga

Lemma sub_dom_raw a s :
(∃ gra : raw_gatom , sraw_atom a s = to_raw_atom gra ) →
∃ ga : gatom , satom a s = to_atom ga.

Reflection view for fact that the vars of an atom a are in the domain of substitution s

Lemma sub_dom_ga (a : atom) s :
reflect (∃ ga, satom a s = to_atom ga)
(atom_vars a \subset dom s).

Implicit Types (ss : {set sub }).

Starting from a substitution ss0 and a list of atom tl, builds the set of all substitutions that match the interpretation i

Definition match_pbody tl i ss0 := foldS (match_atom_all i) ss0 tl.

match_pbody increasing for set sub argument

Lemma match_pbody_incr i tl ss1 ss2 :
ss1 \subset ss2 → match_pbody tl i ss1 \subset match_pbody tl i ss2.

Reflection view on the inductive theorem associated with match_pbody

Lemma match_pbody_cons a l i r ss0 :
reflect (exists2 s, s \in ss0 & r \in match_pbody l i (match_atom_all i a s))
(r \in match_pbody (a :: l) i ss0).

Relates match_pbody and pmatch.match_body

Lemma match_body_pbody tl i r :
match_body i tl = match_pbody tl i [set emptysub ].

If s' is smaller than s and undefined for v, completing it with the binding of v in s will still give a substitution smaller than s

Lemma sub_st_add v d s' s :
s' \sub s → s v = Some d → s' v = None → add s' v d \sub s.

technical lemma. If s in match_pbody (a :: ll) i sp, then s greater than sp

Lemma match_atoms_pbody s sp ll i a:
s \in match_pbody ll i (match_atom_all i a sp) → sp \sub s.

Term Matching Completeness:

Given a solution s to term-matching t w.r.t d, for any sub-substitution s', there exists an r that is a solution and also better/minimal w.r.t s

Lemma match_term_complete d t s s' :
sub_st s' s → sterm s t = Val d →
∃ r, match_term d t s' = Some r ∧ sub_st r s.

Atom Matching Completeness:

Let a be an atom, ga a ground atom and s a substitution that instantiates a to ga. Then, seeding the atom matching algorithm with s', an arbitrary restriction of s, outputs a better matching solution than s, i.e, a substitution r that is smaller or equal to s.

Lemma match_atom_complete ga a s s' :
sub_st s' s → satom a s = to_atom ga →
exists2 r, match_atom s' a ga = Some r & sub_st r s.

Let a be an atom, ga a ground atom and v a grounding. Instantiating a with the coercion of v equals the lifting of ga iff the grounding of a with v equals ga

Lemma to_gr_atomP a v ga :
satom a (to_sub v) = to_atom ga ↔ gr_atom v a = ga.

Let s' be a substitution from init ss0 that is smaller than the grounding v and v such that applying it on the body of clause cl gives atom member of interpretation i, then the set of substitutions matching the body cl for interpretation i starting from ss0 contains a substitution r smaller than v

Lemma match_ptl_complete s' ss0 i cl v :
s' \in ss0 → sub_st s' (to_sub v) →
all (mem i) (body_gcl (gr_cl v cl)) →
exists2 r, r \in match_pbody (body_cl cl) i ss0 &
sub_st r (to_sub v).

Let s' be a substitution from init ss0 that is smaller than s. Let s be such than applying s on a list of atom tl gives a list of ground atom gtl contained in i. Then matching tl in i starting from substitution ss0 contains a substitution r smaller than s

Lemma match_ptl_sub_complete s s' ss0 i tl gtl :
s' \in ss0 → sub_st s' s →
stail tl s = [seq to_atom ga | ga <- gtl ]
→ all (mem i) gtl →
exists2 r, r \in match_pbody tl i ss0 &
sub_st r s.

If applying the grounding v to the body of cl gives ground atoms in i, then matching the body of cl with i starting from the empty substitution contains a substitution r smaller than v

Lemma match_tl_complete i cl v :
all (mem i) (body_gcl (gr_cl v cl)) →
exists2 r, r \in match_pbody (body_cl cl) i [set emptysub ] &
sub_st r (to_sub v).

Let ss0 be a substitution set. If r is in the result of extending substitutions in ss0 with bindings matching the tl atom list against the ground atoms of an interpretation i, then there exists a substitution s in ss0 that r extends.

Lemma match_atom_all_sub tl i r ss0 :
r \in match_pbody tl i ss0 →
exists2 s, s \in ss0 & sub_st s r.

Let r in the result of extending substitutions in ss0 with bindings matching the tl atom list against the ground atoms of an interpretation i. Then, there exists a ground atom list gtl, such that gtl is the instantiation of t with r and all the atoms in gtl are in i.

Lemma match_pbody_sound tl i r ss0 :
  r \in match_pbody tl i ss0 →
      exists2 gtl, stail tl r = [seq to_atom ga | ga <- gtl ]
                   & all (mem i) gtl.

Lemmas on substitutions -- added

Matching between inconsistent atom and gatom fail

Lemma match_atom_dif_lengths (a : atom) (ga : gatom) (s : sub) :
  size (arg_atom a) != size (arg_gatom ga) → match_atom s a ga = None.
Lemma match_atom_diff_cons (a : atom) (ga : gatom) (s : sub) (j : nat) (c d : syntax.constant) :
   nth_error (arg_atom a) j = Some (Val c) → nth_error (arg_gatom ga) j = Some d
→ d != c → match_atom s a ga = None.

Lemma match_atom_diff_heads (s : sub) (a : atom) (ga : gatom) :
  (sym_atom a != sym_gatom ga ) → match_atom s a ga = None.

Lemma arg_c_match j (a : atom) (ga : gatom) s c :
  nth_error (arg_atom a) j = Some (Val c) →
   (nth_error (arg_gatom ga) j = Some c
∨ ((nth_error (arg_gatom ga) j = None
  ∨ ∃ d, d != c ∧ nth_error (arg_gatom ga) j = Some d ) ∧ match_atom s a ga = None )).

If s is the result of matching a on ga starting with r and v a variable of s domain, then either v was in the domain of r or v was a variable of a

Lemma match_atom_dom s r a ga v : Some s = match_atom r a ga
→ v \in dom s
→ v \in atom_vars a ∨ v \in dom r.

For any s in the result of matching a on interpretation i starting with r and v a variable of s domain, then either v was in the domain of r or v was a variable of a

Lemma match_atom_all_dom s r i a v : s \in match_atom_all i a r
→ v \in dom s
→ v \in atom_vars a ∨ v \in dom r.

If s in the result of matching the body tl against i starting with ss, then the domain of s is included in the union of the variables of tl and all the variables in the substitutions of ss

Lemma pmatch_subset_vars s tl i ss : s \in match_pbody tl i ss
→ dom s \subset ((tail_vars tl ) :|: all_dom ss ).

if s in the result of matching the body tl against i, then the domain of s is included in the variables of tl

Lemma match_subset_vars s tl i : s \in match_body i tl
→ dom s \subset tail_vars tl.

if s in the result of matching the body tl against i starting from ss, then there exists s' in ss smaller than s

Lemma match_pbody_sub s i tl ss : s \in match_pbody tl i ss →
[∃ s' in ss , s' \sub s ].

If s in the matching of a against i starting from r, then the variables of a are in the domain of s

Lemma match_atoms_vars_subset s r i a : s \in match_atom_all i a r
→ atom_vars a \subset dom s.

If s in the matching of body tl against i starting from set ss, then the variables of the body tl are in the domain of s

Lemma pmatch_vars_subset s ss tl i : s \in match_pbody tl i ss
→ tail_vars tl \subset dom s.

If s in the matching of body tl against i, then the variables of the body tl are in the domain of s

Lemma match_vars_subset s tl i : s \in match_body i tl
→ tail_vars tl \subset dom s.

If s in the matching of body tl against i, then the variables of the body tl are the domain of s

Lemma match_vars_seteq s tl i : s \in match_body i tl
→ tail_vars tl = dom s.

Let i be a safe interpretation, p a safe program. Let ga be in the semantics of p starting from i after m steps and ga symbol be intensional, then there exists a clause cl in p whose head symbol is the head symbold of ga, a substitution s for which the body of cl match with the (p-1) iteration of the semantics of p from i and ga is the result of applying s to the head of cl

Lemma ga_ded (p : program) (def : syntax.constant) (m : nat) (i : interp) ga :
  (ga \in sem p def m i ) → predtype (sym_gatom ga) = Idb → safe_edb i → prog_safe p →
  ∃ cl, cl \in p ∧ sym_gatom ga = hsym_cl cl
    ∧ ∃ s, s \in match_body (sem p def m .-1 i) (body_cl cl)
      ∧ to_atom ga = satom (head_cl cl) s.

If we apply transub to a clause cl and then take a s in the result of matching the obtained body with i, if the domain of transub was restricted to the variables of the body of cl, then s and transub have no common variable in their domain.

Lemma match_domsI i s transub cl : s \in match_body i (body_cl (scl transub cl))
→ {subset (dom transub ) ≤ tail_vars (body_cl cl)}
→ dom s :&: dom transub = set0.

Domains and variables of elements

If applying r to a term t gives a constant, the variable of t is included in the domain r

Lemma r_dom_term d t r : sterm r t = Val d → term_vars t \subset dom r.

If applying r to an atom a gives a ground atom ga, the variables of a are included in the domain of r

Lemma r_dom_atom a ga r : satom a r = to_atom ga → atom_vars a \subset dom r.

Lemma seq_inj T (x y : T) (xs ys : seq T) :
[:: x & xs ] = [:: y & ys ] → x = y ∧ xs = ys.

If applying r to a list of atom tl gives a list of ground atom gtl, the variables of tl are included in the domain of r

Lemma r_dom_body tl gtl r : stail tl r = [seq to_atom ga | ga <- gtl ] →
tail_vars tl \subset dom r.

If r in the result of matching tl against i, then applying r to tl gives a sequence of ground atoms gtl that are all in i

Lemma match_tl_sound tl i r :
  r \in match_body i tl →
        exists2 gtl, stail tl r = [seq to_atom ga | ga <- gtl ]
                     & all (mem i) gtl.

Clause Consequence Soundness:

Let cl be a safe clause and i an interpretation. If the clause consequence operator derives no new facts from cl, then i is a model for cl.

Lemma cons_cl_sound def cl i :
safe_cl cl → cons_clause def cl i \subset i → cl_true cl i .

if transub domain is included in the variables of the body of a clause cl and s in the matching of the application of transub to cl with the interpretation i, then the composition of transub and s is in the matching of cl with i

Lemma subU_match (def : syntax.constant) s transub i cl :
(dom transub ) \subset (tail_vars (body_cl cl))
→ s \in match_body i (body_cl (scl transub cl))
→ subU transub s \in match_body i (body_cl cl).

Forward Chain Soundness:

Let p be a safe program and i an interpretation. If i is the fixpoint of one iteration of forward chain, then i is a model for p.

Lemma fwd_chain_sound def p i :
prog_safe p → fwd_chain def p i = i → prog_true p i .

Technical lemma: we can define a grounding of a term by applying a substitution s with a default def, or we can complete the substitution to be a grounding using default def and apply it to s. In both cases, the result is the same

Lemma to_gr_sub def t s : gr_term_def def s t = gr_term (to_gr def s) t.

Same as above but on atom

Lemma gr_atom_defE def s a : gr_atom (to_gr def s) a = gr_atom_def def s a.

If applying s to a list of atom tl gives a list of ground atoms gtl, and i contains gtl, then i contains the result of applying s completed to be a grounding to tl.

Lemma tail_mem def s tl gtl i :
stail tl s = [seq to_atom ga | ga <- gtl ] →
all (mem i) gtl →
all (mem i) [seq gr_atom (to_gr def s) x | x <- tl ].

Clause Consequence Stability:

Let cl be a clause and i an interpretation satisfying c. Then, the clause consequence operator derives no new facts from cl.

Lemma cons_cl_stable def cl i : cl_true cl i → cons_clause def cl i \subset i.

Let p be a program. Any interpretation i that is a model of p is a fixpoint of one iteration of forward chain

Lemma fwd_chain_stable def p i : prog_true p i → fwd_chain def p i = i.

Forward Chain reflection lemma: Given a safe program p, an interpretation i is a model of p iff it is a fixpoint of one iteration of forward chain.

Lemma fwd_chainP def p i (p_safe : prog_safe p) :
reflect (prog_true p i) (fwd_chain def p i == i).

Given a program p and an interpretation i. The symbols in the strict result (without i) of applying forward chain on p given i are among the head symbols of p.

Lemma sym_pengine_subset_hsymp def p i :
{subset sym_i ((fwd_chain def p i ) :\: i) ≤ hsym_prog p }.

Forward Chain Extensionality:

If two programs p1 and p2 are extensionally equal, then the output of forward chain on p1 equals that on p2.

Lemma eq_fwd_chain def p1 p2 i :
p1 =i p2 → fwd_chain def p1 i = fwd_chain def p2 i.

Forward Chain Decomposition:

The result of applying forward chain on the concatenation of programs p1 and p2, given an interpretation i equals the union of forward chain on p1 given i with forward chain on p2 given i.

Lemma fwd_chain_cat def p1 p2 i :
fwd_chain def (p1 ++ p2) i = fwd_chain def p1 i :|: fwd_chain def p2 i.

Let ga be a ground atom in the output of applying forward chain on p, given i. Then, either ga is in i or its symbol among the head symbols in p.

Lemma fwd_chain_sym def pp i ga :
(ga \in fwd_chain def pp i ) →
(ga \in i ) || (sym_gatom ga \in hsym_prog pp ).

Let ga be a ground atom in the output of iterating the application of forward chain on p, given i, k times. Then, either ga is in i or its symbol is among the head symbols in p.

Lemma iter_fwd_chain_sym def pp i ga k :
(ga \in iter k (fwd_chain def pp) i ) →
(ga \in i ) || (sym_gatom ga \in hsym_prog pp ).

Atom Matching Decomposition: Let i1, i2 be two interpretations, The substitution set extending a substitution s with bindings matching a against the union of i1 and i2 equals the union of the substitution set extending s with bindings matching a against i1 with that extending s with bindings matching a against i2.

Lemma match_atom_allU s a i1 i2 :
  match_atom_all (i1 :|: i2) a s =
  match_atom_all i1 a s :|:
  match_atom_all i2 a s.

Get the head symbols from a list of atoms

Definition sym_tl tl := [seq sym_atom (val x) | x <- tl ].

Atom Matching Modularity: Let i1, i2 be two interpretations. If the symbol of an atom a does not appear among those in i2, then extending a substitution nu with bindings matching a against the union of i1 and i2 equals that of extending nu with bindings matching a against i1.

Lemma match_atom_all_strata nu a i1 i2 :
  sym_atom a \notin sym_i i2 →
  match_atom_all (i1 :|: i2) a nu =
  match_atom_all i1 a nu.

Body Matching Modularity: Let tl be an atom list and i1, i2 interpretations. If the symbols in tl do not appear in i2, then the result of matching tl against the union of i1 with i2 equals the result of matching tl against i1.

Lemma match_body_strata tl i1 i2 :
disjoint (mem (sym_tl tl)) (mem (sym_i i2)) →
match_body (i1 :|: i2) tl = match_body i1 tl.

Open Scope SET.

Forward Chain Modularity:

Let p be a program and i, ip interpretations. If i is a model for p and the symbols in p do not appear in ip, then the result of applying forward chain on p, starting from the union of i with ip adds no new facts.

Lemma fwd_chain_mod def pp i ip
      (h_tr : prog_true pp i)
      (h_strata : disjoint (mem (sym_prog pp)) (mem (sym_i ip))) :
  fwd_chain def pp (i :|: ip) = i :|: ip.

Lemmas about forward chain iteration.

Lemma iter_fwd_chain_stable def pp i k
(h_tr : prog_true pp i) :
iter k (fwd_chain def pp) i = i.

Auxiliary lemmas - Added

If we start from sp augmented with x → y, then after folding match_term on l1 and l2 (terms and ground terms), if we succeed, s the result contains the binding x → y

Starting from substitution sp. If sp binds vat to term c, after iterating on tlg and tl, the result s contains the same binding.

Lemma match_term_head_some s sp gat vat tlg (tl : seq term) c : Some s = foldl
      (fun (acc : option {ffun 'I_n → option syntax.constant })
           (p : syntax.constant × term) ⇒ obind (match_term p .1 p .2) acc)
      (match_term gat (Var vat) sp) (zip tlg tl)
      → sp vat = Some c
      → s vat = Some c.

Lemma fold_add_mapsto s sp x y l1 l2 : Some s =
      foldl (fun (acc : option {ffun 'I_n → option syntax.constant })
           (p : syntax.constant × term) ⇒ obind (match_term p .1 p .2) acc)
        (Some (add sp x y))
        (zip l1 l2)
    → s x = Some y.

Let t2 be a set of vars, t1 its complement, Let x be the substitution matching a with ga that extends sp, let s be an extension of x, if we substitute the restriction of s to t1 in a and match the result with ga starting from sp restricted to t2, then the substitution we obtain is x restricted to t2. In other word the binding of variables added by s that were outside t2 do not influence the matching.

Lemma only_untyped_match x s sp a ga (t1 t2 : {set 'I_n }) :
[disjoint t1 & t2 ] → [∀ y, ((y \in t1 ) || (y \in t2 ))] →
sub_st x s → sub_st sp s → Some x = match_atom sp a ga
→ Some (sub_filter x t2) = match_atom (sub_filter sp t2) (satom a (sub_filter s t1)) ga.

Let t2 be a set of vars, t1 its complement, s be a substitution matching the body l with i starting from ss1. Let ss1 and ss2 be set of substitution, such that any restriction of s in ss1 verifies that its restriction to t2 is in ss2. Then matching the body resulting from subsituting the restriction of s to t1 in l, on i starting from ss2 contains the same restriction of s to t2

Lemma untyped_in_scl_match_pbody l i s (t1 t2 : {set 'I_n }) (ss1 ss2 : {set sub }) :
     [∀ s' in ss1 , (s' \sub s ) ==> ((sub_filter s' t2 ) \in (pred_of_set ss2 ))]
  → s \in match_pbody l i ss1 → [∀ y, ((y \in t1 ) || (y \in t2 ))] → [disjoint t1 & t2 ]
  → (sub_filter s t2 ) \in match_pbody [seq satom a (sub_filter s t1) | a <- l ] i ss2.

Let t2 be a set of vars, t1 its complement, s be a substitution matching the body of clause cl with i. Then matching the body resulting from subsituting the restriction of s to t1 in cl, on i contains the restriction of s to t2

Lemma untyped_in_scl_match_body cl i (t1 t2 : {set 'I_n }) : ∀ s, s \in match_body i (body_cl cl) →
[disjoint t1 & t2 ] → [∀ y, ((y \in t1 ) || (y \in t2 ))]
→ (sub_filter s t2 ) \in match_body i (body_cl (scl (sub_filter s t1) cl)).

Correspondence between constructive and boolean matches -- added

If s in the result of matching the body of cl with i, then bmatch def i cl s succeeds

Lemma match_body_bmatch def (cl : clause) i s :
s \in match_body i (body_cl cl) → bmatch def i cl s.

If bmatch def i cl s succeeds, then there is a substitution r smaller than s in the result of matching the body of cl with i

Lemma bmatch_match_body def (cl : clause) i s:
  bmatch def i cl s →
        exists2 r : sub ,
         r \in match_body i (body_cl cl) & r \sub s.

End Soundness.