octalgo.third_party.bigop_aux

octalgo.octalgo.utils

• Various utilitary lemmas to reduce proof sizes
  • bool
  • nat
    • Lemmas on max
  • Finset
    • Iter is increasing
    • Disjoint
    • Equivalence partitions
    • A set that is not a singleton {x} is empty or contains y != x
  • Seq
    • Fold with max
    • rem
    • set_nth
    • sremove: trying to remove the element at a given index
    • (p)map leq size
    • all
    • nth_error: trying to get the i-th element of a seq
• Various definitions
  • • dep_iota: returning a sequence of nats as ordinals
    • Equip the elements of a set with a property
  • bigop
    • Shifting operations on ordinals
    • pset: pmap for finsets
    • Prop version of all
    • Cartesian product

octalgo.octalgo.finseqs

• uniq_seq: finite sequences, bounded by unicity
  • Definition
  • uniq_seq is a subtype of seq
  • as well as eqType, choiceType, countType and subCountType
  • constructors for uniq_seq
  • uniq_seq is a finType
• Wlist: finite sequences, with a size bounded by a nat
  • Definition
  • Canceling lemmas
  • Wlist is a type with dedicable equality
  • Wlist is a subtype of seq
  • Wlist is a choice type
  • Wlist is a count type
  • Wlist is a finite type
  • Utility lemmas and definitions for Wlist

octalgo.octalgo.fintrees

• HTrees: syntactically bounded trees
  • Trees are an equality type
  • Htree is a choice type
  • Htree is a countable type
  • Htree is a finite type
• ABTrees: generic trees with different node / leaf types
  • abtree is a countable type
• WUTree : Width and uniqueness constrained ABtrees.
  • WUtree is an finite Type
  • WUTree as a subtype
  • Utilities for WUTree

octalgo.datalogcert.syntax

• Standard Datalog in Coq
  • Hypothesis added for the development
  • Predicate kinds
  • Constants
  • Ground raw atoms
    • Ground Atom Instances
  • Ground Atoms:
  • Ground Clauses:
  • Canonical instances for ground clauses (Added)
  • Interpretation
  • Terms
  • Raw atoms
  • Atoms
  • Atoms are records packing a "raw" atom and a corresponding boolean well-formedness condition
    • A few useful lemmas and auxiliary functions
    • Atoms are a finite type
  • Clauses and programs
  • Programs are clause lists.
  • Grounding
    • Ground valuations and their application
    • Collecting Constants
    • Collecting Variables
  • Program Safety Condition
    • Safety of deduced facts (in the IDB) - added
    • No sharing of variables between clauses - added
  • Program Satisfiability

octalgo.datalogcert.subs

• Substitutions
  • Substitutions as finitely supported partial functions
  • Order on substitutions
    • Substitution Extensionality Lemma
  • Adding an elementary binding
  • Substitution on terms
  • Substitution on atoms
    • Atom Substitution Extensions Lemma:
  • Substitution on clauses
  • Non dependent grounding using default element
    • Non dependent grounding on raw atoms
    • Non dependent grounding on atoms
    • Non dependent grounding on clauses
    • From substitution to grounding
  • Domain of a substitution - modified
  • Restriction of a substitution to a set of variables (Added)

octalgo.datalogcert.pmatch

• constructive match
  • match on terms
  • Generalization to raw atoms
• boolean match - Added

octalgo.datalogcert.bSemantics

• Semantics of a Datalog program
  • Consequences of a clause
  • Semantic of a program up to m steps

octalgo.datalogcert.monotonicity

• Increasing functions

octalgo.datalogcert.soundness

• Soundness of the standard semantics
  • Term Matching Soundness:
  • Atom Matching Soundness:
  • Atom Matching Substitution Lemma:
  • Term Matching Completeness:
  • Atom Matching Completeness:
  • Lemmas on substitutions -- added
  • Domains and variables of elements
  • Clause Consequence Soundness:
  • Forward Chain Soundness:
  • Clause Consequence Stability:
  • Forward Chain Extensionality:
  • Forward Chain Decomposition:
  • Forward Chain Modularity:
  • Auxiliary lemmas - Added
  • Correspondence between constructive and boolean matches -- added

octalgo.datalogcert.fixpoint

• Fixed Points

octalgo.datalogcert.completeness

• Completeness
  • Forward Chain Completeness:

octalgo.octalgo.occurrences

• Occurrences of atoms or terms
  • Atom occurrence
  • Term occurrence
  • Atom occurrence
  • Collecting occurrences of a variable
  • Computing of occurrences of variables in terms, atoms, clauses

octalgo.octalgo.purge

• Purging a program

octalgo.octalgo.tSemantics

• Trace semantics
  • Rule grounding
  • Semantic trees (traces)
  • Trace semantics definition
  • Completeness of the trace semantic.
  • Soundness of the trace semantics
  • Utility lemmas relating tocc and the trace

octalgo.octalgo.norec_sem

• No recursion traces: extracting bounded sequences from deduction traces
  • The actual extraction
  • The sequences in the no recursion trace are disjoint from prev
  • The no recursion trace is monotonuous wrt. its fuel
  • unrec_trace_gen has a normal form wrt. its fuel
  • Core result: any value v can take in practice during an execution of p

octalgo.octalgo.static

• Static analysis of a Datalog program
  • The actual analysis
  • Completeness results on the analysis
  • the content of any sequence in the result of an analysis is disjoint
  • The analysis is monotonous wrt. its fuel
    • Core result: any no recursion trace is captured by the analysis
    • Any no recursion trace is captured in by the analysis with bounded fuel

octalgo.octalgo.rinstance

• Partially instantiating a Datalog program
  • Actual transformation
    • Instantiation of a clause by subs
  • Adequacy of the transformation
    • Completeness: the m iterate of p semantics is contained in the
    • Soundness: the m iterate of tprog semantics is contained in the
    • p and tprog semantic coincide àt each iteration

octalgo.octalgo.extract_static

• Combining the static analysis and the rule instantiation
• Definition of dependent substitutions of clauses for a typing
  • Extraction of the substitutions via the static analysis
  • Adequacy of the transformation

octalgo.octalgo.projection

• Projection over a Datalog program
  • Base hypotheses
    • a safe program p, an interpretation i
    • an intensional predicate and an argument index to project over
    • The predicate is always defined with a constant at the given index
    • A function to build new value-indexed predicates
  • Checking if a predicate or a ground atom is a clone
  • Computing the set of constants used in the definition of f
  • Cloning the different elements of the program
    • Atoms
    • Ground atoms
    • Clauses
  • Rewriting clones
  • Building the P <- P_c rules
    • Arguments
    • Atoms
    • Clauses
  • Projected program
  • Extracting substitutions for P <- P_c rules
  • Matching cloned atoms
    • Using the P <- P_c rules
  • Adequacy
    • Completeness
    • Soundness