有了以下定义,我想证明引理 without_P
Variable n : nat.
Definition mnnat := {m : nat | m < n}.
Variable f : mnnat -> nat.
Lemma without_P : (exists x : mnnat, True) -> (exists x, forall y, f x <= f y).
引理without_P意味着:如果你知道(有限)集合mnnat不是空的,那么mnnat在映射f到之后必须存在一个元素,即所有元素中最小的元素mnnat.
我们知道mnnat是有限的,因为它有n-1数字,并且在证据的背景下,without_P我们也知道mnnat不是空的,因为前提(exists x : mnnat, True).
现在mnnat非空和有限的"自然/直觉"具有一些最小元素(在应用f其所有元素之后).
目前我被困在下面的那个地方,我想在那里进行归纳n,这是不允许的.
1 subgoal
n : nat
f …我想创建混合类型的列表boolean和nat。此列表必须包含某些超类型的元素：boat每个boolean都是a boat，每个nat都是a boat。
我遇到的问题是，此超级类型boat应具有一定的boat_eq_dec含义，应该有一种方法可以确定两个boat对象是相同还是不同。由于nat和boolean两者都有这样的平等决定者，因此超类型也应该有一个平等决定者。
在下面的示例中，我创建了一个超类型，但是无法显示决定相等性的引理Lemma boat_eq_dec : forall x y : Boat, {x = y} + {x <> y}.
Inductive Boat : Set :=
| is_bool (inp: bool)
| is_nat (inp: nat).
定义此超类型或显示引理的正确方法是什么？