Start defining contexts

althelf/README.md

@@ -5,7 +5,7 @@ fulfill some restrictions (For example, all conclusions must be printed),
 and use a specific signature.  The signature collects the Alethe proof rules.
 To avoid confusion, this document refers to Alethe as "Alethe Classic".
 
-An Althe Classic consumer should be able to use the AltheLF proofs, by only
+An Alethe Classic consumer should be able to use the AltheLF proofs, by only
 changing its parser.
 
 ## Changes
@@ -13,7 +13,20 @@ changing its parser.
 * We assume that AletheLF is extended with a `:match-conclusion` feature
   that captures the conclusion of the step.  This is very useful for Alethe
   Classic proofs, since they allow us to avoid extra arguments.
-* `cl` is not unary, instead `(cl)` is the term `false`.  Hence, a the simple
-	`false` term should be parsed as the empty clause, and `cl false` is the
-	 clause containing the literal `false`.
-* Sharing doesn't use `!named`, but instead uses `define` statements.
+* `cl` cannot be used without arguments.  To write `(cl)` AletheLF uses the term
+  `false`.  Hence, a the simple `false` term should be parsed as the empty
+  clause, and `cl false` is the clause containing the literal `false`.
+* Sharing doesn't use `! .. :named`, but instead uses `define` statements.
+
+## Contexts
+
+Alethe Classic has a notion of contexts used to reason about binders.  Contexts
+are lists of variable assignments and shadowings (self assignments). In AletheLF
+a context is represented as a conjunction of equalities `= x t` where `x` is a
+variable and `t` a term.
+
+Since context are scoped, we use AletheLF's context mechanism.  The extended
+context become assumptions of the scope and premises of steps that use contexts.
+Hence, the equivalent to an `anchor` is an `assume-push`.  The
+context-manipulating rules are rules with `:assumption` that check that the
+assumption is the appropriately extended context.

althelf/alethe.smt3

@@ -43,10 +43,10 @@
   :match-conclusion CL
 )
 
-% TODO
-(declare-rule subproof ()
-  :args ()
-  :conclusion true
+(declare-rule subproof ((F Bool) (G Bool))
+  :assumption F
+  :premises (G)
+  :conclusion (=> F G)
 )
 
 % TODO: side condition
@@ -76,10 +76,12 @@
   :match-conclusion CL
 )
 
-% TODO
-(declare-rule bind ()
-  :args ()
-  :conclusion true
+% TODO: side conditiion
+(declare-rule bind ((ctx Bool))
+  :assumption ctx
+  :premises ((cl (= phi phi')))
+  :requires ((check_bind ctx xs ys) true)
+  :match-conclusion (cl (= (forall xs phi) (forall ys phi')))
 )
 
 % TODO