Построить "меньше" из stdlib "меньше" - PullRequest
Новая
       16

Построить "меньше" из stdlib "меньше"

0 голосов
/ 21 марта 2019

Я хотел бы преобразовать стандартную библиотеку "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} ?

Последний знак вопроса - вопрос.

Редактировать : в соответствии с предложением Галле легче доказать вспомогательную лемму. Следующий код выполняет работу: 

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

1 Ответ

1 голос
/ 21 марта 2019

Легче доказать более общую лемму: 

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