From 0ac14e20acac4b670d0b65b47a9b412504ac4916 Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 24 Sep 2019 17:06:36 +0200
Subject: [PATCH] Shorten a few long proofs
---
scripts/known-long-proofs.json | 9 ------
util/list.v | 54 ++++++++++++++++------------------
util/step_function.v | 33 ++++++++-------------
util/sum.v | 19 ++++--------
4 files changed, 44 insertions(+), 71 deletions(-)
diff --git a/scripts/known-long-proofs.json b/scripts/known-long-proofs.json
index ad88b329a..af7f5e796 100644
--- a/scripts/known-long-proofs.json
+++ b/scripts/known-long-proofs.json
@@ -300,15 +300,6 @@
},
"./util/div_mod.v": {
"divSn_cases": 54
- },
- "./util/list.v": {
- "subseq_leq_size": 52
- },
- "./util/step_function.v": {
- "exists_intermediate_point": 43
- },
- "./util/sum.v": {
- "sum_majorant_eqn": 40
}
}
}
diff --git a/util/list.v b/util/list.v
index e822d2314..db5ef24df 100644
--- a/util/list.v
+++ b/util/list.v
@@ -748,6 +748,22 @@ End Order.
(* In this section we prove some additional lemmas about sequences. *)
Section AdditionalLemmas.
+ (* First, we prove that x ∈ xs implies that xs can be split
+ into two parts such that xs = xsl ++ [::x] ++ xsr. *)
+ Lemma in_cat:
+ forall {X : eqType} (x : X) (xs : list X),
+ x \in xs -> exists xsl xsr, xs = xsl ++ [::x] ++ xsr.
+ Proof.
+ intros ? ? ? SUB.
+ induction xs; first by done.
+ move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
+ - by subst; exists [::], xs.
+ - feed IHxs; first by done.
+ clear IN; move: IHxs => [xsl [xsr EQ]].
+ by subst; exists (a::xsl), xsr.
+ Qed.
+
+
(* We define a local function max over lists using foldl and maxn. *)
Let max := foldl maxn 0.
@@ -769,41 +785,24 @@ Section AdditionalLemmas.
(* We prove that for any two sequences xs and ys the fact that xs is a subsequence
of ys implies that the size of xs is at most the size of ys. *)
Lemma subseq_leq_size:
- forall {T: eqType} (xs ys: seq T),
+ forall {X : eqType} (xs ys: seq X),
uniq xs ->
(forall x, x \in xs -> x \in ys) ->
size xs <= size ys.
Proof.
clear; intros ? ? ? UNIQ SUB.
- have Lem:
- forall a ys,
- (a \in ys) ->
- exists ysl ysr, ys = ysl ++ [::a] ++ ysr.
- { clear; intros ? ? ? SUB.
- induction ys; first by done.
- move: SUB; rewrite in_cons; move => /orP [/eqP EQ|IN].
- - by subst; exists [::], ys.
- - feed IHys; first by done.
- clear IN; move: IHys => [ysl [ysr EQ]].
- by subst; exists(a0::ysl), ysr.
- }
- have EXm: exists m, size ys <= m.
- { by exists (size ys). }
+ have EXm: exists m, size ys <= m; first by exists (size ys).
move: EXm => [m SIZEm].
move: SIZEm UNIQ SUB; move: xs ys.
- induction m.
- { intros.
- move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
+ induction m; intros.
+ { move: SIZEm; rewrite leqn0 size_eq0; move => /eqP SIZEm; subst ys.
destruct xs; first by done.
specialize (SUB s).
- feed SUB; first by rewrite in_cons; apply/orP; left.
- by done.
- }
- { intros.
- destruct xs as [ | x xs]; first by done.
- specialize (@Lem _ x ys).
- feed Lem.
- { by apply SUB; rewrite in_cons; apply/orP; left. }
+ by feed SUB; [rewrite in_cons; apply/orP; left | done].
+ }
+ { destruct xs as [ | x xs]; first by done.
+ move: (@in_cat _ x ys) => Lem.
+ feed Lem; first by apply SUB; rewrite in_cons; apply/orP; left.
move: Lem => [ysl [ysr EQ]]; subst ys.
rewrite !size_cat; simpl; rewrite -addnC add1n addSn ltnS -size_cat.
eapply IHm.
@@ -817,8 +816,7 @@ Section AdditionalLemmas.
by subst; move: NIN => /negP NIN; apply: NIN.
}
{ specialize (SUB a).
- feed SUB.
- { by rewrite in_cons; apply/orP; right. }
+ feed SUB; first by rewrite in_cons; apply/orP; right.
clear IN; move: SUB; rewrite !mem_cat; move => /orP [IN| /orP [IN|IN]].
- by apply/orP; right.
- exfalso.
diff --git a/util/step_function.v b/util/step_function.v
index c999715f6..d9ec65b8c 100644
--- a/util/step_function.v
+++ b/util/step_function.v
@@ -37,47 +37,40 @@ Section StepFunction.
Lemma exists_intermediate_point:
exists x_mid, x1 <= x_mid < x2 /\ f x_mid = y.
Proof.
- unfold is_step_function in *.
- rename H_is_interval into INT,
- H_step_function into STEP, H_between into BETWEEN.
+ rename H_is_interval into INT, H_step_function into STEP, H_between into BETWEEN.
move: x2 INT BETWEEN; clear x2.
suff DELTA:
forall delta,
f x1 <= y < f (x1 + delta) ->
- exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y. {
- move => x2 LE /andP [GEy LTy].
+ exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y.
+ { move => x2 LE /andP [GEy LTy].
exploit (DELTA (x2 - x1));
first by apply/andP; split; last by rewrite addnBA // addKn.
- by rewrite addnBA // addKn.
+ by rewrite addnBA // addKn.
}
induction delta.
- {
- rewrite addn0; move => /andP [GE0 LT0].
- by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
+ { rewrite addn0; move => /andP [GE0 LT0].
+ by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
}
- {
- move => /andP [GT LT].
+ { move => /andP [GT LT].
specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.
have LE: y <= f (x1 + delta).
- {
- move: STEP => /orP [/eqP EQ | STEP];
+ { move: STEP => /orP [/eqP EQ | STEP];
first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
rewrite [X in _ < X]addn1 ltnS in STEP.
apply: (leq_trans _ STEP).
- by rewrite addn1 -addnS ltnW.
+ by rewrite addn1 -addnS ltnW.
} clear STEP LT.
rewrite leq_eqVlt in LE.
move: LE => /orP [/eqP EQy | LT].
- {
- exists (x1 + delta); split; last by rewrite EQy.
- by apply/andP; split; [by apply leq_addr | by rewrite addnS].
+ { exists (x1 + delta); split; last by rewrite EQy.
+ by apply/andP; split; [by apply leq_addr | by rewrite addnS].
}
- {
- feed (IHdelta); first by apply/andP; split.
+ { feed (IHdelta); first by apply/andP; split.
move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
exists x_mid; split; last by done.
apply/andP; split; first by done.
- by apply: (leq_trans LT0); rewrite addnS.
+ by apply: (leq_trans LT0); rewrite addnS.
}
}
Qed.
diff --git a/util/sum.v b/util/sum.v
index 106e89008..1c61c685a 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,4 +1,4 @@
-Require Import rt.util.tactics rt.util.notation rt.util.sorting rt.util.nat.
+From rt.util Require Import tactics notation sorting nat ssromega.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
(* Lemmas about sum. *)
@@ -41,22 +41,18 @@ Section ExtraLemmas.
all (fun x => F x == 0) r = (\sum_(i <- r) F i == 0).
Proof.
destruct (all (fun x => F x == 0) r) eqn:ZERO.
- {
- move: ZERO => /allP ZERO; rewrite -leqn0.
+ - move: ZERO => /allP ZERO; rewrite -leqn0.
rewrite big_seq_cond (eq_bigr (fun x => 0));
first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
intro i; rewrite andbT; intros IN.
specialize (ZERO i); rewrite IN in ZERO.
by move: ZERO => /implyP ZERO; apply/eqP; apply ZERO.
- }
- {
- apply negbT in ZERO; rewrite -has_predC in ZERO.
+ - apply negbT in ZERO; rewrite -has_predC in ZERO.
move: ZERO => /hasP ZERO; destruct ZERO as [x IN NEQ]; simpl in NEQ.
rewrite (big_rem x) /=; last by done.
symmetry; apply negbTE; rewrite neq_ltn; apply/orP; right.
apply leq_trans with (n := F x); last by apply leq_addr.
by rewrite lt0n.
- }
Qed.
Lemma leq_sum1_smaller_range m n (P Q: pred nat) a b:
@@ -141,7 +137,7 @@ Section ExtraLemmas.
intros.
rewrite big_mkcond [in X in _ <= X]big_mkcond//= leq_sum //.
intros i _.
- destruct P1 eqn:P1a; destruct P2 eqn:P2a; [by done | | by done | by done].
+ destruct P1 eqn:P1a; destruct P2 eqn:P2a; try done.
exfalso.
move: P1a P2a => /eqP P1a /eqP P2a.
rewrite eqb_id in P1a; rewrite eqbF_neg in P2a.
@@ -209,7 +205,6 @@ Section ExtraLemmas.
\sum_(x <- xs | P x) F1 x = \sum_(x <- xs | P x) F2 x ->
(forall x, x \in xs -> P x -> F1 x = F2 x).
Proof.
- clear.
intros T xs F1 F2 P H1 H2 x IN PX.
induction xs; first by done.
have Fact: \sum_(j <- xs | P j) F1 j <= \sum_(j <- xs | P j) F2 j.
@@ -223,11 +218,7 @@ Section ExtraLemmas.
by rewrite in_cons; apply/orP; right. }
rewrite big_cons [RHS]big_cons in H2.
have EqLeq: forall a b c d, a + b = c + d -> a <= c -> b >= d.
- { clear; intros.
- rewrite leqNgt; apply/negP; intros H1.
- move: H => /eqP; rewrite eqn_leq; move => /andP [LE GE].
- move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
- by apply leq_trans with (a + d); [rewrite ltn_add2l | rewrite leq_add2r]. }
+ { clear; intros; ssromega. }
move: IN; rewrite in_cons; move => /orP [/eqP EQ | IN].
{ subst a.
rewrite PX in H2.
--
GitLab