证明与布尔相等无关

Question

我正在尝试证明 Z_3 类型的群公理：

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.

我们快完成了：

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

我应该用什么定理来证明p = q？

更新 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.

Answer 1

您可能有兴趣知道可判定相等性的每两个证明都是相等的。这在此处进行了解释和证明：https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

您对引理特别感兴趣 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.

然后你将必须证明布尔值的相等性是可判定的（即你可以编写一个函数来说明两个给定的布尔值是否相等）你也应该能够在标准库中找到但是也应该很容易用手证明。

这是一个不同的问题，但既然你问过：bool_dec 存在，甚至有那个名字！找到它的简单方法是使用命令

Search sumbool bool.

它将出现几个 lemmata，包括很早的：

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

我为什么要搜索 sumbool？ sumbool就是上面写的类型：

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

您可以使用非常好的 Locate 命令找到它：

Locate "{".

会出现

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

（以及其他涉及“{”的符号）。

证明与布尔相等无关

Proof irrelevance for boolean equality

coq

proof