Как доказать, что существует рациональное, которое в агде меньше рационального?

Question

Я хочу доказать, что существует рациональное, которое меньше рационального. например..

v : ℚ
v = + 1 ÷ 2

thm : (Σ[ x ∈ ℚ ] (x Data.Rational.≤ v))
thm = ?

Что писать во второй строке??

И в чем смысл x ∈ ℚ, даст ли он элемент из ℚ или что.

И где он определен над Set, как я нашел это в потоке, и там он определен над потоком.

Answer 1

Вам просто нужно следовать определениям.

Прежде всего, мы посмотрим на то, что Σ часть Σ[ x ∈ ℚ ] x ≤ v является. Этот тип данных определен в модуле Data.Product просто как Σ, Все это с ∈ это просто синтаксический сахар, как видно из следующей строки:

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

Так что нам действительно нужно построить что-то типа Σ ℚ λ x → x ≤ v, Взглянув на определение Σ:

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

Это пара, построенная с использованием _,_, Первый элемент - это число (свидетель), а второй элемент - это доказательство того, что первый элемент удовлетворяет данному предложению (≤). Так, thm должен выглядеть так:

thm = ? , ?

Мы уже знаем, что первым элементом является число (или, точнее, что-то типа ℚ). Итак, здесь мы выбираем подходящий номер - я выбрал + 1 ÷ 3который должен быть меньше + 1 ÷ 2,

thm = + 1 ÷ 3 , ?

Это оставляет нас со вторым знаком вопроса. Там нам нужно что-то типа + 1 ÷ 3 ≤ v, Опять же, мы посмотрим на определение ≤:

data _≤_ : ℚ → ℚ → Set where
  *≤* : ∀ {p q} →
        ℚ.numerator p ℤ.* ℚ.denominator q ℤ.≤
        ℚ.numerator q ℤ.* ℚ.denominator p →
        p ≤ q

Ладно, это легко: единственный конструктор *≤* поэтому мы не можем выбрать неправильный:

thm = + 1 ÷ 3 , *≤* ?

? имеет теперь этот тип: + 2 ≤ + 3 (где ≤ происходит от Data.Integer). Опять же, давайте посмотрим на определение ≤:

data _≤_ : ℤ → ℤ → Set where
  -≤+ : ∀ {m n} → -[1+ m ] ≤ + n
  -≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ]
  +≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n

Это становится немного интереснее, так как есть три возможных конструктора. Однако, если присмотреться, то единственный +≤+, потому что числа с обеих сторон положительные.

thm = + 1 ÷ 3 , *≤* (+≤+ ?)

Осталось только написать термин типа 2 ≤ 3 (за ≤ от Data.Nat). Я оставлю это как упражнение для читателя.

---

Если выбор конструктора однозначен, вы можете использовать режим Emacs от Agda, чтобы сделать большую часть работы за вас - вы просто продолжаете нажимать C-c C-R (уточните), и Агда просто пишет проверочный термин для вас.

---

Мне не нравится писать такие глупые проверочные термины, компьютер должен быть более чем способен написать доказательство x ≤ v для меня - в конце концов, ≤ решаемо.

Decidable определяется в стандартной библиотеке:

Decidable : ∀ {a b ℓ} {A : Set a} {B : Set b} → REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

Итак, бинарное отношение ~ разрешимо, если вы можете написать бинарную функцию (давайте вызовем аргументы x а также y), который возвращает либо доказательство x ~ y или опровержение x ~ y (то есть x ~ y → ⊥).

К счастью для нас, доказательство ≤Разрешимость доступна в стандартной библиотеке и может быть найдена под именем ≤? - Мне просто нужно написать довольно простой механизм, чтобы извлечь доказательства оттуда (если оно существует):

open import Relation.Nullary

FromDec : ∀ {A : Set} → Dec A → Set
FromDec {A = A} (yes p) = A
FromDec         (no ¬p) = ⊤

fromDec : ∀ {A : Set} (d : Dec A) → FromDec d
fromDec (yes p) = p
fromDec (no ¬p) = _

fromDec извлекает доказательства из Dec A; если доказательства нет (то есть аргумент был no ¬p для некоторых ¬p), он просто возвращает пустой кортеж.

Теперь мы можем просто позволить компьютеру выяснить, + 1 ÷ 3 ≤ v держит или нет. Если это так - отлично, мы просто извлекаем вычисленное доказательство с fromDec и мы закончили; если нет, fromDec возвращает пустой кортеж, и мы получаем ошибку типа.

thm : Σ[ x ∈ ℚ ] x ≤ v
thm = , fromDec (+ 1 ÷ 3 ≤? v)