Why does this rewrite fail in the context of dependent types

Question

I'm trying to get a hang on dependent types, but I continuously run into a problem like the following. In this example I'm defining an abstraction for arrays, such that every access is guarded to be in the array using dependent typing.

I'm using Coq 8.5, but I don't think that is essential in this example. I'm also using the SfLib and LibTactics from the Software Foundations tutorial. For the latter I found one that does work with 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.

Next follows the inductive and abstract definition of an array.

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

Next a couple of lemmas that no doubt are somehow available in the standard library, but I couldn't find them except for the second, but that was only in the Classical logic part.

  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.

The following lemma characterizes the definition of an array. The proof feels like a coup the force, so if you have any suggestions for simplification then by all means.

  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.

Look up an element in an array, provided the index is in range

  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.

Resize the array by placing new elements at the front

 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.

And next the problematic lemma that specifies what the resize should do. Most of the proof falls through, but I get stuck at the marked rewrite.

  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.

I've tried working my way around it in some other ways, but it always hits this problem. The error message looks like:

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".

The o = None looks to me like the culprit, because it seems to cover a case that I'm actually not handling at the moment. But honestly, I don't understand what is going on. The mentioning of f (i - inc) in the 6th term is also worrying me, as I intended to rewrite it away.

The above approach will rely on proof irrelevance to connect the type dependent guards. I do not understand however how to invoke this axiom in the above situation.

My concrete questions are: why does the rewrite fail? And how can I remedy this?

Hi Brian, actually your question touches too many interesting and deep topics in Coq so it won't easy to answer it quickly. The strategy I can suggest for now is that you try to break your proof down in individual, small lemmas. The best solution to these dependent typing problems is usually a careful design. In particular, your rewrite failure is quite common and is due to type families constructors. — ejgallego
For instance, imagine you have a constructor P: Vector.t (S n) and you have something like X = P, a equality between the two terms at type Vector.t (S n). Then, rewriting S n = n + 1 leads to an ill-typed term as P cannot be typed as Vector.T (n + 1). A direct solution is to "abstract" the index S n itself, but this may be hard in general, so defining an external lemma is usually the best way. — ejgallego

ejgallego ejgallego · Accepted Answer · 2016-04-19T19:37:00

I had a closer look at what you are doing and indeed here are a few comments:

You are relying on transparent proofs, this is in general a bit of a pandora box, as some of your proof terms will be "opaque", and in general will make things a bit difficult.
You could try thus to separate a bit more proofs and "data".
You could also try to have more "computational" definitions. That is, why not to have an array as an actual list?

See below for my 5 mins take on your code, I hope it helps.

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.

Why does this rewrite fail in the context of dependent types

1 Answers