尝试实施
我正在尝试实现一个函数extract，它将像(f (g x y))这样的表达式与变量一起使用，例如y并产生带有SKI运算器的函数y --> (f (g x y))。在这种情况下，结果应为(S (K f) (g x))。
从某种意义上说，我正在从 lambda 术语转换为其 SKI 版本。
我正在尝试做一个打字版本，但我遇到了困难。
建立
这些表达式中的类型由以下归纳类型表示
Inductive type : Type :=
| base_type : forall (n : nat), type
| arrow_type : type -> type -> type.
基本上，我有一些由整数(base_type)索引的基本类型，并且我可以在它们之间创建函数类型(arrow_type)
引入函数类型的表示法
Notation "A --> B" := (arrow_type A B) (at level 30, right associativity).
表达式由以下归纳类型表示
Inductive term : type -> Type :=
| var : forall (n : nat) (A : type), term A
| eval : forall {A B : type}, term (A-->B) -> term A -> term B
| I : forall (A : type) , term (A --> A)
| K : forall (A B : type) , term (A --> (B --> A))
| S : forall (A X Y : type), term ((A --> X --> Y) --> (A --> X) --> A --> Y).
在这里，我再次设置了按整数n : nat索引的基本变量和一个类型A : type(不是Type！
因此，变量x : term X是具有typeX的表达式。
为了减少碍眼，让我们引入函数计算的符号
Notation "f [ x ]" := (eval f x) (at level 25, left associativity).
介绍性示例
原来的问题可以更准确地说明如下。
让我们从定义一些类型开始
Notation X := (base_type 0).
Notation Y := (base_type 1).
定义变量x y和函数f g(它们可以全部索引为 0，因为它们都有不同的type)
Notation x := (var 0 X).
Notation y := (var 0 Y).
Notation g := (var 0 (X --> Y --> X)).
Notation f := (var 0 (X --> Y)).
生成的表达式的type为Y。
Check f[g[x][y]].
我的目标是生成一个函数extract使得
extract f[g[x][y]] y
生产
S[K[f]][g[x]]
填写了类型
(S Y X Y)[(K (X-->Y) Y)[f]][g[x]]
type和term平等
要继续尝试定义extract我需要定义type和term的相等性。
Require Import Arith.EqNat.
Open Scope bool_scope.
Fixpoint eq_type (A B : type) : bool :=
match A, B with
| base_type n, base_type m => beq_nat n m
| arrow_type X Y, arrow_type X' Y' => (eq_type X X') && (eq_type Y Y')
| _, _ => false
end.
Fixpoint eq_term {A B : type} (a : term A) (b : term B) : bool :=
match a, b with
| var n X , var n' X' => (beq_nat n n') && (eq_type X X')
| eval X Y f x , eval X' Y' f' x' => (eq_type X X') && (eq_type Y Y') && (eq_term f f') && (eq_term x x')
| I X , I X' => (eq_type X X')
| K X Y , K X' Y' => (eq_type X X') && (eq_type Y Y')
| S Z X Y , S Z' X' Y' => (eq_type X X') && (eq_type Y Y') && (eq_type Z Z')
| _ , _ => false
end.
尝试实施extract
"实现"非常简单
Fixpoint extract {A B : type} (expr : term B) (val : term A) : term (A-->B) :=
if (eq_term expr val)
then (I A)
else
match expr with
| eval X Y f x => (S A X Y)[extract f val][extract x val]
| _ => (K B A)[expr]
end.
有两个问题
- 返回
I A时：typeI AA --> A没有承诺A --> B，但在这种特殊情况下，我应该能够证明B和A是相同的。 - 返回
(S A X Y)[...时：返回值是A --> Y而不是A --> B，但我应该能够再次证明Y等于B。
在这些特定情况下，如何证明B=A和Y=B，以便接受函数定义？
你可以做的是将布尔函数的eq_type和eq_term转换为相等的决策过程。 目前，据我所知，你的平等完全是句法上的。 所以你可以简单地用Coq的平等概念来谈论术语和类型的平等。 然后，您可以编写：
Definition eq_type_dec (A B : type) : { A = B } + { A <> B }.
你几乎在A和B上做模式匹配，然后为相等的情况返回left eq_refl，在其他情况下right ...，...是你需要做的任何事情来证明不平等。
执行相同的操作并定义eq_term_dec。 这里有两个选择，要么使类型的平等是内在的，要么是外在的：
Definition eq_term_dec (A B : type) (a : A) (b : B) :
{ (A = B) * (existT (fun t => t) A a = existT (fun t => t) B b) }
+
{ (A <> B) + (existT (fun t => t) A a <> existT (fun t => t) B b) }.
或：
Definition eq_term_dec (A : type) (a b : term A) : { a = b } + { a <> b }.
第一个似乎写起来很糟糕，但给了你更多的灵活性。 我可能会喜欢后者，并在处理可能不相等的类型时eq_type_check下使用它。
一旦你有了这些，你可以把你的if变成一个依赖match：
Fixpoint extract {A B : type} (expr : term B) (val : term A) : term (A-->B) :=
match eq_type_dec A B with
| left eqAB =>
match eqAB
in eq _ B1
return term B1 -> term (A --> B1)
with
| eq_refl => fun expr1 => (* now expr1 : A *)
match eq_expr_dec _ _ expr1 val with
| left eqab => I A
| right neqab => (* ... *)
end
end expr (* note here we pass the values that must change type *)
| right neqAB => (* ... *)
end.
在我省略的分支中可能还有相当多的工作要做。您可以查看执行此类依赖类型编程的不同方法，例如我在此处所示的手动操作，或者使用依赖消除策略，或者使用这些类型的递归器。
编辑
为了回答您的评论，以下是我所知道的写eq_term_dec的 twp 方法。 一种方法是使用 Coq 的Program扩展，它添加一个公理，并且更有能力处理依赖类型：
Require Import Program.Equality.
Fixpoint eq_term_dec (A : type) (a b : term A) : { a = b } + { a <> b }.
dependent induction a; dependent induction b; try (right ; congruence).
- destruct (PeanoNat.Nat.eq_dec n n0); [ left | right ]; congruence.
另一种方法是实际找出您需要的依赖类型术语。 必须有一种方法可以使用策略来做到这一点，但我不太确定如何进行，但是，我知道如何写这个词。 它不适合胆小的人，我不希望你在熟悉依赖模式匹配和"护航模式"之前了解发生了什么。 如果你想看看这是什么样子的，这里是：
Fixpoint eq_term_dec (A : type) (a b : term A) : { a = b } + { a <> b }.
revert b.
destruct a.
{
destruct b; try (right ; congruence).
destruct (PeanoNat.Nat.eq_dec n n0) ; [ left | right ] ; congruence.
}
{ destruct b; admit. (* skipping this, it's easy *) }
{
(* Here is the complication: *)
(* `b` has type `term (A -> A)` *)
(* If you abstract over its type, the goal is ill-typed, because the equality *)
(* `I A = b` is at type `A -> A`. *)
intros b.
refine (
(fun (T : type) (ia : term T) (b : term T) =>
match b
as b1
in term T1
return forall (ia0 : term T1),
match T1 as T2 return term T2 -> term T2 -> Type with
| arrow_type Foo Bar => fun ia1 b2 => {ia1 = b2} + {ia1 <> b2}
| _ => fun _ _ => True
end ia0 b1
with
| var n a => fun b => _
| eval h a => fun b => _
| I A => fun b => _
| K A B => fun b => _
| S A B C => fun b => _
end ia
) (A --> A) (I A) b
).
(* from now on it's easy to proceed *)
destruct a.
easy.
destruct b; try ( right ; congruence ).
destruct (PeanoNat.Nat.eq_dec n n0) ; [ left | right ] ; congruence.
(* one more to show it's easy *)
destruct t0.
easy.
destruct b; try ( right ; congruence ).
(* etc... *)
我有一个解决方案，它并不漂亮，但它似乎有效。尤其是，eq_term_dec的证明超长而丑陋。
如果有人感兴趣，我的解决方案：
Inductive type : Type :=
| base_type : forall (n : nat), type
| arrow_type : type -> type -> type.
Notation "A --> B" := (arrow_type A B) (at level 30, right associativity).
Inductive term : type -> Type :=
| var : forall (n : nat) (A : type), term A
| eval : forall {A B : type}, term (A-->B) -> term A -> term B
| I : forall {A : type} , term (A --> A)
| K : forall {A B : type} , term (A --> (B --> A))
| S : forall {A X Y : type}, term ((A --> X --> Y) --> ((A --> X) --> (A --> Y))).
(* Coercion term : type >-> Sortclass. *)
Notation "n :: A" := (var n A).
Notation "f [ x ]" := (eval f x) (at level 25, left associativity).
Fixpoint eq_type_dec (A B : type) : {A = B} + {A <> B}.
Proof.
decide equality.
decide equality.
Defined.
Require Import Coq.Logic.Eqdep.
Fixpoint eq_term_dec {A B : type} (a : term A) (b : term B) :
( (A = B) * (existT (fun T : type => term T) A a = existT (fun T : type => term T) B b) )
+
( (A <> B) + (existT (fun T : type => term T) A a <> existT (fun T : type => term T) B b) ).
Proof.
case a as [n X| X Y f x | X | X Y | Z X Y], b as [n' X'| X' Y' f' x' | X' | X' Y' | Z' X' Y'].
(* var n X ? var n' X'*)
- assert (ndec : {n=n'} + {n<>n'}) by decide equality.
pose (Xdec := eq_type_dec X X').
destruct ndec as [eqn | neqn], Xdec as [eqX | neqX].
left.
rewrite eqn.
rewrite eqX.
split; reflexivity.
right; left. apply neqX.
right; right.
intro H; inversion H as [H1]. auto.
right; left. apply neqX.
- right; right; intro H; inversion H. (* n ? f[x] *)
- right; right; intro H; inversion H. (* n ? I *)
- right; right; intro H; inversion H. (* n ? K *)
- right; right; intro H; inversion H. (* n ? S *)
- right; right; intro H; inversion H. (* f[x] ? n *)
- pose (xdec := eq_term_dec _ _ x x').
pose (fdec := eq_term_dec _ _ f f').
destruct xdec, fdec.
(* x = x' && f = f' *)
left.
split.
apply fst in p0.
inversion p0.
auto.
apply snd in p0.
inversion p0.
revert dependent x.
revert dependent f.
rewrite H0.
rewrite H1.
intros.
apply snd in p.
assert (x=x'). apply inj_pair2; apply p.
assert (f=f'). apply inj_pair2; apply p0.
rewrite H, H3. auto.
right.
destruct s.
left. intro.
apply fst in p.
assert (X-->Y = X' --> Y').
rewrite H, p.
auto. auto.
right. intro.
inversion H.
apply n.
revert dependent x.
revert dependent f.
rewrite H1.
rewrite H2.
intros.
apply inj_pair2 in H4.
apply inj_pair2 in H4.
rewrite H4.
auto.
right.
destruct s.
inversion p.
inversion H.
auto.
inversion p.
inversion H0.
revert dependent x.
revert dependent f.
rewrite H2.
rewrite H3.
intros.
apply inj_pair2 in H0.
rewrite H0.
right.
intro.
apply inj_pair2 in H1.
inversion H1. auto.
destruct s, s0.
right. right.
intro. inversion H. auto.
right. right.
intro. inversion H. auto.
right. right.
intro. inversion H. auto.
right. right.
intro. inversion H. auto.
- right; right; intro H; inversion H. (* f[x] ? I *)
- right; right; intro H; inversion H. (* f[x] ? K *)
- right; right; intro H; inversion H. (* f[x] ? S *)
- right; right; intro H; inversion H. (* I ? n *)
- right; right; intro H; inversion H. (* I ? f[x] *)
- pose (Xdec := eq_type_dec X X'). (* I ? I *)
destruct Xdec.
left; split; rewrite e; auto.
right; left. intro. inversion H. auto.
- right; right; intro H; inversion H. (* I ? K *)
- right; right; intro H; inversion H. (* I ? S *)
- right; right; intro H; inversion H. (* K ? n *)
- right; right; intro H; inversion H. (* K ? f[x] *)
- right; right; intro H; inversion H. (* K ? I *)
- pose (Xdec := eq_type_dec X X').
pose (Ydec := eq_type_dec Y Y').
destruct Xdec, Ydec.
left; split; rewrite e; rewrite e0; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
- right; right; intro H; inversion H. (* K ? S *)
- right; right; intro H; inversion H. (* S ? n *)
- right; right; intro H; inversion H. (* S ? f[x] *)
- right; right; intro H; inversion H. (* S ? I *)
- right; right; intro H; inversion H. (* S ? K *)
- pose (Xdec := eq_type_dec X X').
pose (Ydec := eq_type_dec Y Y').
pose (Zdec := eq_type_dec Z Z').
destruct Xdec, Ydec, Zdec.
left; split; rewrite e; rewrite e0; rewrite e1; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
right; left; intro; inversion H; auto.
Defined.
Fixpoint extract {A B : type} (expr : term B) (val : term A) : term (A-->B).
Proof.
pose (ab_dec := eq_term_dec expr val).
destruct ab_dec.
(* expr is equal to val *)
apply fst in p; rewrite p; apply I.
(* expr is not equal to val *)
inversion expr as [n X | X Y f x | X | X Y | Z X Y].
(* expr is just a constant, i.e. expr = var n X *)
apply (K[expr]).
(* expr is a function evaluation, i.e. expr = f[x]*)
apply (S[extract _ _ f val][extract _ _ x val]).
(* expr is identity, i.e. expr = I *)
rewrite H; apply (K[expr]).
(* expr is constant function, i.e. expr = K *)
rewrite H; apply (K[expr]).
(* expr is constant function, i.e. expr = S *)
rewrite H; apply (K[expr]).
Defined.
Notation X := (base_type 0).
Notation Y := (base_type 1).
Notation x := (var 0 X).
Notation y := (var 0 Y).
Notation f := (var 0 (X --> Y --> X)).
Compute extract (f[x]) x. (* => S [K [f]] [I] *)
Compute extract (f[x][y]) x. (* => S [S [K [f]] [I]] [K [y]] *)