The Coq mailing list

[Andrew Hirsch <akhirsch AT gwmail.gwu.edu>]

Hey,

I have a couple of lemmas about the standard Coq library I would like
to be able to use in a project. However, I can't find a proof of
either, and it seems that there isn't one in the standard libraries.
Is it possible to prove either, or is it possible that either is
false?

The first is about Sigma types. I want to prove that:
forall (A : Set) (Q : A -> Prop) (b : {a : A | Q a}), b = exist Q
(proj1_sig b) (proj2_sig b).

That is, that I can rebuild an element of a sigma type from it's projections.

The other is not about the standard library directly. I have this definition:
Inductive var : Set :=
  Var : nat -> var.

With this decision procedure:
Definition var_eq : forall (a b  : var), {a = b} + {a <> b}.
intros.
decide equality. apply Peano_dec.eq_nat_dec.
Defined.

I want to then prove:
forall (x : var) (A : Set) (a b : A), (if var_dec x x then a else b) = a.

That is, that the same thing should always be equal to itself, and so
we can evaluate that in an if_then_else statement.

Thanks so much for your help!

-Andrew Hirsch