В Coq, есть ли тактика для работы с Рабами, Rineq? - PullRequest
Новая
       55

В Coq, есть ли тактика для работы с Рабами, Rineq?

2 голосов
/ 28 октября 2019

Я новичок в 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.

Ответы [ 2 ]

2 голосов
/ 29 октября 2019

Вот доказательство с использованием кокелико, возможно, с некоторыми из тактик это можно сделать лучше, но это было довольно просто. Всякий раз, когда я задавался вопросом, какую лемму использовать, я делал 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.
1 голос
/ 29 октября 2019

Частичный ответ на мой собственный вопрос: я понял, что тактика 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.
...