Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Partial Points

Some tasks involve showing several lemmas. In order to obtain partial points you may use the sorry command to end proofs you can not solve entirely, while gaining points for lemmas you could prove.

Resources

Download Files

Definitions File

theory Defs imports Main
begin

fun sum where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n"

end

Template File

theory Submission 
imports Defs
begin

lemma goal1: "n \<le> m \<Longrightarrow> sum n \<le> sum m" sorry

lemma goal2: "n <= sum n" sorry

lemma goal3: "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" sorry

end

Check File

theory Check imports Submission begin 


lemma "n \<le> m \<Longrightarrow> sum n \<le> sum m" by(rule Submission.goal1)

lemma "n <= sum n" by(rule Submission.goal2)

lemma "\<And>M. (\<exists>N. \<forall>n\<ge>N. sum n \<ge> M)" by(rule Submission.goal3) 

end
Download Files

Definitions File

-- Lean version: 3.4.2
-- Mathlib version: 2019-07-31

namespace my

def sum : ℕ → ℕ
| 0 := 0
| (n + 1) := (n + 1) + sum n

end my

Template File

import .defs

lemma goal1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m :=
sorry

lemma goal2 : ∀ (n : ℕ), n ≤ my.sum n :=
sorry

lemma goal3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M :=
sorry

Check File

import .defs .submission

lemma lemma1 : ∀ (n m : ℕ), n ≤ m ↔ my.sum n ≤ my.sum m := goal1

lemma lemma2 : ∀ (n : ℕ), n ≤ my.sum n := goal2

lemma lemma3 : ∀ (M : ℕ), ∃ (N : ℕ), ∀ (n ≥ N), my.sum n ≥ M := goal3

Terms and Conditions