时间戳

首页 > 解决方案 > 如何避免真=假条件

coq - 如何避免真=假条件

问题描述

我正在使用标准库中的函数（list_max l）并证明以下引理。我在以下几点面临问题，请指导我。

 Fixpoint g_fun (l : list nat) :=
  match l with
 | nil => 1
 | b::nil=> b
 | b::t => gcd b (g_fun t)
end.
 Lemma gc1: forall (l : list nat),
 l<>nil -> list_max l = 0-> g_fun l=0.
 Proof.
 intros. induction l. unfold g_fun.

标签： coq

解决方案

I haven't tried it, but I think I would prove two auxiliary lemmas first:

  1. if list_max l = 0, then l is a list with only zeros [EDIT: or l is empty]; proving this will likely go through list_max_le.
  2. g_fun [n; n; ...; n] = g_fun [n]; this should be a simple induction together with Nat.gcd_diag.

If l is empty, your lemma is actually false, because list_max nil = 0 and g_fun nil = 1. Otherwise the lemma is an easy corollary of these two facts.

推荐阅读