coq - 为什么这个重写在依赖类型的上下文中失败

Question

我试图摆脱依赖类型，但我不断遇到如下问题。在这个例子中，我为数组定义了一个抽象，这样每次访问都被保护在使用依赖类型的数组中。

我使用的是 Coq 8.5，但我认为这在本例中不是必需的。我还使用了软件基础教程中的 SfLib 和 LibTactics。对于后者，我找到了一个可以与 Coq 8.5 一起工作的。

Add LoadPath "/home/bryan/Projects/Coq/sf8.5".
Require Import SfLib.      (* In the download from https://www.cis.upenn.edu/~bcpierce/sf/current/index.html *)
Require Import LibTactics. (* https://github.com/DDCSF/iron/blob/master/done/Iron/Tactics/LibTactics.v *)

Require Import Omega.

Module Array.

接下来是数组的归纳和抽象定义。

  Inductive array {E: Type} (sz: nat) : Type :=
  | construct_array : forall f : nat -> option E, (forall i, i >= sz <-> f i = None) -> array sz
  .

接下来有几个引理无疑在标准库中以某种方式可用，但除了第二个我找不到它们，但那只在经典逻辑部分。

  Lemma transpose: forall f g : Prop, (f -> g) -> (~ g -> ~ f).
  Proof.
    auto.
  Qed.

  Lemma not_ex_all_not :
   forall U (P:U -> Prop), ~ (exists n, P n) -> forall n:U, ~ P n.
  Proof. (* Intuitionistic *) 
    unfold not. intros U P notex n abs.
    apply notex. 
    exists n; trivial. 
  Qed.

以下引理描述了数组的定义。证明感觉就像是力的妙招，所以如果您有任何简化建议，请务必提出。

  Lemma inside_array: forall E (f: nat -> option E) sz
  ,   (forall i, i >= sz <-> f i = None) 
  <-> (forall i, i < sz <-> exists e, f i = Some e)
  .   
  Proof.  
    introv. split; split.
    introv Hi. remember (f i) as fi. destruct fi.
      exists e. reflexivity.
      symmetry in Heqfi. rewrite <- H in Heqfi. exfalso. omega.
    introv Hex. inversion Hex as [e He]; clear Hex.
    specialize (H i). rewrite He in H. inversion H; clear H.
    apply transpose in H0. SearchAbout ge. apply not_ge in H0. assumption.
    intro Hcontra. inversion Hcontra.
    intro Hi. specialize (H i). inversion H.
    apply transpose in H1. assert (forall e, ~ f i = Some e). apply not_ex_all_not. assumption.
    destruct (f i). specialize (H2 e). exfalso. auto. reflexivity.
    omega.
    intros Hi. specialize (H i). inversion H. apply transpose in H0. omega. rewrite Hi.
    intro Hcontra. inversion Hcontra as [e Hcontra']. inversion Hcontra'.
  Qed.

查找数组中的元素，前提是索引在范围内

  Definition lu_array {E: Type} {sz: nat} (a: @array E sz) (i: nat) (C: i < sz) : E.
  Proof.  
    intros.
    inversion a.
    remember (f i) as elem.
    destruct (elem).
      apply e. symmetry in Heqelem. rewrite <- H in Heqelem.
      exfalso. omega.
  Defined.

通过在前面放置新元素来调整数组大小

 Definition inc_l_array {E: Type} {sz: nat} (a: @array E sz) (inc: nat) (d: E) : @array E (inc + sz).
 Proof.
    destruct a as [f Hi].
    apply construct_array
      with (fun j => if lt_dec j inc then Some d else if lt_dec j (inc + sz) then f (j - inc) else None).
    introv. split; destruct (lt_dec i inc); simpl.
    Case "i < inc ->". introv Hi'. exfalso. omega.
    Case "i >= inc ->". introv Hi'. destruct (lt_dec i (inc + sz)).
      SCase "i < (inc + sz)". exfalso. omega.
      SCase "i >= (inc + sz)". reflexivity.
    Case "i < inc <-". introv Hcontra. inversion Hcontra.
    Case "i >= inc <-". destruct (lt_dec i (inc + sz)).
      SCase "i < (inc + sz)". rewrite <- Hi. omega.
      SCase "i >= (inc + sz)". introv Htriv. omega.
  Defined.

接下来是有问题的引理，它指定了调整大小应该做什么。大多数证明都失败了，但我被标记的重写卡住了。

  Lemma inc_l_array_spec
  :   forall E sz (a: @array E sz) (inc: nat) (d: E) (a': @array E (inc + sz))
  ,   inc_l_array a inc d = a'
      ->  forall i (Ci' : i < inc + sz)
      ,   (   i < inc -> lu_array a' i Ci' = d)
      /\  (   inc <= i < inc + sz
          ->  exists (Ci: i-inc < sz), lu_array a' i Ci' = lu_array a (i-inc) Ci
          )
  .
  Proof.
    introv Heq. introv. subst a'. destruct a as [f Hf]. split; introv Hin.
    Case "i < inc". simpl.
      unfold inc_l_array, lu_array.
      destruct (lt_dec i inc).
      SCase "i < inc". reflexivity.
      SCase "i >= inc". contradiction.  
    Case "inc <= i < inc+sz".
      assert (Ci: i-inc < sz) by omega. exists Ci.
      unfold inc_l_array, lu_array. 
      destruct (lt_dec i inc).
      SCase "i < inc". exfalso. omega. 
      SCase "i >= inc". destruct (lt_dec i (inc+sz)).
        SSCase "i < inc + sz".
          assert (Hf': forall i, i < sz <-> exists e, f i = Some e).
          apply inside_array. assumption.
          specialize (Hf' (i-inc)). inversion Hf'. remember Ci as Ci''. clear HeqCi''. apply H in Ci.
          inversion Ci as [e He].
          rewrite He. (* <---- This rewrite fails *)

        SSCase "i >= inc + sz".
          exfalso. omega. 
  Qed.

End Array.

我试过用其他方法解决这个问题，但总是遇到这个问题。错误消息如下所示:

Error: Abstracting over the term "f (i - inc)" leads to a term
fun o : option E => (... very long term ...) which is ill-typed.
Reason is: Illegal application: 
The term "@RelationClasses.symmetry" of type
 "forall (A : Type) (R : Relation_Definitions.relation A),
  RelationClasses.Symmetric R -> forall x y : A, R x y -> R y x"
cannot be applied to the terms
 "Prop" : "Type"
 "iff" : "Prop -> Prop -> Prop"
 "RelationClasses.iff_Symmetric" : "RelationClasses.Symmetric iff"
 "i - inc >= sz" : "Prop"
 "o = None" : "Prop"
 "Hf (i - inc)" : "i - inc >= sz <-> f (i - inc) = None"
The 6th term has type "i - inc >= sz <-> f (i - inc) = None"
which should be coercible to "i - inc >= sz <-> o = None".

o = None 在我看来是罪魁祸首，因为它似乎涵盖了我目前实际上没有处理的案例。但老实说，我不明白发生了什么。第六学期提到的f (i - inc)也让我很担心，因为我打算重写它。

上述方法将依赖证明无关性来连接依赖于类型的守卫。但是我不明白如何在上述情况下调用这个公理。

我的具体问题是:为什么重写会失败？我该如何补救？

Answer 1

我仔细看了看你在做什么，确实这里有一些评论:

• 你依赖于透明的证据，这通常有点潘多拉盒子，因为你的一些证明条款将是“不透明的”，并且在一般会让事情变得有点困难。
• 您可以尝试将更多证据和“数据”分开。
• 您也可以尝试使用更多的“计算”定义。那就是，为什么不用数组作为实际列表？

下面是我用 5 分钟处理您的代码的过程，希望对您有所帮助。

From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Array.

Variable E : Type.
Implicit Types N   : nat.

Definition i_fun := nat -> option E.
Implicit Types arr : i_fun.
Identity Coercion i_fun_c : i_fun >-> Funclass.

(* A maybe better approach would be to work with reflect predicates *)
(* Definition up_axiom arr N := forall i, *)
(*     reflect (arr i = None) (N <= i). *)

Definition up_axiom arr N := forall i,
    (arr i = None) <-> (N <= i).

Definition down_axiom arr N := forall i,
    (exists e, arr i = Some e) <-> (i < N).

Definition array N := { arr | up_axiom arr N }.

Coercion arr_fun N (arr : array N) := tag arr.

(* Sadly we can't fully reflect this *)
Lemma inside_array arr N : up_axiom arr N <-> down_axiom arr N.
Proof.
split=> ax i; split.
+ by case=> [e he]; rewrite ltnNge; apply/negP/ax; rewrite he.
+ move=> hi; case Ha: (arr i) => [w|]; first by exists w.
  by move/ax: Ha; rewrite leqNgt hi.
+ have := ax i; case: (arr i) => // -[h1 h2 _].
  by rewrite leqNgt; apply/negP=> /h2 [].
+ have := ax i; case: (arr i) => // e [h1 h2].
  have H: i < N; first by apply: h1; exists e.
  by rewrite leqNgt H.
Qed.

(* This being transparent was not very useful... *)
Definition optdef T d (e : option T) : T :=
  match e with
  | Some x => x
  | None => d
  end.

Definition get_array N d arr (i : nat) : E :=
  optdef d (arr i).

Definition inc_array N arr (inc : nat) (d: E) : i_fun :=
  fun i =>
  if i < N       then arr i else
  if i < N + inc then Some d else
  None.

Lemma inc_arrayP N (arr : array N) inc d :
  up_axiom (inc_array N arr (N+inc) d) (N+inc).
Proof.
case: arr => a_f a_ax i; have [h1 h2] := a_ax i.
rewrite /inc_array /arr_fun; case: ifP => hi /=.
+ split; [move/h1; rewrite leqNgt hi //|].
  move=> hil; rewrite (leq_trans (leq_addr inc _)) // in h2.
  exact: h2.