From bcb74d0080c9d7e6e58d9740eae47fbd7475f444 Mon Sep 17 00:00:00 2001
From: bernborgess <bernborgess@outlook.com>
Date: Tue, 1 Apr 2025 14:38:34 -0300
Subject: [PATCH] Fixing back the AletheVerb indentation
---
spec/doc.tex | 87 +++++++++++++++++++++++-----------------------
spec/rule_list.tex | 62 ++++++++++++++++-----------------
2 files changed, 75 insertions(+), 74 deletions(-)
diff --git a/spec/doc.tex b/spec/doc.tex
index 1ba20c3..d535d14 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -670,25 +670,25 @@ An Alethe proof is a list of commands.
\begin{figure}[t]
\begin{AletheVerb}
- (assume h1 (not (p a)))
- (assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
- ...
- (anchor :step t9 :args ((vr4 U) (:= (z2 U) vr4)))
- (step t9.t1 (cl (= z2 vr4)) :rule refl)
- (step t9.t2 (cl (= (p z2) (p vr4)))
- :rule cong :premises (t9.t1))
- (step t9 (cl (= (forall ((z2 U)) (p z2))
- (forall ((vr4 U)) (p vr4))))
- :rule bind)
- ...
- (step t14 (cl (forall ((vr5 U)) (p vr5)))
- :rule th_resolution :premises (t11 t12 t13))
- (step t15 (cl (or (not (forall ((vr5 U)) (p vr5)))
- (p a)))
- :rule forall_inst :args ((:= vr5 a)))
- (step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
- :rule or :premises (t15))
- (step t17 (cl) :rule resolution :premises (t16 h1 t14))
+(assume h1 (not (p a)))
+(assume h2 (forall ((z1 U)) (forall ((z2 U)) (p z2))))
+...
+(anchor :step t9 :args ((vr4 U) (:= (z2 U) vr4)))
+(step t9.t1 (cl (= z2 vr4)) :rule refl)
+(step t9.t2 (cl (= (p z2) (p vr4)))
+ :rule cong :premises (t9.t1))
+(step t9 (cl (= (forall ((z2 U)) (p z2))
+ (forall ((vr4 U)) (p vr4))))
+ :rule bind)
+...
+(step t14 (cl (forall ((vr5 U)) (p vr5)))
+ :rule th_resolution :premises (t11 t12 t13))
+(step t15 (cl (or (not (forall ((vr5 U)) (p vr5)))
+ (p a)))
+ :rule forall_inst :args ((:= vr5 a)))
+(step t16 (cl (not (forall ((vr5 U)) (p vr5))) (p a))
+ :rule or :premises (t15))
+(step t17 (cl) :rule resolution :premises (t16 h1 t14))
\end{AletheVerb}
\caption{Example proof output. Assumptions are
introduced; a subproof renames bound variables; the proof finishes with
@@ -921,17 +921,18 @@ remove the steps of the subproof from memory after checking it.
expressed as a concrete proof.
\begin{AletheVerb}
- (assume h1 (forall ((x S)) (P x)))
- (assume h2 (not (forall ((y S)) (P y))))
- (anchor :step t5 :args ((y S) (:= (x S) y)))
- (step t3 (cl (= x y)) :rule refl)
- (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
- (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
- :rule bind)
- (step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
- (not (forall ((x S)) (P x)))
- (forall ((y S)) (P y))) :rule equiv_pos2)
- (step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
+(assume h1 (forall ((x S)) (P x)))
+(assume h2 (not (forall ((y S)) (P y))))
+(anchor :step t5 :args ((y S) (:= (x S) y)))
+(step t3 (cl (= x y)) :rule refl)
+(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule bind)
+(step t6 (cl (not (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ (not (forall ((x S)) (P x)))
+ (forall ((y S)) (P y))) :rule equiv_pos2)
+(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
+
\end{AletheVerb}
\end{example}
@@ -1099,11 +1100,11 @@ the calculation of the context of the steps in the subproof.
The proof in Example~\ref{ex:ti:ctx-concrete} has only one subproof
and this subproof is also a first-innermost subproof. It is the subproof
\begin{AletheVerb}
- (anchor :step t5 :args ((y S) (:= (x S) y)))
- (step t3 (cl (= x y)) :rule refl)
- (step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
- (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
- :rule bind)
+(anchor :step t5 :args ((y S) (:= (x S) y)))
+(step t3 (cl (= x y)) :rule refl)
+(step t4 (cl (= (P x) (P y))) :rule cong :premises (t3))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule bind)
\end{AletheVerb}
\end{example}
@@ -1195,14 +1196,14 @@ $P_1 = E(P)$, $P_2 = E(E(P))$ and $P_{\mathit{last}} = E(P_{\mathit{last}})$.
Example~\ref{ex:ti:ctx-concrete} gives us the proof
\begin{AletheVerb}
- (assume h1 (forall ((x S)) (P x)))
- (assume h2 (not (forall ((y S)) (P y))))
- (step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
- :rule hole)
- (step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
- (not (forall ((x S)) (P x)))
- (forall ((y S)) (P y)))) :rule equiv_pos2)
- (step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
+(assume h1 (forall ((x S)) (P x)))
+(assume h2 (not (forall ((y S)) (P y))))
+(step t5 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y))))
+ :rule hole)
+(step t6 (cl (= (forall ((x S)) (P x)) (forall ((y S)) (P y)))
+ (not (forall ((x S)) (P x)))
+ (forall ((y S)) (P y)))) :rule equiv_pos2)
+(step t7 (cl) :rule resolution :premises (h1 h2 t5 t6))
\end{AletheVerb}
Since this proof contains no subproof, it is also $P_{\mathit{last}}$.
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index b2aebdf..e13972e 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -483,8 +483,8 @@ to quickly find the definition of rules.
A simple \proofRule{la_generic} step in the logic \textsf{LRA} might look like this:
\begin{AletheVerb}
- (step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
- :rule la_generic :args (1.0 -1.0))
+(step t10 (cl (not (> (f a) (f b))) (not (= (f a) (f b))))
+ :rule la_generic :args (1.0 -1.0))
\end{AletheVerb}
To verify this we have to check the unsatisfiability of $(f\,a) > (f\,b) \land
@@ -497,8 +497,8 @@ to quickly find the definition of rules.
\begin{RuleExample}
The following \proofRule{la_generic} step is from a \textsf{QF\_UFLIA} problem:
\begin{AletheVerb}
- (step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
- :rule la_generic :args (1.0 1/4))
+(step t11 (cl (not (<= f3 0)) (<= (+ 1 (* 4 f3)) 1))
+ :rule la_generic :args (1.0 1/4))
\end{AletheVerb}
After normalization we get $-f_3 \geq 0 \land 4\times f_3 > 0$.
This time step~4 applies and we can strengthen this to
@@ -692,9 +692,9 @@ to quickly find the definition of rules.
\begin{RuleExample}
An application of the \proofRule{forall_inst} rule.
\begin{AletheVerb}
- (step t16 (cl (or (not (forall ((x S) (y T)) (P y x )))
- (P b (f a))
- :rule forall_inst :args ((f a) b)
+(step t16 (cl (or (not (forall ((x S) (y T)) (P y x )))
+ (P b (f a))
+ :rule forall_inst :args ((f a) b)
\end{AletheVerb}
\end{RuleExample}
@@ -840,10 +840,10 @@ to quickly find the definition of rules.
\begin{RuleExample}
An application of the \proofRule{or} rule.
\begin{AletheVerb}
- (step t15 (cl (or (= a b) (not (<= a b)) (not (<= b a))))
- :rule la_disequality)
- (step t16 (cl (= a b) (not (<= a b)) (not (<= b a)))
- :rule or :premises (t15))
+(step t15 (cl (or (= a b) (not (<= a b)) (not (<= b a))))
+ :rule la_disequality)
+(step t16 (cl (= a b) (not (<= a b)) (not (<= b a)))
+ :rule or :premises (t15))
\end{AletheVerb}
\end{RuleExample}
@@ -1370,22 +1370,22 @@ to quickly find the definition of rules.
\rightarrow (f\,x)\land (f\,y))$ look like this:
\begin{AletheVerb}
- (anchor :step t3 :args ((x S) (:= (y S) x)))
- (step t3.t1 (cl (= x y)) :rule refl)
- (step t3.t2 (cl (= (= x y) (= x x)))
- :rule cong :premises (t3.t1))
- (step t3.t3 (cl (= x y)) :rule refl)
- (step t3.t4 (cl (= (f y) (f x)))
- :rule cong :premises (t3.t3))
- (step t3.t5 (cl (= (and (f x) (f y)) (and (f x) (f x))))
- :rule cong :premises (t3.t4))
- (step t3.t6 (cl (= (=> (= x y) (and (f x) (f y)))
- (=> (= x x) (and (f x) (f x)))))
- :rule cong :premises (t3.t2 t3.t5))
- (step t3 (cl (=
+(anchor :step t3 :args ((x S) (:= (y S) x)))
+(step t3.t1 (cl (= x y)) :rule refl)
+(step t3.t2 (cl (= (= x y) (= x x)))
+ :rule cong :premises (t3.t1))
+(step t3.t3 (cl (= x y)) :rule refl)
+(step t3.t4 (cl (= (f y) (f x)))
+ :rule cong :premises (t3.t3))
+(step t3.t5 (cl (= (and (f x) (f y)) (and (f x) (f x))))
+ :rule cong :premises (t3.t4))
+(step t3.t6 (cl (= (=> (= x y) (and (f x) (f y)))
+ (=> (= x x) (and (f x) (f x)))))
+ :rule cong :premises (t3.t2 t3.t5))
+(step t3 (cl (=
(forall ((x S) (y S)) (=> (= x y) (and (f x) (f y))))
(forall ((x S)) (=> (= x x) (and (f x) (f x))))))
- :rule onepoint)
+ :rule onepoint)
\end{AletheVerb}
\end{RuleExample}
@@ -1713,12 +1713,12 @@ to quickly find the definition of rules.
by Carcara's elaborator. It elaborates an implicit application of
symmetry of equality.
\begin{AletheVerb}
- (step t1 (cl (= (= 0 1) (= 1 0))) :rule eq_symmetric)
- (anchor :step t2 :args ((p Bool) (:= (p Bool) p)))
- (step t2.t1 (cl (= (= p false) (= false p))) :rule eq_symmetric)
- (step t2 (cl (= (let ((p (= 0 1))) (= p false))
- (let ((p (= 1 0))) (= false p))))
- :rule bind_let :premises (t1))
+(step t1 (cl (= (= 0 1) (= 1 0))) :rule eq_symmetric)
+(anchor :step t2 :args ((p Bool) (:= (p Bool) p)))
+(step t2.t1 (cl (= (= p false) (= false p))) :rule eq_symmetric)
+(step t2 (cl (= (let ((p (= 0 1))) (= p false))
+ (let ((p (= 1 0))) (= false p))))
+ :rule bind_let :premises (t1))
\end{AletheVerb}
\end{RuleExample}
--
GitLab