我正在尝试处理ssreflect中的规范结构.我从这里获取了 2段代码.
我将为bool和选项类型带来件.
Section BoolFinType.
Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed.
Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed.
End BoolFinType.
Section OptionFinType.
Variable T : finType.
Notation some := (@Some _) (only parsing).
Local Notation enumF T := (Finite.enum T).
Definition option_enum := None :: map some (enumF T).
Lemma …我有以下问题，请查看代码。
(* Suppose we have type A *)
Variable A: Type.
(* Also we have a function that returns the type (option A) *)
Definition f_opt x: option A := ...
(* Then, I can prove that this function always returns something: *)
Theorem always_some: forall x, exists y, f_opt x = Some y.
Admitted.
(* Or, equivalently: *)
Theorem always_not_none: forall x, f_opt x <> None.
Admitted.
现在我想得到一个f_opt总是返回 type 值的版本A。像这样的东西：
Definition f x: A := …