Coq案例分析并使用返回子集类型的函数进行重写 [英] Coq case analysis and rewrite with function returning subset types

问题描述

我正在做这个关于使用子集类型编写认证功能的简单练习.这个想法是先编写一个前置函数

I was working is this simple exercise about writing certified function using subset types. The idea is to first write a predecessor function

pred : forall  (n : {n : nat | n > 0}), {m : nat | S m = n.1}.

然后使用此定义给出功能

and then using this definition give a funtion

pred2 : forall (n : {n : nat | n > 1}), {m : nat | S (S m) = n.1}.

我对第一个没有问题.这是我的代码

I have no problem with the first one. Here is my code

Program Definition pred (n : {n : nat | n > 0}) : {m : nat | S m = n.1} :=
  match n with
  | O => _
  | S n' => n'
  end.
Next Obligation. elimtype False. compute in H. inversion H. Qed.

但是我不能锻炼第二个定义.我试图写这些定义

But I cannot workout the second definition. I trying to write these definition

Program Definition pred2 (n : {n : nat | n > 1}) : {m : nat | S (S m) = n.1} 
:= pred (pred n).

我设法证明了两项首要义务

I managed to prove the two first obligations

Next Obligation. apply (gt_trans n 1 0). assumption. auto. Qed.
Next Obligation. 
  destruct pred.  
  simpl.
  simpl in e. 
  rewrite <- e in H.
  apply gt_S_n in H; assumption.
Qed.

但是对于最后一项义务，我陷入了困境，因为当我尝试对pred的返回类型进行案例分析时，新的假设不会在目标中被重写.

But for the last obligation I get stuck because when I try to do a case analysis for the return type of pred the new hypotesis are not rewrited in the goal.

我尝试了以下策略，但没有结果.

I tried the following tactics with no results.

destruct (pred (n: pred2_obligation_1 (n ; H))).

destruct (pred (n; pred2_obligation_1 (n ; H))) eqn:?.
rewrite Heqs.

我知道我可以直接编写pred2，但是这个想法是使用和编写pred函数.

I know that I can with write pred2 directly, but the idea is to use and compose the function pred.

推荐答案

destruct没有任何作用的原因可能是因为您要进行案例分析的目的未在目标中发生.该术语的隐式参数可能与目标中该术语的隐式参数不匹配.无论哪种方式，您都必须在目标不正确的情况下对该词进行案例分析.

The reason destruct doesn't have any effect is probably because what you're trying to do case analysis on doesn't occur in the goal. The implicit arguments of that term probably don't match the implicit arguments of the term in the goal. Either way, you can't do case analysis on that term without making the goal ill-typed.

但是您可以通过对n进行案例分析来证明这一义务.

But you can prove that obligation by case analysis on n.

Next Obligation.
destruct n.
inversion H.
destruct n.
inversion H.
subst.
inversion H1.
cbn.
eauto.
Qed.

我也能够证明一些辅助定理，但是由于所有类型依赖关系，我无法使用它们.

I was also able to prove some helper theorems, but I wasn't able to use them because of all the type dependency.

Theorem T1 : forall s1, S (` (pred s1)) = ` s1.
Proof. intros [[| n1] H1]. inversion H1. cbn. eauto. Qed.

Theorem T2 : forall T1 (P1 : T1 -> Prop) s1 H1, (forall x1 (H1 H2 : P1 x1), H1 = H2) -> exist P1 (` s1) H1 = s1.
Proof. intros ? ? [x1 H1] H2 H3. cbn in *. rewrite (H3 _ H1 H2). eauto. Qed.

我从没见过在功能上使用destruct.我很惊讶Coq不会抱怨该函数不是归纳定义的.

I had never seen destruct used on a function. I'm surprised Coq doesn't complain that that function isn't inductively defined.

这篇关于Coq案例分析并使用返回子集类型的函数进行重写的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！