The Coq mailing list

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

Well, indefinite description is incompatible with the impredicativity of Prop anyway. Definite description is compatible with Coq, but is indeed incompatible with erasure.

I have indeed implemented a set of proper backtracking primitive in trunk. The main one is called "+" (use as t1+t2) and properly backtracks on subsequent failure. Now, I don't know what exactly you are after, hence I can't give you more precise advice.

On 23 April 2014 17:42, Jonathan <jonikelee AT gmail.com> wrote:

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.