В Coq есть тактика работы с Rabs, Rineq?

Я новичок в Coq, и меня больше всего интересует его использование для решения простых реальных задач анализа. В качестве первого упражнения мне удалось получить доказательство того, что x ^ 2 + 2x стремится к 0, когда x стремится к 0. См. Код ниже.

Это кажется довольно неуклюжим, и мне были бы интересны любые общие отзывы о том, как сократить это доказательство, или хорошие практики для улучшения его читабельности. Однако мой главный вопрос заключается в том, существует ли какая-либо тактика Coq для автоматизации простых задач, связанных с реальными числами, вроде field и lra, но лучше.

возможный пример 1: существуют ли какие-либо тактики для подтверждения идентичности функций из Rbasic_fun, например, абсолютное значение? Например, половина моего доказательства посвящена тому, чтобы показать, что | x * x | + | 2 * x | = | x | | x | +2 | x | !

возможный пример 2: существуют ли какие-либо тактики для автоматизации использования лемм из Rineq, таких как Rlt_le, Rle_trans, Rplus_le_compat_r и Rmult_le_compat_r? То есть леммы, которые человек-создатель доказательств использовал бы, чтобы «связать воедино» последовательность неравенств.

Require Import Rbase.
Require Import Rbasic_fun.
Require Import Lra.
Local Open Scope R_scope.

Definition limit (f:R -> R)
  (D:R -> Prop) (l:R) (x0:R) :=
  forall eps:R,
    eps > 0 ->
    exists delta : R,
      delta > 0 /\
      (forall x:R, D x /\ Rabs (x - x0) < delta -> Rabs ((f x) - l) < eps).

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
Proof.
  unfold limit; intros.
  split with (Rmin (eps/3) 1); split.
  assert (eps / 3 > 0) by lra; clear H.
  assert (1>0) by lra.
  apply (Rmin_Rgt_r (eps/3) 1). apply (conj H0 H).
  intros. destruct H0. clear H0.  replace (x-0) with x in H1 by field.
  apply (Rmin_Rgt_l (eps/3) 1) in H1. destruct H1.
  assert (Rabs (x*x+2*x -0) <= Rabs(x*x)+Rabs(2*x)).
    replace (x*x+2*x-0) with (x*x+2*x) by field.
    apply Rabs_triang.
  assert (Rabs(2*x) =  2 * Rabs(x)). 
    assert (Rabs(2*x) =  Rabs(2) * Rabs(x)).
      apply (Rabs_mult _ _).
    assert (Rabs 2 = 2).
      apply (Rabs_right _). lra.
    replace (Rabs 2) with 2 in H3 by H4. apply H3.
  replace (Rabs (2 * x)) with (2 * Rabs x) in H2 by H3.  clear H3.
  assert (Rabs(x*x) = Rabs(x)*Rabs(x)). 
    apply Rabs_mult.
  replace (Rabs(x*x)) with (Rabs(x)*Rabs(x)) in H2 by H3.  clear H3.
  assert (Rabs x * Rabs x <= 1 * Rabs x).
    apply Rmult_le_compat_r.  apply Rabs_pos.  apply Rlt_le. auto.
  apply (Rplus_le_compat_r (2 * Rabs x) _ _) in H3.
  apply  (Rle_trans _ _ _ H2) in H3. clear H2.
  replace (1 * Rabs x + 2 * Rabs x) with (3 * Rabs x) in H3 by field.
  assert (3 * Rabs x < eps) by lra.
  apply  (Rle_lt_trans _ _ _ H3). auto.
Qed.

theorem-proving coq coq-tactic real-number
person anon    schedule 27.10.2019    source источник
comment
Вы уже знакомы с библиотекой Coquelicot? В нем есть определения ограничений и т. Д., С которыми мне легче работать. И они работают с обычными вещественными числами Coq, имеют леммы преобразования и т. Д., Поэтому они могут использовать леммы о вещественных числах, разработанные в других местах.   -  person larsr    schedule 29.10.2019
comment
Спасибо за ответ! Я мельком взглянул на Кокелико. Однако кажется, что инструменты Coquelicot в основном предназначены для автоматизации ограничений / анализа, тогда как я хочу автоматизировать виды низкоуровневых манипуляций с действительными числами, о которых я упоминал, но не автоматизировать сам эпсилон-дельта-анализ. Вы знаете, есть ли такая возможность в Coquelicot?   -  person anon    schedule 29.10.2019
comment
Библиотеки coquelicot очень читабельны (чего нет во многих других библиотеках), они читаются почти как учебник. Я рекомендую прочитать код (в документе coq), развернуть определения и т. Д., И вы увидите, что определения очень естественны. Есть несколько приемов, например, использование фильтров, но в любом случае их полезно изучить.   -  person larsr    schedule 29.10.2019
comment
Вы также можете прочитать о Coquelicot и о том, как они определяют ограничения и т. Д., В этом документе. Очень читабельная презентация.   -  person larsr    schedule 29.10.2019

Ответы (2)


arrow_upward
2
arrow_downward

Вот доказательство с использованием coquelicot, его, вероятно, можно сделать лучше с помощью некоторых тактик, но это было довольно просто. Всякий раз, когда я задавался вопросом, какую лемму использовать, я делал Search, чтобы найти лемму с членом в ее заключении ...

Require Import Reals.
From Coquelicot Require Import Coquelicot.
Open Scope R.

Lemma limitf : is_lim (fun x => x*x + 2 * x) 0 0.
  eapply is_lim_plus.
  eapply is_lim_mult.
  eapply is_lim_id.
  eapply is_lim_id.
  compute. apply I.
  eapply is_lim_mult.
  eapply is_lim_const.
  eapply is_lim_id.
  compute. apply I.
  compute. f_equal.  f_equal.
  ring.  
Qed.

Редактировать:

Вот доказательство вашей леммы выше с использованием вместо этого лемм из стандартной библиотеки Coq. Я нашел их, сильно полагаясь на Search. Возможно, такой подход упрощает создание подобных доказательств за вас.

Require Import Reals Lra.
Local Open Scope R_scope.

Definition limit (f:R -> R)
  (D:R -> Prop) (l:R) (x0:R) :=
  forall eps:R,
    eps > 0 ->
    exists delta : R,
      delta > 0 /\
      (forall x:R, D x /\ Rabs (x - x0) < delta -> Rabs ((f x) - l) < eps).

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
  intros eps Heps.
  exists (Rmin (eps/3) 1).
  split. apply Rmin_Rgt. lra.
  intros x [_ H].
  destruct (Rmin_Rgt_l _ _ _ H); clear H.
  rewrite Rminus_0_r in *.
  eapply Rle_lt_trans.
  apply Rabs_triang.
  do 2 erewrite Rabs_mult.
  pose proof (Rabs_pos x).
  remember (Rabs x) as a; clear Heqa.
  rewrite (Rabs_right 2) by lra.
  replace eps with (((eps/3)*1) + (2*eps/3)) by lra.
  apply Rplus_lt_compat; try lra.
  apply Rmult_le_0_lt_compat; lra.
Qed.
person larsr    schedule 28.10.2019
comment
Спасибо, что написали это, это, безусловно, очень элегантно! Однако на самом деле я хочу автоматизировать только те виды низкоуровневых задач, которые я упомянул, а не сам эпсилон-дельта-анализ. Дело не в том, что у меня есть этические возражения против фильтров :) - скорее, приложение, которое я имею в виду, предназначено для обучения, поэтому мне нужен набор библиотек, которые автоматизируют те части доказательства, которые студенты считают очевидными, и только эти части. - person anon; 29.10.2019
comment
@anon Я добавил доказательство, используя ваше определение limit, которое, я надеюсь, показывает менее громоздкий способ рассуждать о Rabs, используя леммы из стандартной библиотеки. - person larsr; 29.10.2019
comment
@anon (ой, только что увидел, что вы сделали это в своем посте ниже!) - person larsr; 29.10.2019
comment
Большое спасибо - это действительно помогает новичку увидеть такую ​​детальную ревизию своего кода. Я не знал о pose proof; теперь я могу избавиться от всех этих assert! Однако я предпочитаю использовать nra (как в моем ответе), а не явный вызов Rplus_lt_compat, Rmult_le_0_lt_compat и т. Д. - person anon; 29.10.2019

arrow_upward
1
arrow_downward

Частичный ответ на мой собственный вопрос: я понял, что тактика nra из micromega делает именно то, что я просил в моем "возможном примере 2". Итак, вот версия моего предыдущего кода, в которой рассуждения о неравенстве автоматически выполняет nra. Мне все еще интересно узнать, существует ли тактика рассуждений об абсолютном значении и минимальном / максимальном значении, соответствующая моему "возможному примеру 1".

Обновление: приведенный ниже код улучшен некоторыми идиомами (pose proof, exists), извлеченными из ответа @larsr.

Require Import Psatz.
.....

Lemma limitf : limit (fun (x:R) => x*x + 2 *x) (fun x => True) 0 0.
Proof.
  unfold limit; intros.
  exists (Rmin (eps/3) 1); split.
  apply Rmin_Rgt; lra.
  intros; destruct H0.  
  replace (x-0) with x in H1 by field; replace (x*x+2*x-0) with (x*x+2*x) by field.
  apply Rmin_Rgt_l in H1; destruct H1.
  pose proof (Rabs_triang (x*x) (2*x)).
  pose proof (Rabs_mult 2 x).
  pose proof (Rabs_mult x x).
  pose proof (Rabs_pos x).
  epose proof (Rabs_right 2).
  nra.
Qed.
person anon    schedule 28.10.2019