0

我有一个函数可以给我一对自然数。
每对都由其序列号标识，例如sr1=(1,25) sr2=(26,50) sr3=(51,75).
数字的平均值是 25。然后我有另一个函数，它给了我每对的第一个和第二个之间存在的自然数列表，比如l1=[1,2,......25] l2=[26,27...50].

我想证明如果对的序列号不同，则列表中不会重复任何元素。因此对是互斥的。

Lemma lgroups: forall sn1 sn2 avg, 
S sn1 < S sn2 -> 
avg =? 0  = false ->
(S sn1 * avg <? S sn2 * avg - (avg - 1) = true)

Proof. intros. induction sn1 .  rewrite mult_1_l.
simpl. induction sn2. simpl. rewrite plus1_0_r.
destruct avg. inversion H0. inversion H .
4

1 回答 1

2

上下文对我来说并不完全清楚，但我可以回答证明给定引理的问题。

首先，这种引理通常不会使用布尔运算来陈述，而是使用它们的命题对应物。这会给出这样的结果。

Lemma lgroups: forall sn1 sn2 avg,
  S sn1 < S sn2 -> 
  avg <> 0 ->
  S sn1 * avg < S sn2 * avg - (avg - 1).

其次，我也倾向于在处理自然数时使用+而不是-一般，因为后者的行为由于没有负数而有点不自然。我认为，在你的情况下，这也更有意义，因为它正确表达了直观的陈述“当前序列的最后一个元素小于以下元素的第一次出现”，而我有点不清楚你原来的陈述。

Lemma lgroups: forall sn1 sn2 avg,
  S sn1 < S sn2 -> 
  avg <> 0 ->
  S sn1 * avg + avg - 1 < S sn2 * avg.

第三，我也会放弃S到处，因为结果在这种情况下也成立并且严格更强。

Lemma lgroups: forall sn1 sn2 avg,
  sn1 < sn2 -> 
  avg <> 0 ->
  sn1 * avg + avg - 1 < sn2 * avg.

对于证明，这种简单的算术证明实际上可以通过某些策略自动证明，特别是niaMicromega的策略。

这最终给出：

Require Import Lia.

Lemma lgroups: forall sn1 sn2 avg,
  sn1 < sn2 -> 
  avg <> 0 ->
  sn1 * avg + avg - 1 < sn2 * avg.
Proof.
  intros. nia.
Qed.
于 2019-09-17T13:13:43.283 回答