Skip to content
Snippets Groups Projects
Commit cd82d629 authored by MathisBD's avatar MathisBD
Browse files

push_negs first version

parent 6db6bb1e
No related branches found
No related tags found
No related merge requests found
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
Require Import Bool. Require Import Bool.
Require Import Arith.Div2. Require Import Arith.Div2.
Require Import Lia Field. Require Import Lia Field.
Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def. Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def Ranalysis.
Require Import List. Require Import List.
Require Import SetoidList. Require Import SetoidList.
Require Import Relations. Require Import Relations.
...@@ -69,7 +69,7 @@ Ltac change_RHS E := ...@@ -69,7 +69,7 @@ Ltac change_RHS E :=
____ ____
Q Q
After completing this proof, Q becomes a hypothesis in the context. *) After completing this proof, Q becomes a hypothesis in the context. *)
Ltac feed H := Ltac feed H :=
match type of H with match type of H with
| ?foo -> _ => | ?foo -> _ =>
let FOO := fresh in let FOO := fresh in
...@@ -659,3 +659,179 @@ case (Nat.Even_or_Odd n) as [[k ->] | [k ->]]. ...@@ -659,3 +659,179 @@ case (Nat.Even_or_Odd n) as [[k ->] | [k ->]].
+ rewrite Nat.add_1_r, Nat.div2_succ_double. lia. + rewrite Nat.add_1_r, Nat.div2_succ_double. lia.
+ rewrite 2 Nat.add_1_r. cbn -[Nat.mul]. rewrite Nat.div2_double. lia. + rewrite 2 Nat.add_1_r. cbn -[Nat.mul]. rewrite Nat.div2_double. lia.
Qed. Qed.
Lemma Rmin_nonneg (x y : R) : (0 <= x)%R -> (0 <= y)%R -> (0 <= Rmin x y)%R.
Proof. intros. unfold Rmin. destruct (Rle_dec x y) ; assumption. Qed.
Lemma Rmax_nonneg_left (x y : R) : (0 <= x)%R -> (0 <= Rmax x y)%R.
Proof. intros. transitivity x ; [assumption | apply Rmax_l]. Qed.
Lemma Rmax_nonneg_right (x y : R) : (0 <= y)%R -> (0 <= Rmax x y)%R.
Proof. intros. transitivity y ; [assumption | apply Rmax_r]. Qed.
Lemma Rmax_pos_left (x y : R) : (0 < x)%R -> (0 < Rmax x y)%R.
Proof. intros. apply (Rlt_le_trans _ x) ; [assumption | apply Rmax_l]. Qed.
Lemma Rmax_pos_right (x y : R) : (0 < y)%R -> (0 < Rmax x y)%R.
Proof. intros. apply (Rlt_le_trans _ y) ; [assumption | apply Rmax_r]. Qed.
Ltac pos_R_close := solve [ easy | lra | nra | lia | nia ].
(* Attempt to prove a goal of the form 0%R < ?X or 0%R <= ?X. *)
(* This either fails or succeeds completely (i.e. it does not leave any subgoal open). *)
(* If you have inequalities you would want pos_R to use, consider using generalize before pos_R. *)
Ltac pos_R :=
match goal with
(* Using hypotheses. *)
| [ |- _ -> _] => intros ; pos_R
| [ H : ?P |- ?P ] => exact H
(* Change Rgt/Rge to Rlt/Rle. *)
| [ |- (_ > _)%R ] => apply Rlt_gt ; pos_R
| [ |- (_ >= _)%R ] => apply Rle_ge ; pos_R
(* Addition. *)
| [ |- (0 < ?X + ?Y)%R ] =>
solve [ apply Rplus_lt_0_compat ; pos_R
| apply Rplus_lt_le_0_compat ; pos_R
| apply Rplus_le_lt_0_compat ; pos_R ]
| [ |- (0 <= ?X + ?Y)%R ] => apply Rplus_le_le_0_compat ; pos_R
(* Multiplication. *)
| [ |- (0 < ?X * ?Y)%R ] => apply Rmult_lt_0_compat ; pos_R
| [ |- (0 <= ?X * ?Y)%R ] => apply Rmult_le_pos ; pos_R
(* Inverse. *)
| [ |- (0 < / _)%R ] => apply Rinv_0_lt_compat ; pos_R
(* Division. *)
| [ |- (0 < _ / _)%R ] => apply Rdiv_lt_0_compat ; pos_R
| [ |- (0 <= _ / _)%R ] => apply Rdiv_le_0_compat ; pos_R
(* Square. *)
| [ |- (0 < Rsqr _)%R ] => apply Rlt_0_sqr ; pos_R_close
| [ |- (0 <= Rsqr _)%R ] => apply Rle_0_sqr ; pos_R_close
(* Absolute value. *)
| [ |- (0 < Rabs _)%R ] => apply Rabs_pos_lt ; pos_R_close
| [ |- (0 <= Rabs _)%R ] => apply Rabs_pos ; pos_R_close
(* Norm. *)
| [ |- (0 <= norm _)%R ] => apply norm_nonneg ; pos_R_close
(* Distance. *)
| [ |- (0 <= dist _ _)%R ] => apply dist_nonneg ; pos_R_close
(* Exponential. *)
| [ |- (0 < exp _)%R ] => apply exp_pos ; pos_R_close
| [ |- (0 <= exp _)%R ] => apply Rlt_le, exp_pos ; pos_R_close
(* INR. *)
| [ |- (0 < INR _)%R ] => apply lt_0_INR ; pos_R_close
| [ |- (0 <= INR _)%R ] => apply pos_INR ; pos_R_close
(* Minimum. *)
| [ |- (0 < Rmin _ _)%R ] => apply Rmin_pos ; pos_R
| [ |- (0 <= Rmin _ _)%R ] => apply Rmin_nonneg ; pos_R
(* Maximum. *)
| [ |- (0 < Rmax _ _)%R ] =>
solve [ apply Rmax_pos_left ; pos_R
| apply Rmax_pos_right ; pos_R ]
| [ |- (0 <= Rmax _ _)%R ] =>
solve [ apply Rmax_nonneg_left ; pos_R
| apply Rmax_nonneg_right ; pos_R ]
(* Strengthen Rle to Rlt. *)
| [ |- (_ <= _)%R ] => apply Rlt_le ; pos_R
(* Try to close the goal with lra/nra. *)
| _ => pos_R_close
end.
(* A tactic to push negations in the goal/a hypothesis. *)
Section PushNegs.
Inductive PNProp :=
| PNvar (x : nat)
| PNtrue
| PNfalse
| PNnot (a : PNProp)
| PNand (a : PNProp) (b : PNProp)
| PNor (a : PNProp) (b : PNProp).
(* Turn a PNProp into a real Prop, assuming interpretations for the variables. *)
Fixpoint eval_pn (l : list Prop) (p : PNProp) : Prop :=
match p with
| PNvar x => List.nth x l True
| PNtrue => True
| PNfalse => False
| PNnot a => ~ eval_pn l a
| PNand a b => eval_pn l a /\ eval_pn l b
| PNor a b => eval_pn l a \/ eval_pn l b
end.
(* Implement push-neg on PNProp. *)
(* The bool parameter determines the formula we are working on :
* [p] (when neg = false) or [PNnot p] (when neg = true). *)
Fixpoint push_neg_pn (neg : bool) (p : PNProp) : PNProp :=
match neg, p with
| true, PNvar x => PNnot (PNvar x)
| true, PNtrue => PNfalse
| true, PNfalse => PNtrue
| true, (PNnot a) => push_neg_pn false a
| true, (PNand a b) => PNor (push_neg_pn true a) (push_neg_pn true b)
| true, (PNor a b) => PNand (push_neg_pn true a) (push_neg_pn true b)
| false, PNnot a => push_neg_pn true a
| false, a => a
end.
Lemma pn_correct p l :
(eval_pn l p <-> eval_pn l (push_neg_pn false p)).
Proof. Admitted.
Ltac list_add a l :=
let rec aux a l n :=
lazymatch l with
| nil => constr:((n, List.cons a l))
| a :: _ => constr :((n, l))
| ?x :: ?l =>
match aux a l (S n) with
| (?n , ?l) => constr:((n, List.cons x l))
end
end
in aux a l O.
(* Turn a Prop into a PNProp. *)
Ltac reify_aux t l :=
lazymatch t with
| True => constr:((PNtrue, l))
| False => constr:((PNfalse, l))
| ~ ?t1 =>
match reify_aux t1 l with
| (?p1, ?l') => constr:((PNnot p1, l'))
end
| ?t1 /\ ?t2 =>
match reify_aux t1 l with
| (?p1, ?l') =>
match reify_aux t2 l' with
| (?p2, ?l'') => constr:((PNand p1 p2, l''))
end
end
| ?t1 \/ ?t2 =>
match reify_aux t1 l with
| (?p1, ?l') =>
match reify_aux t2 l' with
| (?p2, ?l'') => constr:((PNor p1 p2, l''))
end
end
| _ =>
match list_add t l with
| (?n, ?l') => constr:((PNvar n, l'))
end
end.
Ltac reify t := reify_aux t (@nil Prop).
Ltac push_negs :=
lazymatch goal with
| [ |- ?P ] =>
lazymatch type of P with
| Prop =>
lazymatch reify P with
| (?t, ?l) =>
change (eval_pn l t) ;
rewrite pn_correct ;
cbn [eval_pn push_neg_pn nth]
end
end
end.
Lemma test (A : Prop) (B : nat -> Prop) : ~(A /\ ~B 0%nat).
Proof. push_negs.
...@@ -717,80 +717,6 @@ Proof. Admitted. ...@@ -717,80 +717,6 @@ Proof. Admitted.
Section WeberFirstOrder. Section WeberFirstOrder.
Lemma Rmin_nonneg (x y : R) : (0 <= x)%R -> (0 <= y)%R -> (0 <= Rmin x y)%R.
Proof. intros. unfold Rmin. destruct (Rle_dec x y) ; assumption. Qed.
Lemma Rmax_nonneg_left (x y : R) : (0 <= x)%R -> (0 <= Rmax x y)%R.
Proof. intros. transitivity x ; [assumption | apply Rmax_l]. Qed.
Lemma Rmax_nonneg_right (x y : R) : (0 <= y)%R -> (0 <= Rmax x y)%R.
Proof. intros. transitivity y ; [assumption | apply Rmax_r]. Qed.
Lemma Rmax_pos_left (x y : R) : (0 < x)%R -> (0 < Rmax x y)%R.
Proof. intros. apply (Rlt_le_trans _ x) ; [assumption | apply Rmax_l]. Qed.
Lemma Rmax_pos_right (x y : R) : (0 < y)%R -> (0 < Rmax x y)%R.
Proof. intros. apply (Rlt_le_trans _ y) ; [assumption | apply Rmax_r]. Qed.
Ltac pos_R_close := solve [ easy | lra | nra | lia | nia ].
(* Attempt to prove a goal of the form 0%R < ?X or 0%R <= ?X. *)
(* This either fails or succeeds completely (i.e. it does not leave any subgoal open). *)
(* If you have inequalities you would want pos_R to use, consider using generalize before pos_R. *)
Ltac pos_R :=
match goal with
(* Using hypotheses. *)
| [ |- _ -> _] => intros ; pos_R
| [ H : ?P |- ?P ] => exact H
(* Change Rgt/Rge to Rlt/Rle. *)
| [ |- (_ > _)%R ] => apply Rlt_gt ; pos_R
| [ |- (_ >= _)%R ] => apply Rle_ge ; pos_R
(* Addition. *)
| [ |- (0 < ?X + ?Y)%R ] =>
solve [ apply Rplus_lt_0_compat ; pos_R
| apply Rplus_lt_le_0_compat ; pos_R
| apply Rplus_le_lt_0_compat ; pos_R ]
| [ |- (0 <= ?X + ?Y)%R ] => apply Rplus_le_le_0_compat ; pos_R
(* Multiplication. *)
| [ |- (0 < ?X * ?Y)%R ] => apply Rmult_lt_0_compat ; pos_R
| [ |- (0 <= ?X * ?Y)%R ] => apply Rmult_le_pos ; pos_R
(* Inverse. *)
| [ |- (0 < / _)%R ] => apply Rinv_0_lt_compat ; pos_R
(* Division. *)
| [ |- (0 < _ / _)%R ] => apply Rdiv_lt_0_compat ; pos_R
| [ |- (0 <= _ / _)%R ] => apply Rdiv_le_0_compat ; pos_R
(* Square. *)
| [ |- (0 < Rsqr _)%R ] => apply Rlt_0_sqr ; pos_R_close
| [ |- (0 <= Rsqr _)%R ] => apply Rle_0_sqr ; pos_R_close
(* Absolute value. *)
| [ |- (0 < Rabs _)%R ] => apply Rabs_pos_lt ; pos_R_close
| [ |- (0 <= Rabs _)%R ] => apply Rabs_pos ; pos_R_close
(* Norm. *)
| [ |- (0 <= norm _)%R ] => apply norm_nonneg ; pos_R_close
(* Distance. *)
| [ |- (0 <= dist _ _)%R ] => apply dist_nonneg ; pos_R_close
(* Exponential. *)
| [ |- (0 < exp _)%R ] => apply exp_pos ; pos_R_close
| [ |- (0 <= exp _)%R ] => apply Rlt_le, exp_pos ; pos_R_close
(* INR. *)
| [ |- (0 < INR _)%R ] => apply lt_0_INR ; pos_R_close
| [ |- (0 <= INR _)%R ] => apply pos_INR ; pos_R_close
(* Minimum. *)
| [ |- (0 < Rmin _ _)%R ] => apply Rmin_pos ; pos_R
| [ |- (0 <= Rmin _ _)%R ] => apply Rmin_nonneg ; pos_R
(* Maximum. *)
| [ |- (0 < Rmax _ _)%R ] =>
solve [ apply Rmax_pos_left ; pos_R
| apply Rmax_pos_right ; pos_R ]
| [ |- (0 <= Rmax _ _)%R ] =>
solve [ apply Rmax_nonneg_left ; pos_R
| apply Rmax_nonneg_right ; pos_R ]
(* Strengthen Rle to Rlt. *)
| [ |- (_ <= _)%R ] => apply Rlt_le ; pos_R
(* Try to close the goal with lra/nra. *)
| _ => pos_R_close
end.
Variables (w : R2) (ps : list R2). Variables (w : R2) (ps : list R2).
(* The points in ps that are not equal to w. *) (* The points in ps that are not equal to w. *)
...@@ -1411,25 +1337,25 @@ Lemma deriv_scale (eps : R2) (s : R) : ...@@ -1411,25 +1337,25 @@ Lemma deriv_scale (eps : R2) (s : R) :
(deriv (s * eps) = Rabs s * deriv eps)%R. (deriv (s * eps) = Rabs s * deriv eps)%R.
Admitted. Admitted.
Lemma deriv_neg_not_weber (eps : R2) : (* If we can find a direction eps such that deriv eps < 0,
(deriv eps < 0)%R -> not (Weber ps w). * then w is not a weber point. *)
Lemma deriv_neg_not_weber :
(exists eps, deriv eps < 0)%R -> ~Weber ps w.
Proof. Admitted. Proof. Admitted.
(* If we cannot find a direction eps such that deriv eps < 0,
* then w is a local minimum for dist_sum ps. *)
Lemma deriv_nonneg_local_min :
(forall eps, deriv eps >= 0)%R ->
exists c,
(0 < c)%R /\
forall eps, (norm eps < c)%R -> (dist_sum ps w <= dist_sum ps (w + eps))%R.
Proof. Admitted.
Lemma candidate_exists_not_weber :
(exists eps, eps <> 0%VS /\ candidate eps) -> not (Weber ps w). (* This is a consequence of the cauchy-schwartz inequality. *)
Proof. Lemma deriv_neg_iff :
(* Show that dist_sum (w + s * eps) < dist_sum w for some positive small s. *) (norm (list_sumVS (List.map u ps)) > INR (mult w))%R <-> (exists eps, deriv eps < 0)%R.
Admitted.
Lemma no_candidate_weber :
(forall eps, eps <> 0%VS -> not (candidate eps)) -> Weber ps w.
Proof.
Admitted.
(* This should be a consequence of the cauchy-schwartz inequality. *)
Lemma candidate_exists_iff :
(norm (list_sumVS (List.map u ps)) > INR (mult w))%R <-> exists eps, eps <> 0%VS /\ candidate eps.
Admitted. Admitted.
(* This is the first order condition for weber points. *) (* This is the first order condition for weber points. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment