来自 stdlib "less" 的内置 "less"

Question

我想将标准库 "less" 转换为内置（布尔）库。

这是我目前的情况：

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat using (_<_)
open import Relation.Nullary using (Dec;yes;no)
open import Data.Nat using (ℕ;zero;suc;_<?_;z≤n;s≤s)

convert : ∀{a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
convert {_} {zero} ()
convert {zero} {suc _} _ = refl
convert {suc a} {suc b} {Data.Nat.s≤s p} eq = 
  convert {a} {b} {p} ?

最后一个问号是问题。

编辑：正如gallais所建议的，使用辅助引理更容易证明。以下代码可以完成这项工作：

lemma : ∀ {a b} → a Data.Nat.< b → (a < b) ≡ true
lemma {a} {zero} ()
lemma {zero} {suc b} eq = refl
lemma {suc a} {suc b} (s≤s eq) = lemma eq

convert : ∀{a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
convert {_} {zero} ()
convert {zero} {suc _} _ = refl
convert {suc a} {suc b} {Data.Nat.s≤s p} eq = lemma p

Answer 1

证明更一般的引理更容易：

lemma : ∀ {a b} → a Data.Nat.< b → (a < b) ≡ true

然后总结：

lemma : ∀ {a b p} → (a <? b) ≡ yes p → (a < b) ≡ true
lemma {p = p} eq = convert p

来自 stdlib "less" 的内置 "less"

Builtin "less" from stdlib "less"

agda