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

### 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```

### 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