Coq 中 "less equal" 传递律的证明

Question

我是 coq 的新手。（我正在阅读软件基础中的 Poly 部分）

在基础部分，他们定义了ble_nat函数，即x <= y，然后我想证明关于这个的传递定律，比如：

Notation "x =< y" := (ble_nat x y) (at level 50, left associativity) : nat_scope.

Theorem ble_trans: forall (n m o:nat),
   n =< m = true -> m =< o = true -> n =< o = true.
Proof.
(* proof *)

但我无法使用 simpl、destruct、induction、rewrite 或 apply 策略来证明这一点。

我用谷歌搜索，发现已经证明了这个库，但我找不到代码。

我如何证明这一点？

Answer 1

要证明forall (n m : nat), n =< m =true -> exists o, m =< o = true -> n =< o = true，只要证明o := S m满足存在量词即可。

Theorem bleS : forall (n m: nat), n =< m = true -> n =< S m = true.
Proof.
  intros n.
  induction n.
  + intros m H. reflexivity.
  + intros m H. destruct m.
    - simpl in H. discriminate.
    - simpl. simpl in H. apply IHn. exact H.
Qed.

Theorem ble_trans_ex: forall (n m :nat),
   n =< m = true -> exists o, m =< o = true -> n =< o = true.
Proof.
  intros n m H1.
  apply ex_intro with (x := S m).
  intros H2. apply bleS. exact H1.
Qed.

Coq 中 "less equal" 传递律的证明

Proof of "less equal" transitive law in Coq

coq

coq-tactic