CODEWITHSUNDEEP
coq
larsr
larsr

Reputation: 5811

Are all proofs of (true=true) the same?

Can I prove the following in Coq?

Lemma bool_uip (H1 : true = true): H1 = eq_refl true.

i.e. that all proofs of true = true are the same?

From it follows for example forall c (H1 H2: c = true), H1 = H2.

It would be nice to not have to add any axiom (like UIP). I found the following thread that suggests that it might be the case:

Proof in COQ that equality is reflexivity

Upvotes: 3

Views: 133

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33464

Here's a proof written as an explicit term.

Definition bool_uip (H1 : true = true): H1 = eq_refl true :=
  match H1 as H in _ = b
        return match b return (_ = b) -> Prop with
               | true => fun H => H = eq_refl true
               | false => fun _ => False
               end H with
  | eq_refl => eq_refl
  end.

The type of H1 : true = _ is inductive with one index (_). Pattern-matching proceeds by first generalizing that type to true = b (in clause), and instantiating the index b in every branch.

The main obstacle to overcome is that this generalization H1 : true = b makes the result type H1 = eq_refl true no longer well-typed (the two sides have different types). The solution is to pattern-match on b to realign the types (in one branch; the other branch is unused and we can in fact put anything instead of False).

We can use the same technique to prove uniqueness of identity proofs whenever the type of the "equalees" (here true of type bool) is decidable.

Upvotes: 5

Related Questions