octalgo.datalogcert.monotonicity
The DatalogCert Library CNRS & Université Paris-Sud, Université Paris-Saclay Copyright 2016-2019 : FormalData Original authors: Véronique Benzaken Évelyne Contejean Stefania Dumbrava
Fifth part of the original file "pengine.v" with modifications
(including some names that were changed).
Require Import utils.
Require Import syntax.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import bigop_aux.
Require Import finseqs.
Set Implicit Arguments.
Implicit Types (s : sub) (t : term) (a : atom) (v : 'I_n)
(b : 'I_n × syntax.constant) (i : interp) (cl : clause).
bindS increasing for its two arguments
Lemma bindS_incr {A B : finType} (i1 i2 : {set A}) (f1 f2 : A → {set B}) :
i1 \subset i2 → (∀ x, f1 x \subset f2 x) →
bindS i1 f1 \subset bindS i2 f2.
i1 \subset i2 → (∀ x, f1 x \subset f2 x) →
bindS i1 f1 \subset bindS i2 f2.
foldS increasing (same l)
Lemma foldS_incr {A : eqType} {B : finType} (f1 f2 : A → B → {set B}) (l : seq A)
(f_incr : ∀ x y, f1 x y \subset f2 x y) :
(∀ (s1 s2 : {set B}), (s1 \subset s2) → foldS f1 s1 l \subset foldS f2 s2 l).
(f_incr : ∀ x y, f1 x y \subset f2 x y) :
(∀ (s1 s2 : {set B}), (s1 \subset s2) → foldS f1 s1 l \subset foldS f2 s2 l).
match_atom_all increasing for the interpretation
Lemma match_atom_all_incr i1 i2 s a :
i1 \subset i2 → match_atom_all i1 a s \subset match_atom_all i2 a s.
i1 \subset i2 → match_atom_all i1 a s \subset match_atom_all i2 a s.
match_body increasing for interpretation argument
Lemma match_body_incr i1 i2 cl :
i1 \subset i2 → match_body i1 (body_cl cl) \subset match_body i2 (body_cl cl).
i1 \subset i2 → match_body i1 (body_cl cl) \subset match_body i2 (body_cl cl).
cons_clause increasing for interpretation argument
Lemma cons_cl_incr (i1 i2 : interp) cl def :
i1 \subset i2 → cons_clause def cl i1 \subset cons_clause def cl i2.
i1 \subset i2 → cons_clause def cl i1 \subset cons_clause def cl i2.
fwd chain increasing for interpretation argument
fwd chain increasing for program argument
sem is increasing wrt. for each iteration
Lemma sem_m_incr (p : program) (def : syntax.constant) (m : nat) (i : interp) :
sem p def m i \subset sem p def m.+1 i.
Section Overlinear.
Lemma fwd_chain_inc i p def : i \subset fwd_chain def p i.
Lemma sem_inc i m p def : i \subset sem def p m i.
End Overlinear.
sem p def m i \subset sem p def m.+1 i.
Section Overlinear.
Lemma fwd_chain_inc i p def : i \subset fwd_chain def p i.
Lemma sem_inc i m p def : i \subset sem def p m i.
End Overlinear.
sem is increasing wrt. number of iterations