Library ATBR.SemiLattice
Properties, definitions, hints and tactics for semilattices.
In particular, the tactic ac_rewrite allows to rewrite closed
equations modulo associativity and commutativity
Require Import Common.
Require Import Classes.
Require Import Graph.
Lemma plus_neutral_right `{SemiLattice} A B: forall (x: X A B), x+0 == x.
Hints
Hint Extern 0 (leq _ _ _ _) => apply leq_refl.
Hint Extern 0 (equal _ _ _ _) => first [
apply plus_assoc
| apply plus_com
| apply plus_idem
| apply plus_neutral_left
| apply plus_neutral_right
]: algebra.
Hint Extern 2 (equal _ _ _ _) => first [
apply plus_compat; instantiate
]: compat algebra.
Hint Rewrite @plus_neutral_left @plus_neutral_right @plus_idem using ti_auto: simpl.
Ltac fold_leq := match goal with |- equal ?A ?B (?a + ?b) ?b => change (leq A B a b) end.
Hint Extern 0 (equal _ _ _ _) => first [
apply plus_assoc
| apply plus_com
| apply plus_idem
| apply plus_neutral_left
| apply plus_neutral_right
]: algebra.
Hint Extern 2 (equal _ _ _ _) => first [
apply plus_compat; instantiate
]: compat algebra.
Hint Rewrite @plus_neutral_left @plus_neutral_right @plus_idem using ti_auto: simpl.
Ltac fold_leq := match goal with |- equal ?A ?B (?a + ?b) ?b => change (leq A B a b) end.
simple tactic for closed rewriting modulo AC, in Ltac
Lemma switch `{SemiLattice} A B (a b c : X A B) : (a+b)+c == (a+c)+b.
Ltac peigne a b n :=
match goal with
| |- context [?q + b] =>
match q with
| context [a] => ( peigne_aux (q+b) a b ) ; (try set (n := a+b))
end
| |- context [?q + a] =>
match q with
| context [b] => ( peigne_aux (q+a) b a ) ; try (rewrite (plus_com b a); set (n := a+b))
end
| _ => fail 0 "failed to find " a " and " b " in the goal"
end
with
peigne_aux q a b :=
match q with
| (?q'+a)+b => rewrite <- (plus_assoc q' a b)
| (?q'+?x)+b => rewrite (switch q' x b); peigne_aux (q' +b) a b
| a+b => idtac
| ?q' + ?x => peigne_aux q' a b
| ?x => fail x end.
Ltac atomic a :=
match a with | _ + _ => fail 1 | _ => idtac end.
Ltac agglomere_motif pat n :=
match pat with
| ?pat' + ?a => atomic a;
let x := fresh "pat" in
let x' := fresh "pat_plus_a" in
(agglomere_motif pat' x;
peigne x a x';
subst x; set (n := x'); subst x')
| ?a => atomic a; set (n := a)
| _ => fail 0 "failed to find the term: " pat
end.
Ltac ac_rewrite Li :=
rewrite ?plus_assoc;
lazymatch type of Li with
| ?pat == _ =>
(let n := fresh "ac_rewrite" in agglomere_motif pat n;
subst n; rewrite Li
) || fail "failed to gather the pattern."
| ?pat <== _ =>
(let n := fresh "ac_rewrite" in agglomere_motif pat n;
subst n; rewrite Li
) || fail "failed to gather the pattern."
| ?x => fail "Not an (in)equality: " Li ": " x
end.
Ltac peigne a b n :=
match goal with
| |- context [?q + b] =>
match q with
| context [a] => ( peigne_aux (q+b) a b ) ; (try set (n := a+b))
end
| |- context [?q + a] =>
match q with
| context [b] => ( peigne_aux (q+a) b a ) ; try (rewrite (plus_com b a); set (n := a+b))
end
| _ => fail 0 "failed to find " a " and " b " in the goal"
end
with
peigne_aux q a b :=
match q with
| (?q'+a)+b => rewrite <- (plus_assoc q' a b)
| (?q'+?x)+b => rewrite (switch q' x b); peigne_aux (q' +b) a b
| a+b => idtac
| ?q' + ?x => peigne_aux q' a b
| ?x => fail x end.
Ltac atomic a :=
match a with | _ + _ => fail 1 | _ => idtac end.
Ltac agglomere_motif pat n :=
match pat with
| ?pat' + ?a => atomic a;
let x := fresh "pat" in
let x' := fresh "pat_plus_a" in
(agglomere_motif pat' x;
peigne x a x';
subst x; set (n := x'); subst x')
| ?a => atomic a; set (n := a)
| _ => fail 0 "failed to find the term: " pat
end.
Ltac ac_rewrite Li :=
rewrite ?plus_assoc;
lazymatch type of Li with
| ?pat == _ =>
(let n := fresh "ac_rewrite" in agglomere_motif pat n;
subst n; rewrite Li
) || fail "failed to gather the pattern."
| ?pat <== _ =>
(let n := fresh "ac_rewrite" in agglomere_motif pat n;
subst n; rewrite Li
) || fail "failed to gather the pattern."
| ?x => fail "Not an (in)equality: " Li ": " x
end.
finite sums and their properties
Section FSumDef.
Context `{SL: SemiLattice}.
Variables A B: T.
Fixpoint sum i k (f: nat -> X A B): X A B :=
match k in nat return X A B with
| 0 => 0
| S k => f i + sum (S i) k f
end.
Lemma sum_empty i (f: nat -> X A B): sum i 0 f == 0.
Lemma sum_enter_left i k (f: nat -> X A B):
sum i (S k) f == f i + sum (S i) k f.
Lemma sum_enter_right i k (f: nat -> X A B):
sum i (S k) f == sum i k f + f (i+k)%nat.
End FSumDef.
Opaque sum.
Ltac simpl_sum_r := simpl; repeat setoid_rewrite sum_empty; repeat setoid_rewrite sum_enter_right.
Ltac simpl_sum_l := simpl; repeat setoid_rewrite sum_empty; repeat setoid_rewrite sum_enter_left.
Context `{SL: SemiLattice}.
Variables A B: T.
Fixpoint sum i k (f: nat -> X A B): X A B :=
match k in nat return X A B with
| 0 => 0
| S k => f i + sum (S i) k f
end.
Lemma sum_empty i (f: nat -> X A B): sum i 0 f == 0.
Lemma sum_enter_left i k (f: nat -> X A B):
sum i (S k) f == f i + sum (S i) k f.
Lemma sum_enter_right i k (f: nat -> X A B):
sum i (S k) f == sum i k f + f (i+k)%nat.
End FSumDef.
Opaque sum.
Ltac simpl_sum_r := simpl; repeat setoid_rewrite sum_empty; repeat setoid_rewrite sum_enter_right.
Ltac simpl_sum_l := simpl; repeat setoid_rewrite sum_empty; repeat setoid_rewrite sum_enter_left.
various properties of semilattices and finite sums
Section Props1.
Context `{SL: SemiLattice}.
Variables A B: T.
Lemma zero_inf: forall (x: X A B), 0 <== x.
Lemma plus_make_left: forall (x y: X A B), x <== x+y.
Lemma plus_make_right: forall (x y: X A B), x <== y+x.
Lemma plus_destruct_leq: forall (x y z : X A B), x<==z -> y<==z -> x+y<==z.
Lemma leq_destruct_plus: forall (x y z: X A B), x+y <== z -> x<==z /\ y<==z.
Global Instance plus_incr:
Proper ((leq A B) ==> (leq A B) ==> (leq A B)) (plus A B).
Lemma sup_def: forall (x y: X A B), (forall z, x <== z <-> y <== z) -> x==y.
Lemma inf_def: forall (x y: X A B), (forall z, z <== x <-> z <== y) -> x==y.
Lemma sum_compat (f f':nat -> X A B) i k:
(forall n, n<k -> f (i+n)%nat == f' (i+n)%nat) -> sum i k f == sum i k f'.
Global Instance sum_compat' i k:
Proper ((pointwise_relation nat (equal A B)) ==> (equal A B)) (sum i k).
Lemma sum_zero i k (f: nat -> X A B):
(forall n, n<k -> f (i+n)%nat == 0) -> sum i k f == 0.
Lemma sum_fun_zero i k :
sum i k (fun _ =>(0 : X A B)) == 0.
Lemma sum_cut k' i k (f: nat -> X A B):
sum i (k'+k) f == sum i k f + sum (k+i) k' f.
Lemma sum_cut_fun i k (f g: nat -> X A B):
sum i k (fun u => f u + g u) == sum i k f + sum i k g.
Lemma sum_cut_nth n (f: nat -> X A B) i k:
n<k -> sum i k f == sum i n f + f (i+n)%nat + sum (i+S n) (k-n-1) f.
Implicit Arguments sum_cut_nth [].
Lemma sum_shift d (f: nat -> X A B) i k:
sum (i+d) k f == sum i k (fun u => f (u+d)%nat).
Theorem sum_inversion (f: nat -> nat -> X A B) i i' k k':
sum i k (fun u => (sum i' k' (f u)))
== sum i' k' (fun u'=> (sum i k (fun u => f u u'))).
Lemma leq_sum (f: nat -> X A B) i k x:
(exists n, i<=n /\ n<i+k /\ x <== f n) -> x <== sum i k f.
Lemma sum_leq (f : nat -> X A B) i k x:
(forall n, i <= n -> n < i +k -> f n <== x) -> sum i k f <== x.
Lemma sum_plus : forall (f : nat -> X A B) i k a, 0 < k -> sum i k f + a == sum i k (fun n => f n + a).
Lemma sum_constant : forall i k (a : X A B), 0 < k -> sum i k (fun _ => a) == a.
Lemma sum_collapse n (f: nat -> X A B) i k:
n<k ->
(forall x, x <> (i+n)%nat -> f x == 0) ->
sum i k f == f (i+n)%nat.
Lemma sum_incr (f f': nat -> X A B) i k:
(forall n, n<k -> f (i+n)%nat <== f' (i+n)%nat) -> sum i k f <== sum i k f'.
Global Instance sum_incr' i k:
Proper ((pointwise_relation nat (leq A B)) ==> (leq A B)) (sum i k).
Lemma xif_plus: forall b (x y z: X A B), xif b x y + z == xif b (x+z) (y+z).
Lemma plus_xif: forall b (x y z: X A B), z + xif b x y == xif b (z+x) (z+y).
Lemma xif_sum_zero: forall b i k (f: nat -> X A B), xif b (sum i k f) 0 == sum i k (fun j => xif b (f j) 0).
Lemma sum_fixed_xif_zero: forall v k b (x: X A B), v < k -> b v = true -> sum 0 k (fun u => xif (b u) x 0) == x.
Lemma compare_sum_xif_zero: forall k k' b c (x: X A B),
(forall i, i < k -> b i = true -> exists2 j, j < k' & c j = true) ->
sum 0 k (fun i => xif (b i) x 0) <== sum 0 k' (fun j => xif (c j) x 0).
End Props1.
Implicit Arguments sum_cut_nth [[G] [SLo] [SL] A B].
Context `{SL: SemiLattice}.
Variables A B: T.
Lemma zero_inf: forall (x: X A B), 0 <== x.
Lemma plus_make_left: forall (x y: X A B), x <== x+y.
Lemma plus_make_right: forall (x y: X A B), x <== y+x.
Lemma plus_destruct_leq: forall (x y z : X A B), x<==z -> y<==z -> x+y<==z.
Lemma leq_destruct_plus: forall (x y z: X A B), x+y <== z -> x<==z /\ y<==z.
Global Instance plus_incr:
Proper ((leq A B) ==> (leq A B) ==> (leq A B)) (plus A B).
Lemma sup_def: forall (x y: X A B), (forall z, x <== z <-> y <== z) -> x==y.
Lemma inf_def: forall (x y: X A B), (forall z, z <== x <-> z <== y) -> x==y.
Lemma sum_compat (f f':nat -> X A B) i k:
(forall n, n<k -> f (i+n)%nat == f' (i+n)%nat) -> sum i k f == sum i k f'.
Global Instance sum_compat' i k:
Proper ((pointwise_relation nat (equal A B)) ==> (equal A B)) (sum i k).
Lemma sum_zero i k (f: nat -> X A B):
(forall n, n<k -> f (i+n)%nat == 0) -> sum i k f == 0.
Lemma sum_fun_zero i k :
sum i k (fun _ =>(0 : X A B)) == 0.
Lemma sum_cut k' i k (f: nat -> X A B):
sum i (k'+k) f == sum i k f + sum (k+i) k' f.
Lemma sum_cut_fun i k (f g: nat -> X A B):
sum i k (fun u => f u + g u) == sum i k f + sum i k g.
Lemma sum_cut_nth n (f: nat -> X A B) i k:
n<k -> sum i k f == sum i n f + f (i+n)%nat + sum (i+S n) (k-n-1) f.
Implicit Arguments sum_cut_nth [].
Lemma sum_shift d (f: nat -> X A B) i k:
sum (i+d) k f == sum i k (fun u => f (u+d)%nat).
Theorem sum_inversion (f: nat -> nat -> X A B) i i' k k':
sum i k (fun u => (sum i' k' (f u)))
== sum i' k' (fun u'=> (sum i k (fun u => f u u'))).
Lemma leq_sum (f: nat -> X A B) i k x:
(exists n, i<=n /\ n<i+k /\ x <== f n) -> x <== sum i k f.
Lemma sum_leq (f : nat -> X A B) i k x:
(forall n, i <= n -> n < i +k -> f n <== x) -> sum i k f <== x.
Lemma sum_plus : forall (f : nat -> X A B) i k a, 0 < k -> sum i k f + a == sum i k (fun n => f n + a).
Lemma sum_constant : forall i k (a : X A B), 0 < k -> sum i k (fun _ => a) == a.
Lemma sum_collapse n (f: nat -> X A B) i k:
n<k ->
(forall x, x <> (i+n)%nat -> f x == 0) ->
sum i k f == f (i+n)%nat.
Lemma sum_incr (f f': nat -> X A B) i k:
(forall n, n<k -> f (i+n)%nat <== f' (i+n)%nat) -> sum i k f <== sum i k f'.
Global Instance sum_incr' i k:
Proper ((pointwise_relation nat (leq A B)) ==> (leq A B)) (sum i k).
Lemma xif_plus: forall b (x y z: X A B), xif b x y + z == xif b (x+z) (y+z).
Lemma plus_xif: forall b (x y z: X A B), z + xif b x y == xif b (z+x) (z+y).
Lemma xif_sum_zero: forall b i k (f: nat -> X A B), xif b (sum i k f) 0 == sum i k (fun j => xif b (f j) 0).
Lemma sum_fixed_xif_zero: forall v k b (x: X A B), v < k -> b v = true -> sum 0 k (fun u => xif (b u) x 0) == x.
Lemma compare_sum_xif_zero: forall k k' b c (x: X A B),
(forall i, i < k -> b i = true -> exists2 j, j < k' & c j = true) ->
sum 0 k (fun i => xif (b i) x 0) <== sum 0 k' (fun j => xif (c j) x 0).
End Props1.
Implicit Arguments sum_cut_nth [[G] [SLo] [SL] A B].
Hints
Hint Extern 1 (equal _ _ _ _) => first [
apply sum_compat
]: compat algebra.
Hint Extern 0 (leq _ _ _ _) => first [
apply plus_destruct_leq
| apply plus_make_left
| apply plus_make_right
| apply zero_inf
]: algebra.
Hint Extern 1 (leq _ _ _ _) => first [
apply sum_incr
]: compat algebra.
Hint Extern 2 (leq _ _ _ _) => first [
apply plus_incr
]: compat algebra.