Search code examples
coqproof

Proof irrelevance for boolean equality

I'm trying to prove group axioms for Z_3 type:

Require Import Coq.Arith.PeanoNat.

Record Z_3 : Type := Z3
{
  n :> nat;
  proof : (Nat.ltb n 3) = true
}.

Proposition lt_0_3 : (0 <? 3) = true.
Proof.
  simpl. reflexivity.
Qed.

Definition z3_0 : Z_3 := (Z3 0 lt_0_3).

Proposition lt_1_3 : (1 <? 3) = true.
Proof.
  reflexivity.
Qed.

Definition z3_1 : Z_3 := (Z3 1 lt_1_3).

Proposition lt_2_3 : (2 <? 3) = true.
Proof.
  reflexivity.
Qed.

Definition z3_2 : Z_3 := (Z3 2 lt_2_3).

Proposition three_ne_0 : 3 <> 0.
Proof.
  discriminate.
Qed.

Lemma mod_upper_bound_bool : forall (a b : nat), (not (eq b O)) -> (Nat.ltb (a mod b) b) = true.
Proof.
  intros a b H. apply (Nat.mod_upper_bound a b) in H. case Nat.ltb_spec0.
  - reflexivity.
  - intros Hcontr. contradiction.
Qed.

Definition Z3_op (x y: Z_3) : Z_3 :=
  let a := (x + y) mod 3 in
  Z3 a (mod_upper_bound_bool _ 3 three_ne_0).

Lemma Z3_eq n m p q : n = m -> Z3 n p = Z3 m q.
Proof.
  intros H. revert p q. rewrite H. clear H. intros. apply f_equal.

We are almost done:

1 subgoal (ID 41)
  
  n, m : nat
  p, q : (m <? 3) = true
  ============================
  p = q

What theorem should I use to prove that p = q?

Update 1

Theorem bool_dec :
  (forall x y: bool, {x = y} + {x <> y}).
Proof.
  intros x y. destruct x.
  - destruct y.
    + left. reflexivity.
    + right. intro. discriminate H.
  - destruct y.
    + right. intro. discriminate H.
    + left. reflexivity.
Qed.

Lemma Z3_eq n m p q : n = m -> Z3 n p = Z3 m q.
Proof.
  intros H. revert p q. rewrite H. clear H. intros. apply f_equal. apply UIP_dec. apply bool_dec.
Qed.
Solution

  • You are probably interested in knowing that every two proofs of a decidable equality are equal. This is explained and proved here: https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

    You are interested in particular in the lemma UIP_dec: https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html#UIP_dec

    Theorem UIP_dec :
  forall (A:Type),
    (forall x y:A, {x = y} + {x <> y}) ->
    forall (x y:A) (p1 p2:x = y), p1 = p2.

    You will have then to prove that equalities of booleans are decidable (i.e. that you can write a function which says whether two given booleans are equal or not) which you should also be able to find in the standard library but which should be easily provable by hand as well.

    This is a different question but since you asked: bool_dec exists and even has that name! The easy way to find it is to use the command

    Search sumbool bool.

    It will turn up several lemmata, including pretty early:

    Bool.bool_dec: forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}

    Why did I search sumbool? sumbool is the type which is written above:

    { A } + { B } := sumbool A B

    You can find it using the very nice Locate command:

    Locate "{".

    will turn up

    "{ A } + { B }" := sumbool A B : type_scope (default interpretation)

    (and other notations involving "{").