coq - 相互递归类型的自定义归纳原则
问题描述
尝试为某些特定的相互递归类型定义归纳原理时,我感到有些困惑。使用Schema
并不能真正解决我的问题,这就是为什么我考虑自己定义原则的原因(也许我使用相互递归类型的整个方法不合适......这也是一个选项)。
我正在使用亚瑟的结构库(这就是它的ordType
来源,它可能是别的东西)。所以,我的类型是:
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From extructures Require Import ord fmap.
Section R.
Variables Name Vals : ordType.
Inductive ResponseObject : Type :=
| SingleResponse : Result -> ResponseObject
| MultipleResponses : Result -> ResponseObject -> ResponseObject
with Result : Type :=
| Empty : Result
| Null : Name -> Result
| SingleResult : Name -> Vals -> Result
| ListResult : Name -> seq Vals -> Result
| NestedResult : Name -> ResponseObject -> Result
| NestedListResult : Name -> seq ResponseObject -> Result.
它基本上是一个非空Result
对象列表,它本身可以包含非空列表(NestedResult
和NestedListResult
)。
我的问题是NestedListResult
因为使用生成的归纳原理Schema
不会检查ResponseObject
. 它声明如下:
Scheme ResponseObject_ind := Induction for ResponseObject Sort Prop
with Result_ind := Induction for Result Sort Prop.
Check ResponseObject_ind.
ResponseObject_ind
: forall (P : ResponseObject -> Prop) (P0 : Result -> Prop),
(forall r : Result, P0 r -> P (SingleResponse r)) ->
(forall r : Result, P0 r -> forall r0 : ResponseObject, P r0 -> P (MultipleResponses r r0)) ->
P0 Empty ->
(forall s : Name, P0 (Null s)) ->
(forall (s : Name) (s0 : Vals), P0 (SingleResult s s0)) ->
(forall (s : Name) (l : seq Vals), P0 (ListResult s l)) ->
(forall (s : Name) (r : ResponseObject), P r -> P0 (NestedResult s r)) ->
(forall (s : Name) (l : seq ResponseObject), P0 (NestedListResult s l)) -> forall r : ResponseObject, P r
我尝试遵循SSReflect GenTree中的示例(它基本上折叠列表并检查每个元素是否满足谓词)但是在尝试定义它时出现语法错误(我猜这是语法错误?)我不确定如何修复它。我的猜测是使用fix
andwith
是不正确的,我应该以其他方式编写它?
我的尝试是这样的:
Definition ResponseObject_ind P Ps IH_SingleResponse IH_MultipleResponses IH_Empty IH_Null IH_SingleResult IH_ListResult IH_NestedResult IH_NestedListResult :=
fix loop (r : ResponseObject) : P r : Prop :=
match r with
| SingleResponse r' => IH_SingleResponse r' (Result_ind r')
| MultipleResponses r' rs => IH_MultipleResponses r' (Result_ind r') rs (loop rs)
end
with Result_ind (r : Result) : Ps r : Prop :=
match r with
| Empty => IH_Empty
| Null l => IH_Null l
| SingleResult l v => IH_SingleResult l v
| ListResult l vals => IH_ListResult l vals
| NestedResult l r' => IH_NestedResult l r' (Result_ind r')
| NestedListResult l rs =>
let fix iter_conj rs : foldr (fun r => and (P r)) True rs :=
if rs is r :: rs' then conj (loop r) (iter_conj rs') else Logic.I
in
IH_NestedListResult l rs (iter_conj rs)
end.
任何帮助,将不胜感激 :)
PS。实际上,也许其他方法比使用相互递归类型更好......在我ResponseObject
用作该Result
类型的另一个构造函数并检查它是否形成“正确”列表(没有嵌套ResponseObject
s 形成奇怪的树事物)之前。上面的这个选项看起来更优雅,但可能不太方便。
解决方案
您的解决方案不尊重语法和键入约束。修复这些约束的一种方法导致以下代码:
Definition ResponseObject_ind' (P : ResponseObject -> Prop)
(Ps : Result -> Prop) IH_SingleResponse IH_MultipleResponses IH_Empty IH_Null
IH_SingleResult IH_ListResult
(IH_NestedResult : forall (s : Name) (r : ResponseObject),
P r -> Ps (NestedResult s r))
IH_NestedListResult :=
fix loop (r : ResponseObject) : P r : Prop :=
match r with
| SingleResponse r' => IH_SingleResponse r' (Result_ind r')
| MultipleResponses r' rs => IH_MultipleResponses r' (Result_ind r') rs (loop rs)
end
with Result_ind (r : Result) : Ps r : Prop :=
match r with
| Empty => IH_Empty
| Null l => IH_Null l
| SingleResult l v => IH_SingleResult l v
| ListResult l vals => IH_ListResult l vals
| NestedResult l r' => IH_NestedResult l r' (loop r')
| NestedListResult l rs =>
let fix iter_conj rs : foldr (fun r => and (P r)) True rs :=
if rs is r :: rs' then conj (loop r) (iter_conj rs') else Logic.I
in
IH_NestedListResult l rs (iter_conj rs)
end
for loop.
我不喜欢你的iter_conj
解决方案。
在我看来,您实际上是在生成一堆归纳类型,其中包含三种归纳类型: ResponseObject
、Result
和seq ResponseObject
. 因此,您的归纳原则不应采用两个谓词P
and Ps
,而应具有三个谓词:P
for type ResponseObject
、Ps
forResult
和Pl
for seq ResponseObject
。这是我遵循以下几行的解决方案:
Definition RO_ind := fun
P P0 P1
(f : forall r : Result, P0 r -> P (SingleResponse r))
(f0 : forall r : Result,
P0 r ->
forall r0 : ResponseObject, P r0 -> P (MultipleResponses r r0))
(f1 : P0 Empty) (f2 : forall n : Name, P0 (Null n))
(f3 : forall (n : Name) (v : Vals), P0 (SingleResult n v))
(f4 : forall (n : Name) (l : seq Vals), P0 (ListResult n l))
(f5 : forall (n : Name) (r : ResponseObject), P r -> P0 (NestedResult n r))
(f6 : forall (n : Name) (l : seq ResponseObject),
P1 l -> P0 (NestedListResult n l))
(f7 : P1 [::])
(f8 : forall (ro : ResponseObject), P ro ->
forall (l : seq ResponseObject),
P1 l -> (P1 (ro :: l))) (ro : ResponseObject) =>
fix F (r : ResponseObject) : P r :=
match r as r0 return (P r0) with
| SingleResponse r0 => f r0 (F0 r0)
| MultipleResponses r0 r1 => f0 r0 (F0 r0) r1 (F r1)
end
with F0 (r : Result) : P0 r :=
match r as r0 return (P0 r0) with
| Empty => f1
| Null n => f2 n
| SingleResult n v => f3 n v
| ListResult n l => f4 n l
| NestedResult n r0 => f5 n r0 (F r0)
| NestedListResult n l => f6 n l
((fix F1 l' : P1 l' :=
match l' with
| [::] => f7
| ro :: l' => f8 ro (F ro) l' (F1 l')
end) l)
end
for F0.
该解决方案是通过调用Scheme
命令然后编辑标题(添加P1
和用于序列)f7
并f8
最后编辑NestedListResult
构造的大小写来产生的。
推荐阅读
- python - 无论我做什么,超级简单的 Flask 应用程序的云构建都失败了
- google-maps - Google Maps 实例中 Koeppen-Geiger 气候区的准确多边形构造
- angular - 注入 SQLitePorter 给出错误:此构造函数与 Angular 依赖注入不兼容
- dependency-injection - .Net core 3.1 - IHosted 服务(AddHostedService
) 没有解决依赖注册 - python - 删除的。为什么不明显?
- hive - 特定表上的 SQL 在 Hive 中总是失败,在 Impala 中有效
- twitter-bootstrap - 如何在 Bootstrap 5 中创建 jumbotron?
- html - 为什么我必须单击两次才能在 jQuery 中切换()
- reason - 可变数量的孩子
- c# - Xamarin 绑定不适用于列表视图