octalgo.octalgo.purge


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


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

Require Import Coq.Program.Equality.

Set Implicit Arguments.

Section Purge.

Purging a program

The underlying idea of this section is that if we have computed the semantic of our program and found all the values of the ith argument of atoms with symbol f, now we can look at the clauses of our program and remove all the clauses that contains atom with symbol f where the ith argument is another constant because they do not play a role in our semantics
Variable p : program.
Variable i : interp.
Variable def : syntax.constant.

A symbol
Variable f : symtype.
The index of an argument of this symbol
Variable ind : 'I_(arity f).
A set of value
Variable vals : {set syntax.constant}.

The hypothesis states that vals contains all the values of the indeth argument of f that appear in the computation of the semantics of p for interpretation i
Hypothesis vals_adeq : ∀ (c def : syntax.constant) (m : nat) (ga : gatom),
           ga \in (sem p def m i) → sym_gatom ga = f
        → nth_error (arg_gatom ga) ind = Some c
        → c \in vals.

keep_atom a filters out the atom a that have symbol f and whose indeth argument is a constant that is not in vals
Definition keep_atom (a : atom) : bool :=
  
  if (sym_atom a == f)
    then match nth_error (arg_atom a) ind with
            
          | Some (Var v) ⇒ true
            
          | Some (Val c) ⇒ c \in vals
            
          | None ⇒ false end
    else true.

We keep a clause if all its atoms in the body and the head are keepable
Definition keep_rule (cl : clause) : bool :=
  match cl with Clause hd tl ⇒
    (keep_atom hd) && all keep_atom tl end.

We define pp as the restriction of p purged of non keepable clauses
Definition pp := filter keep_rule p.

Lemma pp_p : pp \subset p.

If there is a substitution s such that s a is in the semantic of p for i, then a can be kept. (ie it will not have as ind argument something that was not captured by vals
Lemma keep_atom_sem (m : nat) (s : sub) (a : atom) : gr_atom_def def s a \in sem p def m i → keep_atom a.

if tl can be extended by s to be in the semantics of p for i, then we can keep tl.
Lemma keep_atom_tail_match (m : nat) (s : sub) (tl : seq atom) :
  s \in match_body (sem p def m i) tl → all keep_atom tl.

The semantics of the purged program contains the semantics of p
Lemma purge_sem_completeness : ∀ m, sem p def m i \subset sem pp def m i.

The semantics of the purged program is a subset of the semantics of p
Lemma purge_sem_soundness : ∀ m, sem pp def m i \subset sem p def m i.

The semantics of the program and its purged version coincide
Lemma purge_sem_adequacy : ∀ m, sem pp def m i = sem p def m i.

End Purge.