coq现场战术无法简化，因此，“ m< m> 0％R“ [英] coq field tactic fails to simplify, yeilds "m <> 0%R"

问题描述

我是Coq的新手。我一直在研究 Pierce的逻辑基础。我正在步入新的台阶。

I'm new to Coq. I've been working through Pierce's Logical Foundations. I'm stepping into new ground.

我正在尝试第一次使用字段策略。我在下面的定理中使用三次。两次失败，产生 m<> 0％R 其中m是上下文中的术语。

I'm trying use of the field tactic for the first time. I use it thrice in the below theorem. Twice it fails, yielding m <> 0%R where m is a term in context.

我确定我只是不理解正确的用法。有人可以启发我吗？ （我尝试阅读此文档页面，但并没有获得太多的理解！）

I'm sure I just fail to understand proper use. May someone enlighten me? (I tried reading this doc page but didn't gain much understanding!)

From Coq Require Import Reals.Reals. 
Require Import Field.

Definition simple_compound (A r n m : R) : R :=
  A * (Rpower (1 + r / m) (m * n)). 
Definition continuous_compound (A r n: R) : R :=
  A * (exp (r * n)).
Definition simple_to_continuous_interest (Rs n m: R) : R :=
  m * ln (1 + Rs / m). 
Definition continuous_to_simple_interest (Rc n m: R) : R :=
  m * ((exp (Rc / m)) - 1). 

Theorem continuous_to_simple_works : forall (A Rc n m : R),
  continuous_compound A Rc n = simple_compound A (continuous_to_simple_interest Rc n m) n m. 
Proof.
  intros A Rc n m.
  unfold continuous_compound. unfold simple_compound. unfold continuous_to_simple_interest.
  unfold Rpower. apply f_equal.
  assert (H: (m * (exp (Rc / m) - 1) / m)%R = (exp (Rc / m) - 1)%R). {
    field. admit.
  }
  rewrite -> H. 
  assert (H2: (1 + (exp (Rc / m) - 1))%R = (exp (Rc / m))%R). {
    field. 
  }
  rewrite -> H2. 
  assert (H3: (m * n * ln (exp (Rc / m)))%R = (ln (exp (Rc / m)) * m * n)%R). {
    rewrite -> Rmult_comm. rewrite -> Rmult_assoc. reflexivity. 
  }
  rewrite -> H3. 
  rewrite -> ln_exp. 
  assert (H4: (Rc / m * m)%R = Rc%R). {
    field. admit. 
  }
  rewrite -> H4. 
  reflexivity. 
Admitted. 

推荐答案

这是预期的。您第一次使用字段的目标类似于（m * x）/ m = x 。绝对没有定义实数除法的方法，这样当 m 时，所有等价数 x 的等式都成立等于 0 。因此，仅当您能够证明 m<>时，字段策略才能证明这种相等性。 0 。您对字段的第三次使用是在等式（x / m）* m = x 上，它可以如果您知道 m 不为零，则仅对任何 x 成立。

That is expected. Your first use of field is on a goal akin to (m * x) / m = x. There is absolutely no way of defining the division over real numbers so that this equality holds for all real numbers x when m is equal to 0. So, the field tactic is able to prove this equality only if you are able to prove m <> 0. Your third use of field is on an equality (x / m) * m = x, and again, it can only hold for any x if you know that m is nonzero.

这篇关于coq现场战术无法简化，因此，“ m< m> 0％R“的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！