The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Sep 12, 2014 at 2:53 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> Here's is all that I do, really:
>
> Inductive Erasable(A : Type) : Prop :=
>   erasable: A -> Erasable A.
>
> Arguments erasable [A] _.
>
> Axiom Erasable_inj : forall {A : Type}{a b : A}, erasable a=erasable b ->
> a=b.
>
>
> I then use "Erasable nat" (##nat via notation) instead of nat, and "erasable
> 42" (#42 via notation) instead of 42.
>
> I am not sure I understand the difference you are suggesting.  For instance,
> are you saying that if I want an erasable constant replacement for 42, I
> instead use a function from a singleton type based on 42 to Prop?  And then
> achieve injectivity using some variety of extensionality?  Hmmm.....

Here's a simple example of what I was thinking of (though without any
of the hard work which would go into defining something like
vector_map2):

Inductive return_O : nat -> Prop :=
| return_O_intro : return_O O.

Inductive liftM_S (n : nat -> Prop) : nat -> Prop :=
| liftM_S_intro : forall m:nat, n m -> (liftM_S n) (S m).

Inductive vector (A:Type) : (nat -> Prop) -> Type :=
| vector_nil : vector A return_O
| vector_cons : A -> forall {n : nat -> Prop}, vector A n ->
                vector A (liftM_S n).

And here are the general monad operations which are respectful of
being singletons, respectful of extensional equality, etc.:
Inductive singleton_return {A:Type} (x:A) : A -> Prop :=
| singleton_return_intro : singleton_return x x.

Inductive singleton_bind {A:Type} (x:A->Prop)
  {B:Type} (f:A->(B->Prop)) : B -> Prop :=
| singleton_bind_intro : forall (x0:A) (y:B), x x0 -> f x0 y ->
  singleton_bind x f y.

Inductive singleton_algebra_Prop (P : Prop -> Prop) : Prop :=
| singleton_algebra_Prop_intro : forall Q:Prop, P Q -> Q ->
  singleton_algebra_Prop P.
-- 
Daniel Schepler