The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Is it strange at all then that I can get IList.v through the type checker without using -impredicative-set, including the recursor and induction?

Are you using Proof General to run the file ? If so, the first line of the file:

 (* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)

automatically passes the -impredicative-set flag to Coq.

PS: I juste noticed that this conversation has been going partially in private and partially on the public list. For the benefit of all, let me attach my file to this mail.

(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *)

Require Coq.Lists.List.

Definition IList (A:Set) : Set :=
  forall R:Set, (A->R->R) -> R -> R
.

Definition empty {A:Set} : IList A :=
  fun R c e => e
.
Arguments empty {A} R c e /.

Definition single {A:Set} (x:A) : IList A :=
  fun R c e => c x e
.
Arguments single {A} x R c e /.

Definition app {A:Set} (l r:IList A) : IList A :=
  fun R c e => l R c (r R c e)
.
Arguments app {A} l r R c e /.

Notation "l ++ r" := (app l r).

Definition cons {A:Set} (x:A) (l:IList A) : IList A := (single x)++l.
Arguments cons {A} x l R c e /.


Remark app_empty_neutral_r : forall A (l:IList A), l++empty = l.
Proof.
  intros **.
  reflexivity.
Qed.

Remark app_empty_neutral_l : forall A (l:IList A), empty++l = l.
Proof.
  intros **.
  reflexivity.
Qed.

Remark app_associative : forall A (l r q:IList A), (l++r)++q = l++(r++q).
Proof.
  intros **.
  reflexivity.
Qed.

Definition fold_right {A B:Set} (f:A->B->B) (s:B) (l:IList A) : B := l B f s.

Definition ilist_rec0 {A B:Set} (s:B) (f:A->IList A->B->B) (l:IList A) : B :=
  snd (fold_right (fun a lb => (cons a (fst lb) , f a (fst lb) (snd lb))) (empty,s) l)
.

(** Parametricity and is needed to show that impredicative lists are equivalent to lists *)

Notation "A ⇔ B" := (A->B->Prop) (at level 70).

Definition arrow_rel {A A' B B':Type} (rA:A⇔A') (rB:B⇔B') : (A->B)⇔(A'->B') :=
  fun f g => forall x y, rA x y -> rB (f x) (g y)
.
Arguments arrow_rel {A A' B B'} rA rB f g /.
Notation "rA ⟶ rB" := (arrow_rel rA rB) (at level 70, right associativity).

Definition forall_rel {B₁:Set->Set} {B₂:Set->Set}
(rB:forall (A₁ A₂:Set) (r:A₁⇔A₂), B₁ A₁⇔B₂ A₂) : (forall x, B₁ x) ⇔ (forall x, B₂ x) :=
  fun f g => forall (A₁ A₂:Set) (rA:A₁⇔A₂), rB A₁ A₂ rA (f A₁) (g A₂)
.
Notation "∀ ( r : A₁ ⇔ A₂ ) , rB" := (forall_rel (fun A₁ A₂ r => rB)) (at level 90, r ident, A₁ ident, A₂ ident).

Definition Parametric {A:Set} (rA:A⇔A) (l:IList A) : Prop :=
   (∀ (r:R⇔R'), (rA ⟶ r ⟶ r) ⟶ r ⟶ r) l l
.

Definition list_to_ilist {A:Set} (l:list A) : IList A :=
  List.fold_right cons empty l
.

Definition ilist_to_list {A:Set} (l:IList A) : list A :=
  fold_right (@List.cons _) List.nil l
.

Lemma list_retract : forall (A:Set) (l:list A), ilist_to_list (list_to_ilist l) = l.
Proof.
  intros A l.
  induction l as [|x l h].
  + easy.
  + simpl. unfold cons,single,app,ilist_to_list,fold_right in *.
    congruence.
Qed.

(* Basic usage of parametricity, as an example *)
Remark ilist_param_cons_empty_id : forall (A:Set) (l:IList A), Parametric (@eq A) l ->
                                                         forall R c e, l _ cons empty R c e = l R c e.
Proof.
  intros * param *.
  specialize (param (IList A) R (fun l z => l R c e = z)). simpl in param.
  apply param.
  + intros x y <- l' z' h.
    simpl.
    congruence.
  + easy.
Qed.

Lemma ilist_param_retract : forall (A:Set) (l:IList A), Parametric (@eq A) l ->
                                 forall R c e, list_to_ilist (ilist_to_list l) R c e = l R c e.
Proof.
  intros * param *.
  unfold ilist_to_list,fold_right.
  specialize (param (list A) R (fun l z => list_to_ilist l R c e = z)). simpl in param.
  apply param.
  + intros x y <- l' z' h.
    simpl.
    congruence.
  + easy.
Qed.

(** Induction is harder than recursion because it is not true without
    parametricity or functional extensionality. Apart from that, it is
    basically the same definition as [ilist_rec0], but with [{l:IList
    A|P x}] instead of [(IList A*B)]. *)
Theorem ilist_param_ind (A:Set) (P:IList A->Prop)
           (s:P empty) (f:forall (x:A) (l:IList A), P l -> P (cons x l)) (l:IList A) :
  Parametric (@eq A) l -> (forall l', (forall R c e, l' R c e = l R c e) -> l'=l) -> P l.
Proof.
  intros param ext.
  set (ind:= fold_right
               (fun a lp => exist P (cons a (proj1_sig lp)) (f a (proj1_sig lp) (proj2_sig lp)))
               (exist P empty s)
               l).
  assert (proj1_sig ind = l) as h.
  { apply ext. intros R c e.
    unfold ind, fold_right.
    specialize (param {x|P x} R (fun lp z => proj1_sig lp R c e = z)). simpl in param.
    apply param.
    + intros x y <- lp z h.
      simpl.
      now rewrite <- h.
    + easy. }
  rewrite <- h.
  exact (proj2_sig ind).
Qed.


(** Assuming that every [IList A] is parametric together with
    functional extensionality allow to recover the convenience of
    usual lists with the exception of fixed points. *)

Require Import Coq.Logic.FunctionalExtensionality.

Axiom ilist_param : forall (A:Set) (r:A⇔A) (l:IList A), Parametric r l.


Corollary ilist_ind (A:Set) (P:IList A->Prop)
          (s:P empty) (f:forall (x:A) (l:IList A), P l -> P (cons x l)) (l:IList A) : P l.
Proof.
  intros **.
  apply ilist_param_ind; try solve[easy|apply ilist_param].
  intros **.
  extensionality R; extensionality c; extensionality e.
  easy.
Qed.


Lemma fold_right_empty (A B:Set) (f:A->B->B) (s:B) : fold_right f s empty = s.
Proof. reflexivity. Qed.

Lemma fold_right_cons (A B:Set) (f:A->B->B) (s:B) x l :
  fold_right f s (cons x l) = f x (fold_right f s l).
Proof. reflexivity. Qed.

Theorem ilist_rec0_empty (A B:Set) (s:B) (f:A->IList A -> B -> B) : ilist_rec0 s f empty = s.
Proof. reflexivity. Qed.

(** Contrary to the case true inductive type, this property needs to
be proven by induction. *)
Theorem ilist_rec0_cons (A B:Set) (s:B) (f:A->IList A -> B -> B) x l :
  ilist_rec0 s f (cons x l) = f x l (ilist_rec0 s f l).
Proof.
  unfold ilist_rec0.
  simpl.
  f_equal. clear.
  induction l as [ | x l h ] using ilist_ind.
  + easy.
  + simpl.
    congruence.
Qed.

Remark conj_injective (A:Set) (x₁ x₂:A) (l₁ l₂:IList A) :
  cons x₁ l₁ = cons x₂ l₂ -> x₁ = x₂ /\ l₁ = l₂.
Proof.
  intros h.
  split.
  + apply
      (f_equal (ilist_rec0 x₁(*this x₁ is not used, it just fills the gap*) (fun a _ _ => a)) h).
  + (* The list case is harder because it does not reduce up to conversion. *)
    set (tl := (ilist_rec0 l₁ (fun _ l _ => l))).
    assert (forall l x, tl (cons x l) = l) as def.
    { clear. subst tl. intros **.
      rewrite ilist_rec0_cons.
      reflexivity. }
    rewrite <- (def l₁ x₁) , <- (def l₂ x₂).
    congruence.
Qed.