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 

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
Download Files

Definitions File 

(in-package "ACL2")

; This file has no events, because all required definitions are built-in except
; in the case of rev and dotprod, which the user is supposed to define.

Template File 

(in-package "ACL2")

; The following is not necessary in this example, since the book has no
; events.
(include-book "Defs")

; Define rev to reverse its list argument:
; (defun rev (x) ...)

(defthm triple-rev-is-rev
  (equal (rev (rev (rev x)))
         (rev x)))

; Define dotprod so that it takes the dot product of two lists of equal length.
; For example:

(defthm dotprod-test
  (equal (dotprod '(1 2 3 4) '(1 10 100 1000))
         4321))

; Now prove this:

(defthm dotprod-rev-rev
  (implies (equal (len x) (len y))
           (equal (dotprod (rev x) (rev y))
                  (dotprod x y))))

Check File 

; The four lines just below are boilerplate, that is, the same for every
; problem.

(in-package "ACL2")
(include-book "Submission")
(set-enforce-redundancy t)
(include-book "Defs")

; The events below represent the theorems to be proved, and are copied from
; template.lisp.

(defthm triple-rev-is-rev
  (equal (rev (rev (rev x)))
         (rev x)))

(defthm dotprod-test
  (equal (dotprod '(1 2 3 4) '(1 10 100 1000))
         4321))

(defthm dotprod-rev-rev
  (implies (equal (len x) (len y))
           (equal (dotprod (rev x) (rev y))
                  (dotprod x y))))
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
Terms and Conditions