从比赛中提取平等的证据 [英] extracting evidence of equality from match

问题描述

我正在尝试以下工作：

    Definition gen `{A:Type}
           {i o: nat}
           (f: nat -> (option nat))
           {ibound: forall (n n':nat), f n = Some n' -> n' < i}
           (x: svector A i) (t:nat) (ti: t < o): option A
  := match (f t) with
     | None => None
     | Some t' => Vnth x (ibound t t' _)
     end.

要代替最后一个 _，我需要一个证明， ft等于 Some t '。我不知道如何从比赛中得到它。 Vnth定义为：

In place of last "_" I need an evidence that "f t" is equals to "Some t'". I could not figure out how to get it from the match. Vnth is defined as:

Vnth
     : ∀ (A : Type) (n : nat), vector A n → ∀ i : nat, i < n → A

推荐答案

编写此函数需要一个实例被称为车队模式（请参见此处）） 。我相信以下内容应该可以工作，尽管我无法对其进行测试，因为我没有其余的定义。

Writing this function requires an instance of what is known as the convoy pattern (see here). I believe the following should work, although I can't test it, since I don't have the rest of your definitions.

Definition gen `{A:Type}
           {i o: nat}
           (f: nat -> (option nat))
           {ibound: forall (n n':nat), f n = Some n' -> n' < i}
           (x: svector A i) (t:nat) (ti: t < o): option A
  := match f t as x return f t = x -> option A with
     | None => fun _ => None
     | Some t' => fun p => Vnth x (ibound t t' p)
     end (eq_refl (f t)).

这篇关于从比赛中提取平等的证据的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！