The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Jason,

Yes, this extends. Below is a proof for le. This kind of proof is in generally possible for the cases you describe but it is kind of tedious. There may be a more efficient way.

Good luck!

Chris


Require Import Arith.
Require Import Omega.
Require Import Eqdep_dec.

Theorem nat_eq_proof_irrelevant:
   forall a b: nat,
   forall H1 H2: a = b,
   H1 = H2.
Proof.
apply eq_proofs_unicity.
intros a b.
destruct (eq_nat_dec a b) as [H1|H1]; tauto.
Qed.

Definition le_change_type:
   forall n m m': nat,
   n <= m ->
   n <= m' ->
   n <= m'.
intros n m m' H1 H2.
destruct (eq_nat_dec m m') as [H3|H3]; [|exact H2].
rewrite H3 in H1.
exact H1.
Defined.

Theorem le_change_type_lemma1:
   forall a b: nat,
   forall H1 H2: a <= b,
   le_change_type a b b H1 H2 = H1.
Proof.
intros a b H1 H2.
unfold le_change_type, eq_ind, eq_rect.
destruct (eq_nat_dec b b) as [H3|H3]; [|tauto].
rewrite (nat_eq_proof_irrelevant b b H3 (eq_refl _)).
tauto.
Qed.

Theorem le_change_type_lemma2:
   forall a b c: nat,
   forall H1: a <= b,
   forall H2: a <= c,
   b <> c ->
   le_change_type a b c H1 H2 = H2.
Proof.
intros a b c H1 H2 H3.
unfold le_change_type, eq_ind, eq_rect.
destruct (eq_nat_dec b c) as [H4|H4]; tauto.
Qed.

Theorem le_proof_irrelevant0:
   forall H1 H2: 0 <= 0,
   H1 = H2.
Proof.
intros H1 H2.
refine (
      match H1 as H1' in (le _ m) return H1' = le_change_type 0 0 m H2 H1'
      with
      | le_n => _
      | le_S m H3 => _
      end);
   [|rewrite le_change_type_lemma2; [tauto|discriminate]].
refine (
      match H2 as H2' in (le _ m) return le_n 0 = le_change_type 0 m 0 H2' (le_n 0)
      with
      | le_n => _
      | le_S m H3 => _
      end);
   [tauto|].
rewrite le_change_type_lemma2; [tauto|].
discriminate.
Qed.

Theorem le_proof_irrelevant:
   forall a b: nat,
   forall H1 H2: a <= b,
   H1 = H2.
Proof.
intros a b H1 H2.
induction b as [|b IH]; [inversion H2; subst a; apply le_proof_irrelevant0; fail|].
transitivity (le_change_type a (S b) (S b) H2 H1);
   [|rewrite le_change_type_lemma1;
     tauto].
refine (
      match H1 as H1' in (le _ m)
      return m = S b -> H1' = le_change_type a (S b) m H2 H1'
      with
      | le_n => _
      | le_S m H3 => _
      end (refl_equal _));
   intro H4.
(* 1/2 *)
refine (
      match H2 as H2' in (le _ m) return le_n a = le_change_type a m a H2' (le_n a)
      with
      | le_n => _
      | le_S m H3 => _
      end);
   [rewrite le_change_type_lemma1;
    tauto|].
rewrite le_change_type_lemma2; [tauto|].
omega.
(* 2/2 *)
injection H4.
intro H5.
subst m.
refine (
   match H2 as H2' in (le _ m)
   return m = S b -> le_S a b H3 = le_change_type a m (S b) H2' (le_S a b H3)
   with
   | le_n => _
   | le_S m H5 => _
   end (refl_equal _));
   [rewrite le_change_type_lemma2;
    [tauto|];
    omega|].
intro H6.
injection H6.
intro H7.
subst m.
rewrite le_change_type_lemma1.
f_equal.
apply IH.
Qed.

2013/4/7 Jason Gross <jasongross9 AT gmail.com>

I know that if [A : Type] has decidable equality (that is, [∀ x y : A, x = y ∨ x ≠ y]) than [eq_proofs_unicity] (in the standard library) tells me that [∀ (x y : A) (p1 p2 : x = y), p1 = p2].  Does this extend to other relations?

In particular, say I have an inductive relation [Inductive R : A → A → Prop], for each pair of distinct constructors [c1], [c2], and some elements [x y : A], I have a proof that if there are some arguments which can be passed to [c1] to construct [R x y], and also some arguments which can be passed to [c2] to construct [R x y], then one can derive absurdity.  For example, [le] fits this model, because it has two constructors, but they can't both apply at the same time.

If this is the case, is there a decision procedure for generating a proof of [∀ (x y : A) (p1 p2 : R x y), p1 = p2]?

Thanks,

Jason