How to use Streicher_K_ Axiom

can someone show me a simple example how to use the Streicher_K_ axiom from Coq.Logic.EqdepFacts?

Maybe for showing the simple fact:

Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v.

I managed to prove it with Streicher_K_on_:

Variable A:Type.
Variable x:A. 
Axiom SK:Streicher_K_on_ A x (fun p:x=x => (eq_refl x) = p).

Lemma single_proof : forall (y:A)(u v:x = y), u = v.
intros.
destruct u.
apply (SK).
reflexivity.
Qed.

By trial and error I also found out how to prove it with Streicher_K_ , which is even more simple:

Axiom SK:Streicher_K_ A.

But the problem is that I have no idea why this works. I don't understand the underlying type checking.

Solution

K and its many equivalent statements

The statement of axiom K is a bit difficult to grasp at first sight. It's even harder to understand in the standard library, because of the additional parameters. Fortunately, it is equivalent to the following alternative, which generalizes the one you were trying to prove, and is often what we need in practice:

UIP : forall (T : Type) (x y : T) (p q : x = y), p = q

("UIP" stands for "unicity of identity proofs.")

The Coq standard library has a EqdepTheory module that shows this equivalence of these two statements and a few other, similar ones. It allows us to freely use any of these statements while one assuming one of them, eq_rect_eq:

Require Import Coq.Logic.EqdepFacts.

Module Ax : EqdepElimination.

Axiom eq_rect_eq :
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
      x = eq_rect p Q x p h.

End Ax.

Module Export UIPM := EqdepTheory Ax.

After this snippet, we can run, for instance,

Check UIP.

But how do we prove stuff with K?

You also seemed puzzled about how we could use K to prove UIP. The answer lies in the following statement:

Definition J (A : Type) (x : A) (P : forall y, x = y -> Prop) :
  P x eq_refl -> forall y (p : x = y), P y p :=
  fun H y p =>
    match p with
    | eq_refl => H
    end.

At first sight, K and J are fairly similar. Let's compare their types:

J : forall (A : Type) (x : A) (P : forall y : A, x = y -> Prop), 
    P x eq_refl -> forall (y : A) (p : x = y), P y p

K : forall (A : Type) (x : A) (P :               x = x -> Prop),
    P   eq_refl -> forall         (p : x = x), P   p

(I wrote K instead of Streicher_K just for legibility.) One difference is that J is parameterized by a predicate P of equalities x = y that is generic with respect to the right-hand side y. K also has a predicate P, but it only considers equalities x = x.

Another difference is that, while J can be proved in Coq's theory, as done above, K can only be proved by adding extra axioms into the theory. This might seem surprising, given that the predicate P used in K is more specific than the one used in J, but is a consequence of how the match statement is typed in Coq.

By combining K and J, we can arrive at a proof of UIP. Let's first prove a specialized version of it, that only works for reflexive equalities:

Definition UIP_refl (A : Type) (x : A) (p : x = x) : eq_refl = p :=
  Streicher_K A x (fun q => eq_refl = q) eq_refl p.

Then, J allows us to generalize this to arbitrary equalities:

Definition UIP (A : Type) (x y : A) (p q : x = y) : p = q :=
  J A x (fun y p => forall q : x = y, p = q) (UIP_refl A x) y p q.

Notice that the definition of J uses pattern matching. Under the hood, Coq was also using pattern matching in your proof, when you invoked destruct (SK)..