How to prove there exist a rational which is less than some rational in agda?

Question

I want to proof that there exist an rational which is less than some rational. for example..

v : ℚ
v = + 1 ÷ 2

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

What to write in second line??

And what is the meaning of x ∈ ℚ, will it give an element of ℚ or what.

And where is it defined over Set as i found this in Stream and there it defined over stream.

Answer 1

You just need to follow the definitions.

First of all, we take a look at what the Σ part of Σ[ x ∈ ℚ ] x ≤ v is. This data type is defined in the module Data.Product simply as Σ. The whole thing with ∈ is just a syntactic sugar, as can be seen from the following line:

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

So what we really need to construct is something of type Σ ℚ λ x → x ≤ v. Taking a look at the definition of Σ:

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

It's a pair, constructed using _,_. The first element is the number (a witness) and the second element is the proof that the first element satisfies the given proposition (≤). So, thm should look like this:

thm = ? , ?

We already know that the first element is a number (or, more precisely, something of type ℚ). So here we pick a suitable number - I picked + 1 ÷ 3, which should hopefully be less than + 1 ÷ 2.

thm = + 1 ÷ 3 , ?

This leaves us with the second question mark. There, we need something of type + 1 ÷ 3 ≤ v. Again, we'll take a look at the definition of ≤:

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

Okay, this makes it easy: the only constructor is *≤* so we can't possibly pick the wrong one:

thm = + 1 ÷ 3 , *≤* ?

The ? has now this type: + 2 ≤ + 3 (where ≤ comes from Data.Integer). Again, let's take a look at definition of ≤:

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

This gets slightly more interesting, as there are three possible constructors. However, taking a closer look, the only relevant one is +≤+, because the numbers on both sides are positive.

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

The only thing that is left is to write a term of type 2 ≤ 3 (for ≤ from Data.Nat). I'll leave that as an exercise for the reader.

---

If the choice of constructor is unambiguous, you can use Agda's Emacs mode to do most of the work for you - you just keep pressing C-c C-R (refine) and Agda just writes the proof term for you.

---

I don't like writing silly proof terms like that, the computer should be more than able to write a proof of x ≤ v for me - after all, ≤ is decidable.

Decidable is defined in the standard library:

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

So, a binary relation ~ is decidable if you can write a binary function (let's call the arguments x and y), that returns either a proof of x ~ y or a refutation of x ~ y (that is x ~ y → ⊥).

Luckily for us, the proof of ≤'s decidability is available in the standard library and can be found under the name ≤? - I just need to write fairly simple machinery to extract the proof from there (if it exists):

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 extracts the proof from Dec A; if the proof is not there (i.e. the argument was no ¬p for some ¬p), it just returns the empty tuple.

Now we can just let the computer figure out whether + 1 ÷ 3 ≤ v holds or not. If it does - great, we just extract the computed proof with fromDec and we're done; if it doesn't, fromDec returns the empty tuple and we get a type error.

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