Break the System

Definitions File

theory Defs
  imports Main
begin  
end

Template File

theory Submission
  imports Defs
begin

lemma soundnessbug: "False" sorry

end

Check File

theory Check
imports Submission
begin

                     
lemma "False"
by (rule Submission.soundnessbug)
   

end

Definitions File

(* nothing here *)

Template File

Theorem soundnessbug : False.
Proof.
  (* todo? *)
Admitted.

Definitions File

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

Template File

theorem soundness_bug : false := sorry

Check File

import .submission

theorem you_broke_it : false := soundness_bug

Definitions File

(in-package "ACL2")

Template File

(in-package "ACL2")

(include-book "Defs")

(defthmd cannot-prove (equal (car a) nil))

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 theorem to be proved, and are copied from
; template.lisp.


(defthmd cannot-prove (equal (car a) nil))

Definitions File

theory Defs
  imports Main
begin  
end

Template File

theory Submission
  imports Defs
begin

lemma soundnessbug: "False" sorry

end

Check File

theory Check
imports Submission
begin

                     
lemma "False"
by (rule Submission.soundnessbug)
   

end