Hello World

Structure of Problem Statements

This problem should illustrate how to use the system.

Below you find three theories:

Defs

containing all the definitions that are needed fo this problem

Check

containing the goal of the problem. Most of the time this will be one ore more theorems.

Submission

being a template for you in order to solve the problem. Most of the time this will consist of the theorems that are to be shown with sorry as justification. Maybe some hints are given by providing a proof outline.

How to come up with a solution

In order to find a solution we recommend to make a new directory with three fresh theories Defs.thy, Submission.thy and Check.thy. Start Isabelle/JEdit and copy the content of the textboxes below into the appropriate files. If you are new to Isabelle, find a short installation guide at the end of this text

Now edit your Submission file and prove the lemma 'goal', e.g. "by simp". In order to check whether your solution is correct it suffices to let Isabelle proof-check the Check theory. Keep in mind that you must not alter the Defs and Checks files. If you do, the proof checking in our system may give a different result from your local copy

How to submit your solution

Once you solved the problem, and it is checked successfully on your machine, you can navigate to the appropriate submit form and upload the Submission file. Note that, the Defs and Check file need not be uploaded.

Now you can review the status of your Submission by using the "My Submissions" page. There you find all your submissions (to the current contest) and their status: here, "Pending" means, that your submission is in the grading pipeline, "Failed" means that some error occured (you can view details when hovering over the "Failed" textbox) and "Passed" means that you solved the problem - congratulations.

The Leaderboard shows your score in the current contest and how you perform relative to the other contestants.

How to setup the Proof Assistant Isabelle

Setting up Isabelle takes only a few steps: After downloading it from the webpage, you just need to unpack it and you are ready to go. The first startup may take a while because the Editor Isabelle/JEdit will build Isabelle/HOL's Library which you can then use.

Resources

• Isabelle2018
• Isabelle2019
• Coq
• Isabelle2020

theory Defs imports Main
begin

definition hello :: "bool => bool" where [simp]:
  "hello x == x"
definition [simp]: "world == True"          

end

theory Submission 
imports Defs 
begin 

lemma goal: "hello world" sorry    

end

theory Check imports Submission begin 

lemma  "hello world" by(rule Submission.goal)

end

theory Defs imports Main
begin

definition hello :: "bool => bool" where [simp]:
  "hello x == x"
definition [simp]: "world == True"          

end

theory Submission 
imports Defs 
begin 

lemma goal: "hello world" sorry    

end

theory Check imports Submission begin 

lemma  "hello world" by(rule Submission.goal)

end

Definition hello : Type -> Type :=
  fun x => x.

Inductive world :=
  W.

Require Import Defs.

Lemma goal : hello world.
Proof.
  (* your proof here *)
Admitted.

theory Defs imports Main
begin

definition hello :: "bool => bool" where [simp]:
  "hello x == x"
definition [simp]: "world == True"          

end

theory Submission 
imports Defs 
begin 

lemma goal: "hello world" sorry    

end

theory Check imports Submission begin 

lemma  "hello world" by(rule Submission.goal)

end