The Coq mailing list

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

Interestingly, the IList code appears to work without the -impredicative-set flag.  Are you sure it needs it?

Yes. You get almost no property without impredicativity (the first version I sent was a bit incorrect by the way, the version in the file is better). Basically, you don't have the recursor (only fold_right, which is trivial) nor induction.

I was primarily using eauto, so I will have to create my own try-different-things tactics that use +.  I have yet to try that, so I don't know what will be needed in addition to +.

I think "typeclasses eauto" behaves better than eauto (it is implemented quite the same way as +) and it's in v8.4. "typeclasses eauto with core" should be, I think, a better version of "solve[eauto]".

I am having difficulty proving the injectivity of cons within IList.v.  Mostly I suspect because I don't grasp the proper use of ilist_param and the Parametric function.  I can get injectivity of single - but don't need ilist_param for that.  It's the second (Ilist) arg of cons that I'm having difficulty with.  I don't have the intuition about what arguments to pass to Parametric.

You can kind of forget about parametricity once induction is established. Induction is trivially stronger.

Here goes the proof of injectivity. It's not trivial.

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.