我如何证明 (eqb x y) 意味着 x = y

Question

我是 Coq 的新手，这个任务应该很简单：

forall x: nat, forall y: nat,
x == y = true -> x = y

这是更大任务的一小部分，但我坚持不懈。我知道逆问题更容易解决。并表明此类问题很少见。

在罗德里戈评论后更新

The proof proceeds by induction on x then case analysis on y

Lemma Obvious: forall x: nat, forall y: nat,
eq x y = true -> x = y.
Proof.
intros x y H.
  induction x as [| x'].
  (* Case x = 0 *)
    destruct y.
    (* Case y = 0 *)
      reflexivity. (* 0 = 0 *)
    (* Case y = S y' *)
      inversion H. (* 0 = S y', I can't explain what I should do in this situation *)
  (* Case x = S x' *)
    destruct y.
    (* Case y = 0 *)
      inversion H. (* S x' = 0 *)
    (* Case y = S y' *)
      rewrite <- IHx'. (* S x' = S y *) 
(* Now S x' = x' and this is looks falsy, but magical inversion didn't work as before. *)
(* rewrite <- IHx' in H... *)

Answer 1

为了解决数据类型构造函数之间这种不可能相等的问题，最好的策略是同余，它实现了一个称为同余闭包的决策过程。我已经证明了这个引理而没有输入任何 "case".

 Fixpoint beq_nat (x y : nat) : bool :=
   match x, y with
     | O , O => true
     | S n, S n' => beq_nat n n'
     | _ , _ => false                       
   end.

Lemma Obvious: forall x: nat, forall y: nat,
  beq_nat x y = true -> x = y.
Proof.
  intro x.
  induction x.
  intros y H.
  destruct y. reflexivity. simpl in *. congruence.
  intros y H. destruct y.
  simpl in *. congruence. f_equal ; auto.
Qed.

Answer 2

在 Coq 中，根据所谓的莱布尼兹等式（_ = _ 使用的那个），用不同的构造函数构造的两个项根据定义是不同的项。

对于nat值，S _和O是不同的构造函数，所以S n = O永远不可能为真。因为bool、true和false是不同的构造函数，所以true = false永远不可能为真。

当您使用 destruct、induction 等

对不可能的案例进行案例分析时，您会得到这些 "non-sensical" 假设

在证明上下文中获得这些假设时使用的策略是 congruence。它定位了一个"bad"假设，并证明它蕴含了目标，因为任何错误的假设都蕴含着任何命题。

congruence用起来很舒服，但你也可以创建证明项"by hand"。例如：

Goal  true <> false.
Proof.
    intro C.   (* now we have "C : true = false" in the context *)
    refine (match C with eq_refl => I end).
Qed.

我如何证明 (eqb x y) 意味着 x = y

How can I prove that (eqb x y) means x = y

coq