Sequent Help

Workflow

Check

Parses and checks the current source. Proof boxes and warnings appear on the right.

Format

Parses the source and rewrites it with consistent spacing. Comments are not preserved.

Share

Creates a link containing the current source. Use the link in the notice that appears.

Report

Prepares a bug report via email and adds the current program to the email body.

Theme

The theme selector provides various themes to change the look of the user interface.

Drag the divider between the editor and output panes to resize them. Drag the divider between proof output and diagnostics to change their relative height.

Proof Shape

A proof has a name, a sequent, and a bracketed block of proof lines. A line has a label, a formula or sequent, and a rule justification.

proof_name : premise_1, premise_2 |- conclusion [
    line_label : formula   by rule references;
]

Labels may be ordinary names such as l1, or box labels such as @box. Rules refer to earlier labels.

A source file may contain many proofs and rules. Declarations can use earlier declarations, so put reusable rules and helper proofs above the proofs that call them.

Formula Syntax

Building Proofs

Start by writing the sequent you want to prove. Then add premise lines, open boxes for temporary assumptions, and close boxes with the rule that needs the whole subproof.

Start from the target sequent

want_conjunction : p, q |- p /\ q [
    l1 : p        by premise;
    l2 : q        by premise;
    l3 : p /\ q   by con_i l1 l2;
]

Each premise line must match one of the formulas to the left of |-. Later lines cite earlier labels. Here con_i needs a proof of the left conjunct and a proof of the right conjunct.

Use boxes for temporary assumptions

make_implication : |- p => p [
    @self [
        l1 : p    by assumption;
        l2 : p    by copy l1;
    ]
    l3 : p => p   by imp_i @self;
]

A box label names the whole subproof. The @self box proves the sequent p |- p, so imp_i can turn that box into p => p. Labels introduced inside the box are local to the box.

Use case boxes for disjunction elimination

case_example : p \/ q, p => r, q => r |- r [
    l1 : p \/ q   by premise;
    l2 : p => r   by premise;
    l3 : q => r   by premise;
    @left [
        l4 : p    by assumption;
        l5 : r    by imp_e l4 l2;
    ]
    @right [
        l6 : q    by assumption;
        l7 : r    by imp_e l6 l3;
    ]
    l8 : r        by dis_e l1 @left @right;
]

The two case boxes must end in the same formula. The final line cites the disjunction and both boxes.

Use variables for universal introduction

all_identity : all x. P(x) |- all y. P(y) [
    l1 : all x. P(x)   by premise;
    @any [ var y0;
        l2 : P(y0)     by all_e l1;
        l3 : P(y0)     by copy l2;
    ]
    l4 : all y. P(y)   by all_i @any;
]

Put var y0; at the start of a box when the box should prove something for an arbitrary object. The displayed quantifier name in the conclusion can differ from the internal variable name.

Common Rules

The checker supports the standard introduction and elimination rules for propositional and first-order connectives. These names are used in proof lines:

• premise, assumption, copy
• con_i, con_e1, con_e2
• dis_i1, dis_i2, dis_e
• imp_i, imp_e
• neg_i, neg_e, bot_e
• all_i, all_e, exi_i, exi_e
• eq_i, eq_e

A proof line can also call another proof by name with by proof name refs. Use %inline proof name refs when you want the called proof expanded in the rendered box proof. Put %hide before a proof declaration when it should remain available for reuse but should not get its own proof tab in the interface.

Defining Rules

A custom rule looks like a proof, but its type uses ||-. Items before ||- are the references the rule expects. The formula after ||- is the formula the rule produces.

A rule that uses two line references

mp_rule : (|- p => q), (|- p) ||- q [
    r1 : |- p => q   by premise;
    r2 : |- p        by premise;
    r3 : q           by imp_e r2 r1;
]

This rule packages implication elimination. The caller must provide a reference proving p => q and a reference proving p, in that order.

Using the rule

use_mp_rule : r => s, r |- s [
    l1 : r => s   by premise;
    l2 : r        by premise;
    l3 : s        by mp_rule l1 l2;
]

A rule that takes a box reference

neg_from_box : (p |- bot) ||- ~p [
    r1 : p |- bot   by premise;
    r2 : ~p         by neg_i r1;
]

use_neg_from_box : p => bot |- ~p [
    l1 : p => bot    by premise;
    @contra [
        l2 : p       by assumption;
        l3 : bot     by imp_e l2 l1;
    ]
    l4 : ~p          by neg_from_box @contra;
]

A box can be passed to a custom rule just like it can be passed to a built-in rule. The box must prove the sequent required by the rule argument.

Rule declarations without a proof body

given_rule : (|- p) ||- q;

A declaration ending in a semicolon states a rule without proving it. Use this only when your course or exercise explicitly gives you the rule as available.

Using Proofs as Rules

A completed proof can be called from a later proof with proof. This is useful for small helper theorems that you want to reuse.

Define a reusable proof

and_left : p /\ q |- p [
    l1 : p /\ q   by premise;
    l2 : p        by con_e1 l1;
]

Call the proof later

use_and_left : (r /\ s) /\ t |- r /\ s [
    l1 : (r /\ s) /\ t   by premise;
    l2 : r /\ s          by proof and_left l1;
]

The helper proof and_left expects one premise of the form p /\ q. In the caller, that premise is (r /\ s) /\ t, so the conclusion becomes r /\ s.

Hide a helper proof from the proof tabs

%hide hidden_identity : p |- p [
    l1 : p   by premise;
    l2 : p   by copy l1;
]

use_hidden_identity : p |- p [
    l1 : p   by premise;
    l2 : p   by proof hidden_identity l1;
]

Hidden proofs are still checked and can still be reused. They are only omitted from the proof tab list to keep the rendered interface focused on the proofs you want to inspect.

Inline a helper proof in the rendered proof

use_and_left_inline : (r /\ s) /\ t |- r /\ s [
    l1 : (r /\ s) /\ t   by premise;
    l2 : r /\ s          by %inline proof and_left l1;
]

Without %inline, the rendered proof shows a single line that cites and_left. With %inline, the renderer expands the helper proof at the call site.

Inline a custom rule

use_mp_rule_inline : r => s, r |- s [
    l1 : r => s   by premise;
    l2 : r        by premise;
    l3 : s        by %inline mp_rule l1 l2;
]

Use %inline before a custom rule name, and use %inline proof before a proof name. If a called proof or rule itself contains inline calls, those calls are expanded too.

Small Examples

These examples are meant to demonstrate the syntax and the construction of proofs.

State a Premise

identity : p |- p [
    l1 : p   by premise;
]

Conjunction Introduction

pair : p, q |- p /\ q [
    l1 : p        by premise;
    l2 : q        by premise;
    l3 : p /\ q   by con_i l1 l2;
]

Implication Introduction

self_imp : |- p => p [
    @box [
        l1 : p    by assumption;
        l2 : p    by copy l1;
    ]
    l3 : p => p   by imp_i @box;
]

Universal Elimination

instantiate : all x. P(x) |- P(x) [
    l1 : all x. P(x)   by premise;
    l2 : P(x0)         by all_e l1;
]

Existential Elimination

exi_to_result : exi x. P(x), all y. (P(y) => q) |- q [
    l1 : exi x. P(x)          by premise;
    l2 : all y. (P(y) => q)   by premise;
    @case [ var a;
        l3 : P(a)             by assumption;
        l4 : P(a) => q        by all_e l2;
        l5 : q                by imp_e l3 l4;
    ]
    l6 : q                    by exi_e l1 @case;
]