Let \(x, y ∈ ℝ\). Prove that \[ (∀ ε > 0, y ≤ x + ε) → y ≤ x \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {x y : ℝ} example : (∀ ε > 0, y ≤ x + ε) → y ≤ x := by sorry
In Lean4, one can define that \(x\) is an upper bound of \(A\) by
def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x
and \(x\) is supremum of \(A\) by
def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y
Prove that if \(x\) is the supremum of \(A\), then \[ (∀ y)[y < x → (∃ a ∈ A)[y < a]] \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {A : Set ℝ} variable {x : ℝ} def is_upper_bound (A : Set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x def is_supremum (A : Set ℝ) (x : ℝ) := is_upper_bound A x ∧ ∀ y, is_upper_bound A y → x ≤ y example (hx : is_supremum A x) : ∀ y, y < x → ∃ a ∈ A, y < a := by sorry
In Lean4, the Fibonacci function can be defined as
def fibonacci : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fibonacci n + fibonacci (n+1)
Another more efficient definition is
def fib (n : Nat) : Nat := (loop n).1 where loop : Nat → Nat × Nat | 0 => (0, 1) | n + 1 => let p := loop n (p.2, p.1 + p.2)
Prove that both definitions are equivalent; that is,
fibonacci = fib
To do this, complete the following Lean4 theory:
open Nat set_option pp.fieldNotation false def fibonacci : Nat → Nat | 0 => 0 | 1 => 1 | n + 2 => fibonacci n + fibonacci (n+1) def fib (n : Nat) : Nat := (loop n).1 where loop : Nat → Nat × Nat | 0 => (0, 1) | n + 1 => let p := loop n (p.2, p.1 + p.2) example : fibonacci = fib := by sorry
The tree corresponding to
3 / \ 2 4 / \ 1 5
can be represented by the term
Node 3 (Node 2 (Leaf 1) (Leaf 5)) (Leaf 4)
using the datatype defined by
inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α
The mirror image of the previous tree is
3 / \ 4 2 / \ 5 1
and the list obtained by flattening it (traversing it in infix order) is
[4, 3, 5, 2, 1]
The definition of the function that calculates the mirror image is
def mirror : Tree' α → Tree' α | Leaf x => Leaf x | Node x l r => Node x (mirror r) (mirror l)
and the one that flattens the tree is
def flatten : Tree' α → List α | Leaf x => [x] | Node x l r => (flatten l) ++ [x] ++ (flatten r)
Prove that
flatten (mirror a) = reverse (flatten a)
To do this, complete the following Lean4 theory:
import Mathlib.Tactic open List variable {α : Type} set_option pp.fieldNotation false inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α namespace Tree' variable (a l r : Tree' α) variable (x : α) def mirror : Tree' α → Tree' α | Leaf x => Leaf x | Node x l r => Node x (mirror r) (mirror l) def flatten : Tree' α → List α | Leaf x => [x] | Node x l r => (flatten l) ++ [x] ++ (flatten r) example : flatten (mirror a) = reverse (flatten a) := by sorry
The tree corresponding to
3 / \ 2 4 / \ 1 5
can be represented by the term
Node 3 (Node 2 (Leaf 1) (Leaf 5)) (Leaf 4)
using the datatype defined by
inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α
The mirror image of the previous tree is
3 / \ 4 2 / \ 5 1
whose term is
Node 3 (Leaf 4) (Node 2 (Leaf 5) (Leaf 1))
The definition of the function that calculates the mirror image is
def mirror : Tree' α → Tree' α | (Leaf x) => Leaf x | (Node x l r) => Node x (mirror r) (mirror l)
Prove that the mirror function is involutive; that is,
mirror (mirror a) = a
To do this, complete the following Lean4 theory:
import Mathlib.Tactic variable {α : Type} set_option pp.fieldNotation false inductive Tree' (α : Type) : Type | Leaf : α → Tree' α | Node : α → Tree' α → Tree' α → Tree' α namespace Tree' variable (a l r : Tree' α) variable (x : α) def mirror : Tree' α → Tree' α | (Leaf x) => Leaf x | (Node x l r) => Node x (mirror r) (mirror l) example : mirror (mirror a) = a := by sorry end Tree'
In Lean4, the function
reverse : List α → List α
is defined such that (reverse xs) is the list obtained by reversing the order of elements in xs, such that the first element becomes the last, the second element becomes the second to last, and so on, resulting in a new list with the same elements but in the opposite sequence. For example,
reverse [3,2,5,1] = [1,5,2,3]
Its definition is
def reverseAux : List α → List α → List α | [], ys => ys | x::xs, ys => reverseAux xs (x::ys) def reverse (xs : List α) : List α := reverseAux xs []
The following lemmas characterize its behavior:
reverseAux_nil : reverseAux [] ys = ys reverseAux_cons : reverseAux (x::xs) ys = reverseAux xs (x::ys)
An alternative definition is
def reverse2 : List α → List α | [] => [] | (x :: xs) => reverse2 xs ++ [x]
Prove that the two definitions are equivalent; that is,
reverse xs = reverse2 xs
To do this, complete the following Lean4 theory:
import Mathlib.Data.List.Basic open List variable {α : Type} variable (xs : List α) example : reverse xs = reverse2 xs := by sorry
In Lean4, the functions
take : Nat → List α → Nat drop : Nat → List α → Nat (++) : List α → List α → List α
are defined such that
(take n xs) is the list consisting of the first n elements of xs. For example,
take 2 [3,5,1,9,7] = [3,5]
(drop n xs) is the list containing all elements of xs except the first n elements. For example,
drop 2 [3,5,1,9,7] = [1,9,7]
(xs ++ ys) is the list obtained by concatenating xs and ys. For example,
[3,5] ++ [1,9,7] = [3,5,1,9,7]
These functions are characterized by the following lemmas:
take_zero : take 0 xs = [] take_nil : take n [] = [] take_cons : take (succ n) (x :: xs) = x :: take n xs drop_zero : drop 0 xs = xs drop_nil : drop n [] = [] drop_succ_cons : drop (n + 1) (x :: xs) = drop n xs nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)
Prove that
take n xs ++ drop n xs = xs
To do this, complete the following Lean4 theory:
import Mathlib.Data.List.Basic import Mathlib.Tactic open List Nat variable {α : Type} variable (n : ℕ) variable (x : α) variable (xs : List α) example : take n xs ++ drop n xs = xs := by sorry
In Lean, the functions
length : List α → Nat (++) : List α → List α → List α
are defined such that
(length xs) is the length of xs. For example,
length [2,3,5,3] = 4
(xs ++ ys) is the list obtained by concatenating xs and ys. For example.
[1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]
These functions are characterized by the following lemmas:
length_nil : length [] = 0 length_cons : length (x :: xs) = length xs + 1 nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)
To prove that
length (xs ++ ys) = length xs + length ys
To that end, complete the following Lean4 theory
import Mathlib.Tactic open List variable {α : Type} variable (xs ys : List α) example : length (xs ++ ys) = length xs + length ys := by sorry
En Lean4 la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas
nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)
Demostrar que la concatenación es asociativa; es decir,
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.List.Basic open List variable {α : Type} variable (xs ys zs : List α) -- 1ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as HI . calc [] ++ (ys ++ zs) = ys ++ zs := nil_append (ys ++ zs) _ = ([] ++ ys) ++ zs := congrArg (. ++ zs) (nil_append ys).symm . calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) := cons_append a as (ys ++ zs) _ = a :: ((as ++ ys) ++ zs) := congrArg (a :: .) HI _ = (a :: (as ++ ys)) ++ zs := (cons_append a (as ++ ys) zs).symm -- 2ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as HI . calc [] ++ (ys ++ zs) = ys ++ zs := by rw [nil_append] _ = ([] ++ ys) ++ zs := by rw [nil_append] . calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) := by rw [cons_append] _ = a :: ((as ++ ys) ++ zs) := by rw [HI] _ = (a :: (as ++ ys)) ++ zs := by rw [cons_append] _ = ((a :: as) ++ ys) ++ zs := by rw [← cons_append] -- 3ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as HI . calc [] ++ (ys ++ zs) = ys ++ zs := by exact rfl _ = ([] ++ ys) ++ zs := by exact rfl . calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) := rfl _ = a :: ((as ++ ys) ++ zs) := by rw [HI] _ = (a :: (as ++ ys)) ++ zs := rfl _ = ((a :: as) ++ ys) ++ zs := rfl -- 4ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as HI . calc [] ++ (ys ++ zs) = ys ++ zs := by simp _ = ([] ++ ys) ++ zs := by simp . calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) := by simp _ = a :: ((as ++ ys) ++ zs) := congrArg (a :: .) HI _ = (a :: (as ++ ys)) ++ zs := by simp _ = ((a :: as) ++ ys) ++ zs := by simp -- 5ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as . simp . exact (append_assoc (a :: as) ys zs).symm -- 6ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction' xs with a as HI . -- ⊢ [] ++ (ys ++ zs) = ([] ++ ys) ++ zs rw [nil_append] -- ⊢ ys ++ zs = ([] ++ ys) ++ zs rw [nil_append] . -- a : α -- as : List α -- HI : as ++ (ys ++ zs) = as ++ ys ++ zs -- ⊢ (a :: as) ++ (ys ++ zs) = ((a :: as) ++ ys) ++ zs rw [cons_append] -- ⊢ a :: (as ++ (ys ++ zs)) = ((a :: as) ++ ys) ++ zs rw [HI] -- ⊢ a :: ((as ++ ys) ++ zs) = ((a :: as) ++ ys) ++ zs rw [cons_append] -- ⊢ a :: ((as ++ ys) ++ zs) = (a :: (as ++ ys)) ++ zs rw [cons_append] -- 7ª demostración -- =============== lemma conc_asoc_1 (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by induction xs with | nil => calc [] ++ (ys ++ zs) = ys ++ zs := by rw [nil_append] _ = ([] ++ ys) ++ zs := by rw [nil_append] | cons a as HI => calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) := by rw [cons_append] _ = a :: ((as ++ ys) ++ zs) := by rw [HI] _ = (a :: (as ++ ys)) ++ zs := by rw [cons_append] _ = ((a :: as) ++ ys) ++ zs := congrArg (. ++ zs) (cons_append a as ys) -- 8ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := (append_assoc xs ys zs).symm -- 9ª demostración -- =============== example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by simp -- Lemas usados -- ============ -- variable (x : α) -- #check (append_assoc xs ys zs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs)) -- #check (cons_append x xs ys : (x :: xs) ++ ys = x :: (xs ++ ys)) -- #check (cons_inj x : x :: xs = x :: ys ↔ xs = ys) -- #check (nil_append xs : [] ++ xs = xs)
En Lean4 están definidas las funciones length y replicate tales que
(length xs) es la longitud de la lista xs. Por ejemplo,
length [1,2,5,2] = 4
(replicate n x) es la lista que tiene el elemento x n veces. Por ejemplo,
replicate 3 7 = [7, 7, 7]
Demostrar que
length (replicate n x) = n
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.List.Basic open Nat open List variable {α : Type} variable (x : α) variable (n : ℕ) example : length (replicate n x) = n := by sorry