Commit 0ac14e20 authored by Sergey Bozhko's avatar Sergey Bozhko Committed by Björn Brandenburg

Shorten a few long proofs

parent 4db8d20a
Pipeline #20638 passed with stages
in 3 minutes and 41 seconds
......@@ -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
}
}
}
......@@ -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.
......
......@@ -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.
......
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment