The Coq mailing list

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

Actually… in the case of list I found a solution. It uses the -impredicative-set flag of Coq: the impredicative encoding of lists have associativity of append/empty up to conversion (this requires eta, but it's already available in Coq v8.4).

Here is the relevant definitions. Since this type (kind of) isomorphic to lists you should be able to reason on sorted lists quite nicely.



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

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

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

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

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


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.

On 23 April 2014 09:18, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

On 23 April 2014 11:17, AUGER Cédric <sedrikov AT gmail.com> wrote:

If you can decide of some property, then you have a form of irrelevance.
Any function to the 'bool' type can be converted in a function to
'Prop' by composition with 'conv (fun x => if x then True else False) :
bool -> Prop'. And for any boolean 'b', a term of type 'conv b' is
"irrelevant" (there is only a single habitant to that type).

That is mainly the main reason why we have UIP on decidable equalities.

This is, however, not sufficient for the trick I mentioned which needs conversion-level irrelevance. Which, indeed, isn't implemented in the current Coq. So, unfortunately, there is no conversion-level associativity yet in Coq. But we can hope the future makes it available.