小编Lar*_*Lee的帖子

背景

我知道Iota减少用于减少/扩展递归函数.例如,给定以下简单递归函数的应用(自然数上的阶乘):

((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)

Iota缩减扩展了递归调用,有效地迭代递归函数一次:

Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
 = (fun n:nat =>
    match n with
    | 0 => 1
    | S m =>
        n *
        (fix fact (m : nat) : nat :=
           match m with
           | 0 => …

我有一个简单的定理,我想通过案例证明.下面给出一个例子.

Goal forall a b : Set, a = b \/ a <> b.
Proof
  intros a b.
  ...

我将如何解决这个问题.而且,我究竟如何使用两个可能的相等值(True或False)来定义证明？

任何帮助,将不胜感激.谢谢,