将无穷级数的存在性证明转换为给出该无穷级数的函数

Question

我正在尝试根据TRS进行推理，并且遇到了以下证明义务：

  infinite_sequence : forall t' : Term,
                      transitive_closure R t t' ->
                      exists t'' : Term, R t' t''
  ============================
   exists f : nat -> Term, forall n : nat, R (f n) (f (n + 1))

transitive_closure定义如下：

Definition transitive_closure (trs : TRS) (x y : Term) := 
    exists f: nat -> Term, 
            f 0 = x 
        /\ 
            exists l: nat, 
                    f l = y 
                /\ 
                    forall n: nat, 
                            n < l 
                        -> 
                            trs (f n) (f (n + 1))
.

所以当我unfold：

  infinite_sequence : forall t' : Term,
                      (exists f : nat -> Term,
                         f 0 = t /\
                         (exists l : nat,
                            f l = t' /\
                            (forall n : nat, n < l -> R (f n) (f (n + 1))))) ->
                      exists t'' : Term, R t' t''
  ============================
   exists f : nat -> Term, forall n : nat, R (f n) (f (n + 1))

此证明义务是否有可能履行？我还没有嫁接到transitive_closure的确切定义，因此如果通过为它选择一个不同的定义变得容易得多，我可以接受。

Answer 1

由于您的目标始于exists f : nat -> Term，因此您必须显式构建此类功能。最简单的方法是先构建一个返回类型稍微更丰富的函数（用{ u: Term | transitive_closure R t u }代替Term），然后逐点投影其第一个组件以完成证明。这将提供以下脚本：

simple refine (let f : nat -> { u: Term | transitive_closure R t u } := _ in _).
- fix f 1.
  intros [|n].
  { exists t. exists (fun _ => t). admit. }
  destruct (f n) as [t' H].
  destruct (infinite_sequence t' H) as [t'' H']. (* ISSUE *)
  exists t''.
  destruct H as [f' [H1 [l [H2 H3]]]].
  exists (fun m => if Nat.ltb m l then f' m else t'').
  admit.
- exists (fun n => proj1_sig (f n)).
  intros n.
  rewrite Nat.add_1_r.
  simpl.
  destruct (f n) as [fn Hn].
  now destruct infinite_sequence as [t'' H'].

两个admit只是为了使代码简单；他们没有什么困难。真正的问题来自destruct (infinite_sequence t' H)行，因为Coq会抱怨“归纳定义ex不允许对sort Set进行案例分析”。确实，infinite_sequence指出存在t''使得R t' t''，但它是以非信息性的方式（即，在Prop中），而您需要它来构建生活在具体环境中的函数世界（即Set中）。

只有两种无公理解决方案，但是两者都可能与其余的开发不兼容。最简单的方法是将infinite_sequence放入Set，这意味着其类型已更改为forall t', transitive_closure R t t' -> { t'' | R t' t'' }。

第二种解决方案要求R是可确定的关系，Term是可枚举的集合。这样，您仍然可以通过列举所有条件直到找到一个满足t''的条件来构建具体的R t' t''。在这种情况下，infinite_sequence仅用于证明该过程已终止，因此它可以是非信息性的。