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.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma plus_neutral_right `{SemiLattice} A B: ∀ (x: X A B), x+0 == x.
Proof. intros. rewrite plus_com; apply plus_neutral_left. Qed.
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.
Proof. intros. rewrite <- plus_assoc, (plus_com b). apply plus_assoc. Qed.
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.
Proof. intros. rewrite <- plus_assoc, (plus_com b). apply plus_assoc. Qed.
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.
Proof. reflexivity. Qed.
Lemma sum_enter_left i k (f: nat → X A B):
sum i (S k) f == f i + sum (S i) k f.
Proof. reflexivity. Qed.
Lemma sum_enter_right i k (f: nat → X A B):
sum i (S k) f == sum i k f + f (i+k)%nat.
Proof.
revert i; induction k; intro i.
simpl. rewrite plus_0_r; apply plus_com.
change (sum i (S (S k)) f) with (f i + sum (S i) (S k) f).
rewrite IHk, plus_assoc. simpl. auto with compat.
Qed.
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.
Proof. reflexivity. Qed.
Lemma sum_enter_left i k (f: nat → X A B):
sum i (S k) f == f i + sum (S i) k f.
Proof. reflexivity. Qed.
Lemma sum_enter_right i k (f: nat → X A B):
sum i (S k) f == sum i k f + f (i+k)%nat.
Proof.
revert i; induction k; intro i.
simpl. rewrite plus_0_r; apply plus_com.
change (sum i (S (S k)) f) with (f i + sum (S i) (S k) f).
rewrite IHk, plus_assoc. simpl. auto with compat.
Qed.
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: ∀ (x: X A B), 0 <== x.
Proof (@plus_neutral_left _ _ _ A B).
Lemma plus_make_left: ∀ (x y: X A B), x <== x+y.
Proof. intros; unfold leq. rewrite plus_assoc, plus_idem. reflexivity. Qed.
Lemma plus_make_right: ∀ (x y: X A B), x <== y+x.
Proof. intros; unfold leq. rewrite (plus_com y), plus_assoc, plus_idem. reflexivity. Qed.
Lemma plus_destruct_leq: ∀ (x y z : X A B), x<==z → y<==z → x+y<==z.
Proof. unfold leq; intros x y z H H'. ac_rewrite H'; trivial. Qed.
Lemma leq_destruct_plus: ∀ (x y z: X A B), x+y <== z → x<==z ∧ y<==z.
Proof.
intros x y z H; rewrite <- H; split; unfold leq.
rewrite plus_assoc, plus_idem. reflexivity.
rewrite (plus_com x), plus_assoc, plus_idem. reflexivity.
Qed.
Global Instance plus_incr:
Proper ((leq A B) ==> (leq A B) ==> (leq A B)) (plus A B).
Proof.
unfold leq; intros x x' Hx y y' Hy.
ac_rewrite Hx. ac_rewrite Hy. reflexivity.
Qed.
Lemma sup_def: ∀ (x y: X A B), (∀ z, x <== z ↔ y <== z) → x==y.
Proof.
intros x y H. apply leq_antisym.
apply <- H; reflexivity.
apply → H; reflexivity.
Qed.
Lemma inf_def: ∀ (x y: X A B), (∀ z, z <== x ↔ z <== y) → x==y.
Proof.
intros x y H. apply leq_antisym.
apply → H; reflexivity.
apply <- H; reflexivity.
Qed.
Lemma sum_compat (f f':nat → X A B) i k:
(∀ n, n<k → f (i+n)%nat == f' (i+n)%nat) → sum i k f == sum i k f'.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite IHk, E by auto with arith.
reflexivity.
Qed.
Global Instance sum_compat' i k:
Proper ((pointwise_relation nat (equal A B)) ==> (equal A B)) (sum i k).
Proof. repeat intro; auto using sum_compat. Qed.
Lemma sum_zero i k (f: nat → X A B):
(∀ n, n<k → f (i+n)%nat == 0) → sum i k f == 0.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite IHk, E by auto with arith.
apply plus_idem.
Qed.
Lemma sum_fun_zero i k :
sum i k (fun _ =>(0 : X A B)) == 0.
Proof.
rewrite sum_zero; auto.
Qed.
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.
Proof.
induction k'; simpl_sum_r.
auto with algebra.
rewrite IHk', plus_assoc.
auto with compat omega.
Qed.
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.
Proof.
induction k; simpl_sum_r.
auto with algebra.
rewrite IHk.
rewrite switch. setoid_rewrite plus_com at 6.
rewrite 2plus_assoc. reflexivity.
Qed.
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.
Proof.
intros; pattern k at 1; replace k with (S(k-n-1)+n)%nat by omega.
rewrite sum_cut.
rewrite sum_enter_left, plus_assoc.
auto with compat omega.
Qed.
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).
Proof.
induction k; simpl_sum_r; auto with compat omega.
Qed.
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'))).
Proof.
induction k'; simpl_sum_r.
apply sum_zero; reflexivity.
rewrite sum_cut_fun.
rewrite IHk'; reflexivity.
Qed.
Lemma leq_sum (f: nat → X A B) i k x:
(∃ n, i≤n ∧ n<i+k ∧ x <== f n) → x <== sum i k f.
Proof.
intros [n [? [? E]]].
rewrite E, (sum_cut_nth (n-i)) by omega.
replace (i+(n-i))%nat with n by auto with arith.
rewrite <- plus_make_left. apply plus_make_right.
Qed.
Lemma sum_leq (f : nat → X A B) i k x:
(∀ n, i ≤ n → n < i +k → f n <== x) → sum i k f <== x.
Proof.
revert x.
induction k.
intros x H. simpl_sum_r. apply plus_neutral_left.
intros x H. simpl_sum_r. rewrite (IHk x) , H.
auto using plus_destruct_leq.
auto with arith.
auto with arith.
intros; apply H; omega.
Qed.
Lemma sum_plus : ∀ (f : nat → X A B) i k a, 0 < k → sum i k f + a == sum i k (fun n ⇒ f n + a).
Proof.
induction k; intros.
omega_false.
simpl_sum_r.
destruct (eq_nat_dec 0 k).
subst. simpl_sum_r. auto with algebra.
setoid_rewrite <- IHk.
setoid_rewrite switch at 2. rewrite <- !plus_assoc, plus_idem. reflexivity.
omega.
Qed.
Lemma sum_constant : ∀ i k (a : X A B), 0 < k → sum i k (fun _ ⇒ a) == a.
Proof.
induction k; intros.
omega_false.
simpl_sum_r.
destruct (eq_nat_dec 0 k).
subst. simpl_sum_r. auto with algebra.
setoid_rewrite IHk. trivial with algebra.
omega.
Qed.
Lemma sum_collapse n (f: nat → X A B) i k:
n<k →
(∀ x, x ≠ (i+n)%nat → f x == 0) →
sum i k f == f (i+n)%nat.
Proof.
intros Hn H.
rewrite (sum_cut_nth n), 2 sum_zero by ( auto || intros; apply H ; omega).
rewrite plus_neutral_left. apply plus_neutral_right.
Qed.
Lemma sum_incr (f f': nat → X A B) i k:
(∀ n, n<k → f (i+n)%nat <== f' (i+n)%nat) → sum i k f <== sum i k f'.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite 2 sum_enter_right.
rewrite IHk, E by auto with arith.
reflexivity.
Qed.
Global Instance sum_incr' i k:
Proper ((pointwise_relation nat (leq A B)) ==> (leq A B)) (sum i k).
Proof. repeat intro; auto using sum_incr. Qed.
Lemma xif_plus: ∀ b (x y z: X A B), xif b x y + z == xif b (x+z) (y+z).
Proof. intros. destruct b; trivial. Qed.
Lemma plus_xif: ∀ b (x y z: X A B), z + xif b x y == xif b (z+x) (z+y).
Proof. intros. destruct b; trivial. Qed.
Lemma xif_sum_zero: ∀ 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).
Proof.
intros. revert i. induction k; intro i; simpl_sum_l.
apply xif_idem.
rewrite <- IHk. destruct b; auto with algebra.
Qed.
Lemma sum_fixed_xif_zero: ∀ v k b (x: X A B), v < k → b v = true → sum 0 k (fun u ⇒ xif (b u) x 0) == x.
Proof.
intros v k b x ? H. apply leq_antisym.
apply sum_leq. intros. case b. apply leq_refl. apply zero_inf.
apply leq_sum. ∃ v. rewrite H. auto with arith.
Qed.
Lemma compare_sum_xif_zero: ∀ k k' b c (x: X A B),
(∀ 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).
Proof.
intros until x; intro H. apply sum_leq. intros n _ Hn.
specialize (H _ Hn). destruct (b n). destruct (H refl_equal) as [j ? Hj].
apply leq_sum. ∃ j. rewrite Hj. auto with arith.
apply zero_inf.
Qed.
End Props1.
Implicit Arguments sum_cut_nth [[G] [SLo] [SL] A B].
Context `{SL: SemiLattice}.
Variables A B: T.
Lemma zero_inf: ∀ (x: X A B), 0 <== x.
Proof (@plus_neutral_left _ _ _ A B).
Lemma plus_make_left: ∀ (x y: X A B), x <== x+y.
Proof. intros; unfold leq. rewrite plus_assoc, plus_idem. reflexivity. Qed.
Lemma plus_make_right: ∀ (x y: X A B), x <== y+x.
Proof. intros; unfold leq. rewrite (plus_com y), plus_assoc, plus_idem. reflexivity. Qed.
Lemma plus_destruct_leq: ∀ (x y z : X A B), x<==z → y<==z → x+y<==z.
Proof. unfold leq; intros x y z H H'. ac_rewrite H'; trivial. Qed.
Lemma leq_destruct_plus: ∀ (x y z: X A B), x+y <== z → x<==z ∧ y<==z.
Proof.
intros x y z H; rewrite <- H; split; unfold leq.
rewrite plus_assoc, plus_idem. reflexivity.
rewrite (plus_com x), plus_assoc, plus_idem. reflexivity.
Qed.
Global Instance plus_incr:
Proper ((leq A B) ==> (leq A B) ==> (leq A B)) (plus A B).
Proof.
unfold leq; intros x x' Hx y y' Hy.
ac_rewrite Hx. ac_rewrite Hy. reflexivity.
Qed.
Lemma sup_def: ∀ (x y: X A B), (∀ z, x <== z ↔ y <== z) → x==y.
Proof.
intros x y H. apply leq_antisym.
apply <- H; reflexivity.
apply → H; reflexivity.
Qed.
Lemma inf_def: ∀ (x y: X A B), (∀ z, z <== x ↔ z <== y) → x==y.
Proof.
intros x y H. apply leq_antisym.
apply → H; reflexivity.
apply <- H; reflexivity.
Qed.
Lemma sum_compat (f f':nat → X A B) i k:
(∀ n, n<k → f (i+n)%nat == f' (i+n)%nat) → sum i k f == sum i k f'.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite IHk, E by auto with arith.
reflexivity.
Qed.
Global Instance sum_compat' i k:
Proper ((pointwise_relation nat (equal A B)) ==> (equal A B)) (sum i k).
Proof. repeat intro; auto using sum_compat. Qed.
Lemma sum_zero i k (f: nat → X A B):
(∀ n, n<k → f (i+n)%nat == 0) → sum i k f == 0.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite IHk, E by auto with arith.
apply plus_idem.
Qed.
Lemma sum_fun_zero i k :
sum i k (fun _ =>(0 : X A B)) == 0.
Proof.
rewrite sum_zero; auto.
Qed.
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.
Proof.
induction k'; simpl_sum_r.
auto with algebra.
rewrite IHk', plus_assoc.
auto with compat omega.
Qed.
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.
Proof.
induction k; simpl_sum_r.
auto with algebra.
rewrite IHk.
rewrite switch. setoid_rewrite plus_com at 6.
rewrite 2plus_assoc. reflexivity.
Qed.
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.
Proof.
intros; pattern k at 1; replace k with (S(k-n-1)+n)%nat by omega.
rewrite sum_cut.
rewrite sum_enter_left, plus_assoc.
auto with compat omega.
Qed.
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).
Proof.
induction k; simpl_sum_r; auto with compat omega.
Qed.
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'))).
Proof.
induction k'; simpl_sum_r.
apply sum_zero; reflexivity.
rewrite sum_cut_fun.
rewrite IHk'; reflexivity.
Qed.
Lemma leq_sum (f: nat → X A B) i k x:
(∃ n, i≤n ∧ n<i+k ∧ x <== f n) → x <== sum i k f.
Proof.
intros [n [? [? E]]].
rewrite E, (sum_cut_nth (n-i)) by omega.
replace (i+(n-i))%nat with n by auto with arith.
rewrite <- plus_make_left. apply plus_make_right.
Qed.
Lemma sum_leq (f : nat → X A B) i k x:
(∀ n, i ≤ n → n < i +k → f n <== x) → sum i k f <== x.
Proof.
revert x.
induction k.
intros x H. simpl_sum_r. apply plus_neutral_left.
intros x H. simpl_sum_r. rewrite (IHk x) , H.
auto using plus_destruct_leq.
auto with arith.
auto with arith.
intros; apply H; omega.
Qed.
Lemma sum_plus : ∀ (f : nat → X A B) i k a, 0 < k → sum i k f + a == sum i k (fun n ⇒ f n + a).
Proof.
induction k; intros.
omega_false.
simpl_sum_r.
destruct (eq_nat_dec 0 k).
subst. simpl_sum_r. auto with algebra.
setoid_rewrite <- IHk.
setoid_rewrite switch at 2. rewrite <- !plus_assoc, plus_idem. reflexivity.
omega.
Qed.
Lemma sum_constant : ∀ i k (a : X A B), 0 < k → sum i k (fun _ ⇒ a) == a.
Proof.
induction k; intros.
omega_false.
simpl_sum_r.
destruct (eq_nat_dec 0 k).
subst. simpl_sum_r. auto with algebra.
setoid_rewrite IHk. trivial with algebra.
omega.
Qed.
Lemma sum_collapse n (f: nat → X A B) i k:
n<k →
(∀ x, x ≠ (i+n)%nat → f x == 0) →
sum i k f == f (i+n)%nat.
Proof.
intros Hn H.
rewrite (sum_cut_nth n), 2 sum_zero by ( auto || intros; apply H ; omega).
rewrite plus_neutral_left. apply plus_neutral_right.
Qed.
Lemma sum_incr (f f': nat → X A B) i k:
(∀ n, n<k → f (i+n)%nat <== f' (i+n)%nat) → sum i k f <== sum i k f'.
Proof.
induction k; intro E; simpl_sum_r.
reflexivity.
rewrite 2 sum_enter_right.
rewrite IHk, E by auto with arith.
reflexivity.
Qed.
Global Instance sum_incr' i k:
Proper ((pointwise_relation nat (leq A B)) ==> (leq A B)) (sum i k).
Proof. repeat intro; auto using sum_incr. Qed.
Lemma xif_plus: ∀ b (x y z: X A B), xif b x y + z == xif b (x+z) (y+z).
Proof. intros. destruct b; trivial. Qed.
Lemma plus_xif: ∀ b (x y z: X A B), z + xif b x y == xif b (z+x) (z+y).
Proof. intros. destruct b; trivial. Qed.
Lemma xif_sum_zero: ∀ 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).
Proof.
intros. revert i. induction k; intro i; simpl_sum_l.
apply xif_idem.
rewrite <- IHk. destruct b; auto with algebra.
Qed.
Lemma sum_fixed_xif_zero: ∀ v k b (x: X A B), v < k → b v = true → sum 0 k (fun u ⇒ xif (b u) x 0) == x.
Proof.
intros v k b x ? H. apply leq_antisym.
apply sum_leq. intros. case b. apply leq_refl. apply zero_inf.
apply leq_sum. ∃ v. rewrite H. auto with arith.
Qed.
Lemma compare_sum_xif_zero: ∀ k k' b c (x: X A B),
(∀ 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).
Proof.
intros until x; intro H. apply sum_leq. intros n _ Hn.
specialize (H _ Hn). destruct (b n). destruct (H refl_equal) as [j ? Hj].
apply leq_sum. ∃ j. rewrite Hj. auto with arith.
apply zero_inf.
Qed.
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.