octalgo.datalogcert.subs

Second part of the original file "pengine.v" with some modifications

Require Import syntax.

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

Set Implicit Arguments.

Section Substitutions.

Substitutions

Substitutions as finitely supported partial functions

Definition sub := finfun_finType (ordinal_finType n) (option_finType cons_finType).

Coercion opt_sub (s : option sub) : (option_finType sub) := s.

empty substitution

Definition emptysub : sub := [ffun _ ⇒ None ].

For each variable, either there is a constant mapped or None

Lemma sub_elim (s:sub) v : (∃ c, s v = Some c ) ∨ (s v = None ).

Added notion of composition of substitutions: not exactly sub union as there is a priority on s1

Definition subU (s1 s2 : sub) : sub :=
[ffun v ⇒ if (s1 v) is Some c then Some c else s2 v ].

empty is neutral element for subU

Lemma subU_0l (s : sub) : subU emptysub s = s.

Lemma subU_0r (s : sub) : s = subU emptysub s.

Implicit Types (s : sub) (t : term) (a : atom) (v : 'I_n)
(b : 'I_n × syntax.constant).

Variable is mapped/free by the substitution s

Definition mem_bound s v : bool := s v.
Definition mem_free s v : bool := s v == None.

Binding b belongs to s

Definition mem_binding s b : bool := s b .1 == Some b .2.

mem_binding = \in to be used as generic predicate

Definition eqbind_class := sub.

Coercion pred_of_eq_bind (s : eqbind_class) : pred_class := [eta mem_binding s ].

Canonical mem_bind_symtype := mkPredType mem_binding.

Lemma mem_bindE s b : b \in s = (s b .1 == Some b .2 ).

Definition inE_bis := (mem_bindE , inE ).

Order on substitutions

substitution s2 extends s1

Definition sub_st s1 s2 :=
[∀ v : 'I_n , if s1 v is Some b1 then (v , b1) \in s2 else true ].

Notation "A \sub B" := (sub_st A B)
(at level 70, no associativity) : bool_scope.

reflection lemma for substitution ordering

Lemma substP s1 s2 : reflect {subset s1 ≤ s2 } (s1 \sub s2).

Substitution Extensionality Lemma

Lemma substE s1 s2 :
reflect (∀ d v, s1 v = Some d → s2 v = Some d) (s1 \sub s2).

reflexivity of substitution ordering

Lemma substss s : s \sub s.

transitivity of substitution ordering

Lemma subst_trans s1 s2 s3 : s2 \sub s3 → s1 \sub s2 → s1 \sub s3.

any substitution extends the empty substitution

Lemma subst0s s : emptysub \sub s.

Adding an elementary binding

Extending a substitution s with a binding (v,d)

Definition add s v d :=
[ffun u ⇒ if u == v then Some d else s u ].

If v was free in s, substitution extension respects ordering.

Lemma sub_add s v d : mem_free s v → s \sub (add s v d ).

Value of substitution on variable added

Lemma addE (s : sub) (v : 'I_n) d : (add s v d) v = Some d.

Adding a binding is idempotent

Lemma add_add (s : sub) v d e : (add (add s v e) v d ) = add s v d.

More lemmas: If s1 and s2 do not bind v, adding a binding on v on the composition or composing the substitution after adding v gives the same result

Lemma subU_addl v c (s1 s2 : sub) : s1 v = None → s2 v = None
→ (add (subU s1 s2) v c ) = subU (add s1 v c) s2.

If binding are on different variables we can permute the additions of those binding to s

Lemma add_com (s : sub) v1 v2 c1 c2 :
v1 ≠ v2
→ add (add s v1 c1) v2 c2 = add (add s v2 c2) v1 c1.

Substitution on terms

Term substitution

Definition sterm s t : term :=
  match t with
  | Val d ⇒ Val d
  | Var v ⇒ if s v is Some d
             then Val d
             else Var v
  end.

Empty term substitution application

Lemma emptysubE t : sterm emptysub t = t.

Substitution extension for terms

Lemma sterm_sub t s1 s2 d :
s1 \sub s2 → sterm s1 t = Val d → sterm s2 t = Val d.

Substitution on atoms

Atom substitution: applying a substiution s to a "raw" atom ra

Definition sraw_atom ra s := RawAtom (sym_atom ra) [seq sterm s x | x <- arg_atom ra ].

Given an atom a and a substitution s, the atom resulting by instantiating a with s is well-formed

Lemma satom_proof a s : wf_atom (sraw_atom a s).

Instantiation function that, for a given atom a, takes a substitution s and returns the corresponding substituted atom

Definition satom a : sub → atom := fun s ⇒ Atom (satom_proof a s).

Atom symbols are preserved by substitution instantiation

Lemma sym_satom a nu : sym_atom (satom a nu) = sym_atom a.

The ground atom that is the result of applying s to a if any

Definition atom_gr a s := { gtl : gatom | to_atom gtl = satom a s }.

Atom Substitution Extensions Lemma:

Let s1, s2 be two substitutions. If s2 extends s1 and s1 instantiates an atom a to a ground atom ga, then s2 also instantitates a to ga.

Lemma satom_sub a s1 s2 ga :
s1 \sub s2 → satom a s1 = to_atom ga → satom a s2 = to_atom ga.

The variables of the result of applying s to a are included in the variables of a

Lemma satom_vars_subset a s : atom_vars (satom a s) \subset atom_vars a.

Tail substitution

Definition stail tl s : list atom := [seq satom a s | a <- tl ].

Lifting of a ground tail to tail

Definition to_tail gtl : list atom := [seq to_atom ga | ga <- gtl ].

Grounding of atom list

Definition tail_gr tl s := { gtl : list gatom | to_tail gtl = stail tl s }.

The set of variables also decrease when we use a list of atoms.

Lemma stail_vars_subset tl s : (tail_vars [seq satom a s | a <- tl ])
\subset tail_vars tl.

Composition of substitutions giving a ground atom

Lemma satomeq_subU a ga s1 s2 :
satom (satom a s1) s2 = to_atom ga
→ satom a (subU s1 s2) = to_atom ga.

Same as above but generalized to a list of atoms (body of clause)

Lemma staileq_subU tl gtl s1 s2 :
stail [seq satom a s1 | a <- tl ] s2 = [seq to_atom ga | ga <- gtl ]
→ stail tl (subU s1 s2) = [seq to_atom ga | ga <- gtl ].

Substitution on clauses

Definition scl s (cl : clause) : clause :=
match cl with
| Clause h tl ⇒ Clause (satom h s) (wmap (fun a ⇒ satom a s) tl) end.

End Substitutions.

Export the notation

Notation "A \sub B" := (sub_st A B)
(at level 70, no associativity) : bool_scope.

Hint Resolve substss subst0s.

Non dependent grounding using default element

Section NoDepGrounding.

Implicit Types (s : sub) (t : term) (a : atom) (v : 'I_n)
(b : 'I_n × syntax.constant).

default element

Variable def : syntax.constant.

grounding a term t with a substitution s and the default element def

Definition gr_term_def s t : syntax.constant :=
  match t with
  | Val c ⇒ c
  | Var i ⇒ odflt def (s i)
  end.

We can use the above def, or first apply the definition and then ground using the empty substitution.

Lemma gr_term_def_scl_eq s t : gr_term_def s t = gr_term_def emptysub (sterm s t).

If, when instantiating a term t with a substitution s, we obtain a constant c, then we obtain c also when grounding t with s using the default element def.

Lemma gr_term_defP c t s :
sterm s t = Val c → gr_term_def s t = c.

If t1 has less variables than t2 (reminder at most one), then if s applied to t2 gives a constant, so does s applied to t1

Lemma gr_term_sub t1 t2 s d (t_sub : term_vars t1 \subset term_vars t2) :
sterm s t2 = Val d → ∃ e, sterm s t1 = Val e.

Non dependent grounding on raw atoms

grounding a raw atom ra with a substitution s and the default element def

Definition gr_raw_atom_def s ra : raw_gatom :=
RawGAtom (sym_atom ra) (map (gr_term_def s) (arg_atom ra)).

Let s1 and s2 be two substitutions. For each variable v, either s1 or s2 is undefined and the other coincide with s. Then grounding a raw atom with s2 and then s1 is the same as grounding with s

Lemma gr_raw_atom_scl_eq (s s1 s2 : sub) ra :
(∀ v, (s1 v = s v ∧ s2 v = None ) ∨ (s2 v = s v ∧ s1 v = None ))
→ gr_raw_atom_def s ra = gr_raw_atom_def s1 (sraw_atom ra s2).

Non dependent grounding on atoms

well-formedness is preserved by non-dependent grounding

Lemma gr_atom_def_proof s a : wf_gatom (gr_raw_atom_def s a).

grounding an atom a with a substitution s

Definition gr_atom_def s a : gatom := GAtom (gr_atom_def_proof s a).

Let a be an atom and s a substitution. If, when instantiating a with s, we obtain the ground atom ga, then, when grounding a with s and the default element def, we also obtain ga.

Lemma gr_atom_defP a s ga :
satom a s = to_atom ga → gr_atom_def s a = ga.

Let ga be a ground atom. If we lift it to an atom and ground it with a substitution s and a default element def, ga is preserved.

Lemma gr_atom_defK ga s : gr_atom_def s (to_atom ga) = ga.

Non dependent grounding on clauses

Definition gr_cl_def s cl :=
GClause (gr_atom_def s (head_cl cl)) (wmap (gr_atom_def s) (body_cl cl)).

From substitution to grounding

Using default value to lift a subst to a grounding

Definition to_gr s : gr := [ffun v ⇒ if s v is Some c then c else def ].

From grounding to substitution

Definition to_sub (g : gr) : sub := [ffun v ⇒ Some (g v)].

Applied to a term, a grounding gives as the associated subst

Lemma to_subE t g : sterm (to_sub g) t = Val (gr_term g t).

If s is defined on t, applying it on t gives as applying its associated grounding

Lemma to_grP t s c : sterm s t = Val c → gr_term (to_gr s) t = c.

Domain of a substitution - modified

substitution domain: set of all variables it binds (moved)

Definition dom s := [set v : 'I_n | s v ].

The domain of the empty subsitution is the empty set

Lemma dom_emptysub : dom emptysub = set0.

domain of a "singleton sub" is the relevant variable - added

Lemma dom_singlesub v c : dom (add emptysub v c) = [set v ].

equality of a "singleton sub" - added

Lemma eq_singlesub s v c :
dom s = [set v ]
→ s v = Some c
→ s = add emptysub v c.

Lemma sub_dom (s1 s2 : sub) :
s1 \sub s2 → dom s1 \subset dom s2.

If v in the domain of s, v cannot be in the result of applying s to an atom a

Lemma v_in_dom_satom v s a : v \in dom s
→ v \in atom_vars (satom a s) → False.

If v in the domain of s, v cannot be in the result of applying s to a list of atoms l.

Lemma v_in_dom_stail v s l: v \in dom s
→ v \in tail_vars [seq satom a s | a <- l ]
→ False.

If the domain of s contains all the variables of ato, then applying s as a grounding to ato with default value gr gives the same result as applying s as a regular substitution.

Lemma to_atom_satom_eq (s : sub) ato : atom_vars ato \subset dom s →
to_atom (gr_atom_def s ato) = satom ato s.

Two substitution having the same domain and such that one is smaller than the other are in fact identical.

Lemma subU_eq (s1 s2 : sub) :
dom s1 = dom s2
→ s1 \sub s2
→ s1 = s2.

For variables in the domain substitution and grounding coincide

Lemma dom_sub_grE (s : sub) (v : 'I_n) :
v \in dom s → s v = (to_sub (to_gr s)) v.

If domain of substitution is empty, then s is the empty substitution

Lemma emptymin s : dom s \subset set0 → s = emptysub.

The domain of a set of substitution is the union of the domain of its members

Definition all_dom (ss : {set sub }) := \bigcup_(s in ss ) dom s.

The domain of the set of substitution reduced to the empty substitution is empty

Lemma all_dom_empty : all_dom [set emptysub ] = set0.

Restriction of a substitution to a set of variables (Added)

Definition sub_filter (s : sub) (t : {set 'I_n }) :=
[ffun v ⇒ if v \in t then s v else None ].

The restriction has a smaller domain

Lemma sub_filter_subset_s (s : sub) (t : {set 'I_n }) :
dom (sub_filter s t) \subset dom s.

Its domain is in fact also included in t (the restriction)

Lemma sub_filter_subset_t (s : sub) (t : {set 'I_n }) :
dom (sub_filter s t) \subset t.

For v in t, if s v is defined, then so is the restriction and it gives the same result.

Lemma sub_filter_eq (s : sub) (t : {set 'I_n }) (v : 'I_n) :
v \in t → (sub_filter s t) v = s v.

Restricting a substitution to a set that contains its domain does not change the substitution

Lemma sub_sub_filter (s : sub) (sb : {set 'I_n }) :
dom s \subset sb
→ sub_filter s sb = s.

Restricting the empty sub does not change it.

Lemma utemptysub (t : {set 'I_n }) : sub_filter emptysub t = emptysub.

Let t1 and t2 disjoint, v in t1, the restriction of sp to t2 is the same as the restriction of sp augmented with a binding for v to t2

Lemma add_typed_untyped v (t1 t2 : {set 'I_n }) c sp :
(v \in t1 ) → [disjoint t1 & t2 ] →
sub_filter sp t2 = sub_filter (add sp v c) t2.

If v in ŧ2, the restriction of sp augmented with a binding for v to t2 is equal to augmenting the restriction of sp to t2 with this same binding.

Lemma add_untyped_untyped v (t : {set 'I_n }) c sp :
   v \in t
→ add (sub_filter sp t) v c = (sub_filter (add sp v c) t ).

Lemma atom_vars_sub_gr (a:atom) (s1 s2:sub) :
   atom_vars a \subset dom s1
→ s1 \sub s2
→ gr_atom (to_gr s1) a = gr_atom (to_gr s2) a.

Lemma atom_vars_sub_gr_def (a:atom) (s1 s2:sub) :
   atom_vars a \subset dom s1
→ s1 \sub s2
→ gr_atom_def s1 a = gr_atom_def s2 a.

Lemma gr_term_def_eq_in_dom s1 s2 v1 v2 :
   gr_term_def s1 (Var v1) = gr_term_def s2 (Var v2)
→ v1 \in dom s1
→ v2 \in dom s2
→ s1 v1 = s2 v2.

End NoDepGrounding.