时间戳

首页 > 解决方案 > 克服在另一个构造函数的定义中有构造函数的需要

coq - 克服在另一个构造函数的定义中有构造函数的需要

问题描述

很可能我正在尝试实现一些有缺陷的东西，但是我遇到了在另一个构造函数的定义中需要一个构造函数。

愚蠢的例子：

Inductive silly_type : Type :=
| constr1 : nat -> silly_type
| constr2 : forall (x : silly_type), (exists n : nat, (x = constr1 n)) -> silly_type.

有两种方法可以创建 的元素silly_type，或者使用自然数，constr1或者使用创建的constr2元素。silly_typeconstr1

上面的定义silly_type在 coq 中无效，但我不知道如何在我不太愚蠢的示例中克服这一点。

不那么愚蠢的例子：

我试图有一个expr表示类型表达式的归纳类型。

让我们首先从表示类型的归纳类型开始：

Inductive type : Type :=
| base_type  : nat -> type
| arrow_type : type -> type -> type
| iso_arrow_type   : type -> type -> type.

有一些用整数索引的基本类型，arrow_type表示类型之间的函数和iso_arrow_type表示类型之间的可逆函数。

符号：

Notation "A --> B" := (arrow_type A B)   (at level 30, right associativity).
Notation "A <-> B" := (iso_arrow_type A B).

输入表达式：

Inductive expr : type -> Type :=
| var  : forall (X : type) (n : nat), expr X
| eval : forall {X Y : type} (f : expr (X --> Y)) (x : expr X), expr Y
| inv  : forall {X Y : type}, expr ((X <-> Y) --> (Y <-> X))
| to_fun : forall {X Y : type}, expr ((X <-> Y) --> (X --> Y))
| to_iso : forall {X Y : type} (f : expr (X --> Y)), (is_invertible f) -> expr (Y --> X).

您可以使用 来创建任何类型的索引变量，使用var来评估函数eval，使用 来反转可逆函数inv，使用 将可逆函数转换为实际函数，to_fun这样您就可以使用 来评估它eval。

问题出在最后一个构造函数上to_iso。有时，我会知道函数（的元素X --> Y）实际上是可逆的，我想要一些机制将其转换为类型X <-> Y。

但是，要定义is_invertible我认为我需要使用eval. 这让我想到了构造函数eval需要在构造函数的定义中的问题to_iso。

要定义is_invertible，我们首先需要定义 的相等概念expr：

Inductive ExprEq : forall (X : type),  X ->  X -> Prop :=
| expr_eq_refl : forall {X : type}, forall (x : X), ExprEq X x x
| eq_on_values : forall {X Y : type}, forall (f g : (X --> Y)), (forall (x : X), f[x] == g[x]) -> f == g
where 
"x == y" := (ExprEq _ x y) and "f [ x ]" := (eval f x) and "x =/= y" := (not (ExprEq _ x y)).

因此，我们有标准的自反性x == x，函数的相等性f==g可以由所有元素的相等性来决定f[x]==g[x]。

现在，我们准备好定义is_invertible：

Definition is_invertible {X Y : type} (f : X --> Y) : Prop := exists g : Y --> X, (forall x, g[f[x]] == x) /\ (forall y, f[g[y]] == y).

这个定义is_invertible是有问题的，它使用eval（f[x] := (eval f x)）。此外，问题有点复杂。我们需要定义ExprEq已经用于eval定义其构造函数的类型。

约束：保持expr可判定

我真正想要保留的是equal( =)expr是可判定的，即能够证明

Lemma eq_expr_dec {X : type} (x y : type) : {x=y} + {x<>y}.

我真的不关心定义的相等==性的可判定性，但可判定性=对我来说很重要。

标签： coq

解决方案

您可以使用依赖类型来索引您的构造函数。例如

Inductive silly_type : nat -> Type :=
| constr1 : nat -> silly_type 0
| constr2 : silly_type 0 -> silly_type 1.

所以你只能在 constr2 中使用由 constr1 产生的值。这种方法通常可以区分使用不同构造函数创建的值。

推荐阅读