Z_3：左身份证证明

如何解决Z_3：左身份证证明

我即将结束Z_3左id的证明。这是我到目前为止所拥有的

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Bool.Bool.
Require Import Coq.Logic.Eqdep_dec.

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),b <> O -> (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. apply UIP_dec. apply bool_dec.
Qed.

Proposition Z3_left_id' : forall x: Z_3,(Z3_op z3_0 x) = x.
Proof.
  intro. unfold Z3_op. destruct x as [n proof]. apply Z3_eq.

结果：

1 subgoal (ID 46)
  
  n : nat
  proof : (n <? 3) = true
  ============================
  (z3_0 + {| n := n; proof := proof |}) mod 3 = n

我发现以下定理可能有用：

Nat.ltb_spec0
     : forall x y : nat,reflect (x < y) (x <? y)

Nat.mod_small: forall a b : nat,a < b -> a mod b = a

是否有可能摆脱目标中的教授，将证据从bool转换为Prop，然后使用Nat.mod_small？

更新

Proposition Z3_left_id' : forall x: Z_3,(Z3_op z3_0 x) = x.
Proof.
  intro. unfold Z3_op. destruct x as [vx proof]. apply Z3_eq. unfold n,z3_0. rewrite plus_O_n. apply Nat.mod_small.

1 subgoal (ID 67)
  
  vx : nat
  proof : (vx <? 3) = true
  ============================
  vx < 3

解决方法

您需要强制执行。不幸， 通过命名证明n的绑定变量和从Z_3到nat n的投影，您将自己画在了一个角落。

以下是四种解决方案：

1 /我仅是出于记录目的提到这一点：您可以使用文件名作为模块限定符来讨论此文件中定义的常量n。

unfold user4035_oct_16.n.

user4035_oct_16是当前文件的名称，很难看。

2 /您可以调用一个计算所有内容的计算函数，但是模的计算在目标中留下难看的术语，因此您可以决定不计算该特定部分。

cbn -[Nat.modulo].

我喜欢这个，但它要求您花一些时间来学习如何使用cbn。

3 /您可以通过在目标中重命名变量来避免名称冲突。

rename n into m.
unfold n,Z3_0.

也不是很好。

4 /只需返回脚本并将destruct x as [n proof]替换为destruct x as [vx proof]，然后您可以输入：

unfold n,z3_0.

您将能够使用您建议的引理。

证明：

Proposition Z3_left_id : forall x: Z_3,(Z3_op z3_0 x) = x.
Proof.
  intro. unfold Z3_op. destruct x as [vx proof]. apply Z3_eq. unfold n,z3_0. rewrite plus_O_n. apply Nat.mod_small. apply Nat.ltb_lt in proof. assumption.
Qed.