From 5f185011e2380212911b9c195947a1675773b1c2 Mon Sep 17 00:00:00 2001 From: Jim Portegies Date: Tue, 31 Oct 2023 16:15:18 +0100 Subject: [PATCH] feat: some adaptations for the continuity exercises --- theories/Automation/Hints.v | 5 + theories/Libs/Analysis/ContinuityDomainNat.v | 100 +++++++++++++++---- theories/Libs/Analysis/ContinuityDomainR.v | 13 ++- 3 files changed, 93 insertions(+), 25 deletions(-) diff --git a/theories/Automation/Hints.v b/theories/Automation/Hints.v index 8a84d3b7..938b1907 100644 --- a/theories/Automation/Hints.v +++ b/theories/Automation/Hints.v @@ -431,6 +431,11 @@ Create HintDb wp_reals. #[export] Hint Resolve Rmin_right : wp_reals. #[export] Hint Resolve Rmin_glb : wp_reals. #[export] Hint Resolve Rmin_glb_lt : wp_reals. + (** lemmas to relate <= with >= and < with > *) + #[export] Hint Resolve Rge_le : wp_reals. + #[export] Hint Resolve Rle_ge : wp_reals. + #[export] Hint Resolve Rgt_lt : wp_reals. + #[export] Hint Resolve Rlt_gt : wp_reals. #[export] Hint Resolve div_sign_flip : wp_reals. #[export] Hint Resolve div_pos : wp_reals. diff --git a/theories/Libs/Analysis/ContinuityDomainNat.v b/theories/Libs/Analysis/ContinuityDomainNat.v index 2a18dc20..3daac0e3 100644 --- a/theories/Libs/Analysis/ContinuityDomainNat.v +++ b/theories/Libs/Analysis/ContinuityDomainNat.v @@ -18,16 +18,19 @@ Require Import Coq.Reals.Reals. +Require Import Tactics. Require Import Automation. Require Import Libs.Negation. Require Import Notations. -Require Import Tactics. Waterproof Enable Automation RealsAndIntegers. Open Scope R_scope. (** Hints *) + +(** TODO: move these lemmas somewhere else *) + Lemma aux1 : for all n m : ℕ, (n = m) ⇒ |m - n| = |n - n|. Proof. Take n, m : ℕ. @@ -36,28 +39,82 @@ Proof. Qed. #[export] Hint Resolve aux1 : wp_reals. -(** Useful lemma *) -Lemma useful_lemma : for all n m : ℕ, (n ≠ m) ⇒ (1 ≤ | m - n |). +Lemma Rabs_n_min_m : forall m n : ℕ, (m <= n)%nat -> | n - m | = n - m. +Proof. + Take m, n : nat. + Assume that (m <= n)%nat. + It holds that (m <= n). + We conclude that (| n - m | = n - m). +Qed. + +#[export] Hint Resolve Rabs_n_min_m : wp_reals. + +Lemma Rabs_m_lt_n : forall m n : ℕ, (m < n)%nat -> 1 <= | n - m |. +Proof. + Take m, n : nat. + Assume that (m < n)%nat. + It holds that (m <= n). + It holds that ( | n - m | = n - m). + It holds that (m + 1 <= n)%nat. + It holds that (INR m + INR 1 = INR (m + 1)%nat). + It holds that ((m + 1)%nat <= n). + It holds that (& INR m + INR 1 = INR (m + 1)%nat <= n). + We conclude that (1 <= | n - m |). +Qed. + +#[export] Hint Resolve Rabs_m_lt_n : wp_reals. + +Lemma nat_not_equal_dist_larger_one : for all n m : ℕ, (n ≠ m) -> (1 ≤ | m - n |). Proof. - Take n, m : ℕ. Assume that (n ≠ m). + Take n, m : ℕ. + Assume that (n ≠ m). assert (n > m ∨ n < m)%nat as i by (apply Nat.lt_gt_cases; auto). Because (i) either (n > m)%nat or (n < m)%nat holds. + Case (n > m)%nat. - It holds that (n ≥ S m)%nat. - By S_INR it holds that (m + 1 = S m). - It holds that (m + 1 - m = S m - m). - It holds that ((S m) ≤ n). - It holds that ((S m) - m ≤ n - m). - We conclude that - (& 1 = m + 1 - m = (S m) - m ≤ n - m = | n - m | = | m - n | ). - + Case (n < m)%nat. - It holds that (S n ≤ m)%nat. - By S_INR it holds that (n + 1 = S n). - It holds that (n + 1 - n = S n - n). - It holds that ((S n) ≤ m). - It holds that ((S n) - n ≤ m - n). - We conclude that (& 1 = n + 1 - n = (S n) - n ≤ m - n = |m - n|). + It holds that (| n - m | = | m - n | ). + It holds that (1 <= | n - m |). + We conclude that (1 <= | m - n |). + + Case (m > n)%nat. + We conclude that (1 <= | m - n |). +Qed. +#[export] Hint Resolve nat_not_equal_dist_larger_one : wp_reals. + +Lemma nat_dist_larger_zero_not_equal : + forall n m : nat, 0 < | n - m | -> ~(n = m). +Proof. +Take n, m : nat. +Assume that (0 < | n - m | ). +Either (n = m)%nat or (~(n= m))%nat. ++ Case (n = m)%nat. + It holds that (| m - n| = 0). + Contradiction. ++ Case (~(n = m)). + We conclude that (~(n = m)). Qed. +#[export] Hint Resolve nat_dist_larger_zero_not_equal : wp_reals. + +Lemma nat_dist_less_than_one_iff_equal : + forall n m : ℕ, (n = m) <-> (| m - n | < 1). +Proof. + Take n, m : nat. + We show both directions. + - We need to show that (n = m ⇨ |m - n| < 1). + Assume that (n = m). + We argue by contradiction. + Assume that (~ | m - n | < 1). + It holds that (1 <= | m - n|). + It holds that (~(n=m)). + Contradiction. + - We need to show that (| m - n | < 1 -> n = m). + Assume that (| m - n| < 1). + We argue by contradiction. + Assume that (~ (n = m)). + It holds that (1 <= | m - n|). + Contradiction. +Qed. + +#[export] Hint Resolve <- nat_dist_less_than_one_iff_equal : wp_reals. +#[export] Hint Resolve -> nat_dist_less_than_one_iff_equal : wp_reals. (** Definitions *) Section metricspace. @@ -107,7 +164,7 @@ Proof. It holds that (| x - a | = 0). Contradiction. + Case (~(x = a)). - By useful_lemma it holds that (1 ≤ | x - a |). + It holds that (1 ≤ | x - a |). Contradiction. * We need to show that ((for all ε : ℝ, ε > 0 ⇨ there exists δ : ℝ, @@ -132,12 +189,15 @@ Proof. We conclude that (|n - a| = 0). + Case (~(n=a)). It suffices to show that ((1/2) ≤ | n - a |). - By useful_lemma it holds that (1 ≤ | n - a |). + It holds that (1 ≤ | n - a |). We conclude that (1/2 ≤ | n - a | ). Qed. End metricspace. +#[export] Hint Resolve -> alt_char_continuity : wp_reals. +#[export] Hint Resolve <- alt_char_continuity : wp_reals. + (** Notations *) Notation "a 'is' 'an' '_accumulation' 'point_'" := (is_accumulation_point a) (at level 68). diff --git a/theories/Libs/Analysis/ContinuityDomainR.v b/theories/Libs/Analysis/ContinuityDomainR.v index 5c1910ab..95dd8491 100644 --- a/theories/Libs/Analysis/ContinuityDomainR.v +++ b/theories/Libs/Analysis/ContinuityDomainR.v @@ -108,7 +108,10 @@ Proof. + By (every_point_in_R_acc_point_R) we conclude that (is_accumulation_point a). + We conclude that (limit_in_point(h, a, h a)). Qed. - + +#[export] Hint Resolve -> alt_char_continuity : wp_reals. +#[export] Hint Resolve <- alt_char_continuity : wp_reals. + (** Notations *) Notation "a 'is' 'an' '_accumulation' 'point_'" := (is_accumulation_point a) (at level 68). @@ -132,9 +135,9 @@ Ltac2 Notation "Expand" "the" "definition" "of" "isolated" "point" "in" statemen Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "isolated" "point" "in" statement(constr) := unfold_in_statement_no_error unfold_isol_point (Some "isolated point") statement. -Notation "'_limit_' 'of' f 'in' a 'is' L" := (limit_in_point _ f a L) (at level 68). +Notation "'_limit_' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 68). -Notation "'limit' 'of' f 'in' a 'is' L" := (limit_in_point _ f a L) (at level 68, only parsing). +Notation "'limit' 'of' f 'in' a 'is' L" := (limit_in_point f a L) (at level 68, only parsing). Local Ltac2 unfold_lim_in_point (statement : constr) := eval unfold limit_in_point in $statement. @@ -144,9 +147,9 @@ Ltac2 Notation "_internal_" "Expand" "the" "definition" "of" "limit" "in" statem unfold_in_statement_no_error unfold_lim_in_point (Some "limit") statement. -Notation "f 'is' '_continuous_' 'in' a" := (is_continuous_in _ f a) (at level 68). +Notation "f 'is' '_continuous_' 'in' a" := (is_continuous_in f a) (at level 68). -Notation "f 'is' 'continuous' 'in' a" := (is_continuous_in _ f a) (at level 68, only parsing). +Notation "f 'is' 'continuous' 'in' a" := (is_continuous_in f a) (at level 68, only parsing). Local Ltac2 unfold_is_cont (statement : constr) := eval unfold is_continuous_in in $statement.