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