The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Thank you!  I will try this out.  I'm a bit reluctant about 
-impredicative-set, but erasability is already incompatible with certain 
things - certainly with indefinite description (which would unerase 
erasable terms).  Also, I anticipate that I need both this associativity 
up to conversion and real backtracking of tactics over evars (which I've 
been told is in the trunk, but haven't figured out how to use yet) to 
get the full benefit.

-- Jonathan

On 04/23/2014 07:37 AM, Arnaud Spiwack wrote:
> 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.