Welcome to the 15-150 Interactive Proof System!

This will be the platform where you will complete the proof portions of your homework assignments and labs for 15-150.

This system is still under active development by Abubakr Mohamed. If you find any problem that you wish to report, please submit an issue on github. We are awaiting your feedback.

Note: This system has been tested on the following browsers: Chrome (v110.0.5481), Opera (v96.0.4693) and Edge (v110.0.1587)

First Steps

Upon uploading your SML code to the system, you will be redirected to a page with three color-coded editor panes.

The first pane (pink) contains the translations of your SML datatype declarations (eg. trees). The second pane (blue) contains the translation of your function definitions. The last pane, which you will work in, contains the assignment questions to be proved as theorems. Note that the first two panes are read-only.

How to Write a Proof

The proof for every theorem should be encapsulated by "Proof." and "Qed." commands as follows:

Theorem example1: forall n:nat, n = n. Proof. trivial. Qed.

In between these two commands, you should use a series of commands, called tactics, that allow you to manipulate the goal (statement to be proved) until it can be proven trivially.

Use Alt+↓/↑ or option+↓/↑ to step through the proof, executing tactics individually and observe the proof state on the right panel. You can also use the green arrow buttons on the top right instead.

The proof state displays information about the current statement that needs to be proven (goal) as well as the current proof context (variables, types, hypotheses, etc). Once a proof has been completed, the right panel should reflect that there are "No more goals" to be proven.

Below is a table of some of the most common tactics that you might need to use in 15-150 along with a brief explanation of their meaning:

Tactic	Definition
introduce	Introduce quantified variables into context.
induction <var>	Perform structural induction on the variable indicated by <var>
simpl	Simplify / evaluate mathematical expressions
simp <fun>	Apply / evaluate the function <fun>
by_math	Use to prove trivial arithmetic statements (eg. x + x = 2x)
trivial	Use to finish goals of the form (x = x)
rewrite <S1> in <S2>	Use a statement/hypothesis <S1> rewrite <S2>
apply <S>	Use a statement/hypothesis <S> to finish a (sub)goal
contradict	Use to finish a (sub)goal when one of the assumptions/hypotheses is a contradiction (eg. false = true)
cases <expr>	Break the proof into cases based on the possible values of <expr>

Example Proof 1: negb ∘ negb = id

Consider the following SML definition of boolean negation.

The following is a simple proof that the negation of a boolean is its own inverse.

Use Alt+↓/↑ or option+↓/↑ to step through the proof, and observe the proof state on the right panel. You can also use the green arrow buttons on the top right instead.

From Equations Require Import Equations. Equations negb (x1: bool): bool := negb b := match b with | true => false | false => true end. Theorem inverse: forall b : bool, negb (negb (b)) = b. Proof. cases b. - simp negb. trivial. - simp negb. trivial. Qed.

Explanation:

The proof proceeds by taking cases on the value of b using the cases tactic. Each subgoal is proved by first simplifying the negb function using the simp tactic. Then we have goals of the form True = True or False = False which we solve by using the trivial tactic.

Example Proof 2: rev ∘ rev = id

Consider the following SML definition of a list reversal function

Suppose that our task is to prove that rev is its own inverse. (i.e reversing a list twice returns the original list). From Coq Require Import List. Import ListNotations. From listSml Require Import listSml. From notationsSml Require Import notationsSml. From Coq Require Import ZArith. Equations rev (x1: @list Z): @list Z := rev [] := []; rev (x :: l) := ((rev l) @ [x]).

First, we are going to need the following lemma to complete the proof.

Lemma rev_lemma : forall (a : Z), forall (l : list Z), rev (l @ [a]) = a :: rev(l). Admitted.

Now we prove the desired theorem by induction on the list l.

Theorem rev_rev : forall (l : list Z), rev (rev l) = l. Proof. induction l. - simp rev. trivial. - simp rev. rewrite rev_lemma. rewrite IHl. trivial. Qed.

Explanation:

The proof proceeds by induction on the list l using the induction tactic.

The base case considers when the list is empty. Here we simplifying the function rev using the simp tactic. We are then left with a goal of the form [] = [] which we can solve by the trivial tactic.

For inductive case, we consider the case when the list is of the form a :: l. We also get the inductive hypothesis in our context as IHl. After simplifying rev, we are able to make use of the rev_lemma which we apply using the rewrite tactic. We can then use our inductive hypothesis with the rewrite tactic.

Note that the inductive hypothesis is always of the form IH + <var_name>.

---

Quick start

Actions

Button	Key binding	Action
	F8	Toggles the goal panel.
	Alt+↓/↑ or Alt+N/P	Move through the proof.
	Alt+Enter or Ctrl+Enter (⌘ on Mac)	Run (or go back) to the current point.
	Ctrl+	Hover executed statements to peek at the proof state after each step.

Special symbols can be entered in the editor by using the following keywords.

Syntax

Symbol	Term
∀	forall
∃	exists
∧	/\\
∨	\\/
λ	fun
ℙ	Prop
ℕ	nat
→	->
⇒	=>
←	<-
ℝ	Real