涉及不平等的车队模式和比赛
convoy pattern and match involving inequality
我在实现简单功能时遇到问题,我很确定答案是 "convoy pattern",但我只是想不出如何在这种特殊情况下应用它。这是一个完整的例子:
Require Import Coq.Lists.List.
Definition index_map_spec (domain range: nat) :=
forall n : nat, n < domain -> {v : nat | v < range}.
Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.
Fixpoint natrange_f_spec
(n:nat)
{i o: nat}
(nd: n<i)
(f_spec: index_map_spec i o)
: list nat
:=
match n return list nat with
| 0 => nil
| S n' => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
end.
我得到的错误是:
The term "nd" has type "n < i" while it is expected to have type
"S ?578 < ?579".
所以基本上我想在 'n' 上以某种方式匹配 (n=S p) 它会重写 (n
您只需对 match
上的 nd
证明进行抽象,相应地更改其 return 类型:
Require Import Coq.Lists.List.
Definition index_map_spec (domain range: nat) :=
forall n : nat, n < domain -> {v : nat | v < range}.
Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.
Fixpoint natrange_f_spec
(n:nat)
{i o: nat}
(nd: n<i)
(f_spec: index_map_spec i o)
: list nat
:=
match n return n < i -> list nat with
| 0 => fun _ => nil
| S n' => fun nd => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
end nd.
我在实现简单功能时遇到问题,我很确定答案是 "convoy pattern",但我只是想不出如何在这种特殊情况下应用它。这是一个完整的例子:
Require Import Coq.Lists.List.
Definition index_map_spec (domain range: nat) :=
forall n : nat, n < domain -> {v : nat | v < range}.
Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.
Fixpoint natrange_f_spec
(n:nat)
{i o: nat}
(nd: n<i)
(f_spec: index_map_spec i o)
: list nat
:=
match n return list nat with
| 0 => nil
| S n' => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
end.
我得到的错误是:
The term "nd" has type "n < i" while it is expected to have type
"S ?578 < ?579".
所以基本上我想在 'n' 上以某种方式匹配 (n=S p) 它会重写 (n
您只需对 match
上的 nd
证明进行抽象,相应地更改其 return 类型:
Require Import Coq.Lists.List.
Definition index_map_spec (domain range: nat) :=
forall n : nat, n < domain -> {v : nat | v < range}.
Lemma lt_pred_l {n m} (H: S n < m): n < m.
Proof. auto with arith. Defined.
Fixpoint natrange_f_spec
(n:nat)
{i o: nat}
(nd: n<i)
(f_spec: index_map_spec i o)
: list nat
:=
match n return n < i -> list nat with
| 0 => fun _ => nil
| S n' => fun nd => cons n' (natrange_f_spec n' (lt_pred_l nd) f_spec)
end nd.