\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Commands

Command Proof

Enter proof mode with a unique subgoal corresponding to the previous unproved lemma.

Command Qed

Close the current proof, if it’s completed (i.e. has no remaining unclosed goal).

Command Abort

Abort the current proof.

Command undo natural?

undo n undoes the n (default 1) last sentence(s). Concretely, the tactic restores the n\(^{th}\) previous prover state as the current one.

In general undo commands are not used in Squirrel scripts but used for Proof-General navigation.

Command Reset

Reset the prover state. This command can be undone with undo since it does not clear the prover state history.

Command include file

Attempt to find file file.sp, first in the same directory as the current Squirrel file, and then in the theories directory.

Example: Including theories/Basic.sp

include Basic.

If you install squirrel (with make install) and not running it from root directory of its sources, the theories directory is located in ~/.local/bin.

Command set ident = bool​natural

Set any squirrel option using its ident:

Option identifier	Description	Default value
timeout	Timeout for the solver in seconds	10
printTRSEquations	Print equations of the TRS	false
debugConstr	Debug information for the constraint checker	false
debugCompletion	Debug information for the completion checker	false
debugTactics	Debug information for tactics	false
processStrictAliasMode	Strict alias mode for processus	false
showStrengthenedHyp	Show hypothesis after strengthening	false
autoFADup	Automatic FA Dup	true
newInduction	New equivalence induction principle (FIXME)	false
postQuantumSound	Post-quantum soundness	false
checkInclude	Include will check proofs	true

Command print ident?

Show the definition of a given ident if it is a lemma, function, name, macro or system. print without idendifier shows the current system.

Example: printing a lemma

lemma [any] foo : true.

Goal foo : true

Proof.

[goal> Focused goal (1/1): System: any —————————————- true

admit.

[goal> lemma foo is proved

Qed.

lemma [any] foo : true Exiting proof mode.

print foo.

lemma [any] foo : true

Command search term in [system_id​system_exp]?

Search lemmas containing a given term (that can contain holes _ as specified in sterm). A system_id​system_expr can be specified, otherwise the command searches in any system.

Example: searching axioms with included patterns

axiom [any] bar1 [’a] : exists (x : ‘a), true.

axiom [any] bar1 [‘a] : exists (x:’a), true

axiom [any] bar2 [’a] : exists (x : ‘a -> ‘a), true.

axiom [any] bar2 [‘a] : exists (x:’a -> ‘a), true

search exists (x : _), _.

Search in context system [any]. Search result(s): axiom [any] bar2 [‘a] : exists (x:’a -> ‘a), true axiom [any] bar1 [‘a] : exists (x:’a), true

search exists (x : _ -> _), _.

Search in context system [any]. Search result(s): axiom [any] bar2 [‘a] : exists (x:’a -> ‘a), true

Command hint rewrite ident

Add a rewriting rule from the lemma ident to the user-defined rewriting database. The lemma should establish a local formula consisting of a universally quantified conditional equality. In other words, it should essentially be of the form forall binders, phi_1 => ... => phi_n => u = v.

The goal will be used to rewrite occurrences of u into the corresponding occurrences of v, assuming the conditions phi_1, ..., phi_n reduce to true (using Reduction).

Example: add rewriting rule

axiom [any] and_true_l (b : boolean) : (true && b) = b.

hint rewrite and_true_l.

Command prof

Print profiling information.