/* 
 * Formalization of integers, addition, and a proof that addition commutes
 *
 * Author: Jonathan Aldrich
 * 
 * This file defines natural numbers in terms of zero (z) and successor s n,
 * defines judgments for sums and less than, proves a few simple theorems,
 * and then inductively proves that addition commutes.  As we go along,
 * we illustrate the SASyLF language in tutorial style.
 *
 */


/** The package declaration is currently a placeholder, but
 * will eventually support a module system for SASyLF
 */
package edu.cmu.cs.sum;

/** SASyLF programs explicitly declare terminals that are
 * used to parse expressions.  This helps the SASyLF parser
 * detect problems in the input grammar--anything that is not
 * a declared terminal, non-terminal, or variable must be an error.
 * The user should declare all identifiers used in syntax and judgment
 * that do not themselves denote syntactic classes.  Symbols like
 * + or |- do not need to be declared, even if they are terminals.
 */
terminals z s


/************************ SYNTAX **************************************/

/** The syntax section declares the syntax of the formal
 * system, in this case of the lambda calculus.  Syntax is
 * given using an ordinary BNF grammar.
 */
syntax

/** This declaration declares n as a nonterminal, representing a natural
 * number.  n and variants of n (n', n'', n1, n2, etc.--you can add
 * primes or numbers) are used as metavariables for this syntactic
 * category, as commonly used in the PL research literature.
 */
n ::= z
  | s n


/************************ JUDGMENTS **************************************/

/** We declare a judgment with a name ("sum") and a form ("n + n = n").
 * The judgment is then followed by a series of inference rules that define
 * the judgment's semantics.
 *
 * Rules are defined with the premises above the line and the conclusion
 * below the line.
 */

judgment sum: n + n = n

--------- sum-z
z + n = n

n1 + n2 = n3
-------------------- sum-s
(s n1) + n2 = (s n3)


judgment less: n < n

------- less-one
n < s n

n1 < n3
n3 < n2
------- less-transitive
n1 < n2



/************************ THEOREMS **************************************/





/*************************
 * Test richer induction *
 *************************/

theorem sum-s-rh: forall d1: n1 + n2 = n3 exists n1 + (s n2) = (s n3).

d2: n1 + (s n2) = s n3 by induction on d1:

/* A rule case is of the form "case rule <rule> is <derivation> end case"
 * Here <rule> is a rule defined above, but instantiated with actual
 * expressions as appropriate for the judgment we are doing case analysis over.
 */

case rule

----------------- sum-z
dzc: (z) + n = n

is

dz1: (z) + (s n) = (s n) by rule sum-z

end case


case rule

dsp: n1' + n2 = n3'
---------------------------- sum-s
dsc: (s n1') + n2 = (s n3')

is

ds1: n1' + (s n2) = (s n3') by induction hypothesis on dsp
ds2: (s n1') + (s n2) = (s s n3') by rule sum-s on ds1

end case
end induction
end theorem



/***********************
 * Test a real theorem *
 ***********************/

theorem sum-commutes: forall d1: n1 + n2 = n3 exists n2 + n1 = n3.

d2: n2 + n1 = n3 by induction on d1:

case rule

----------------- sum-z
dzc: (z) + n = n

is

/* We can use a theorem or lemma previously defined, just like a rule,
 * by giving a syntax or a judgment for each of the "forall" clauses
 * of the theorem.
 */

dz1: n + (z) = n by theorem sum-z-rh on n

end case


case rule

dsp: n1' + n2 = n3'
---------------------------- sum-s
dsc: (s n1') + n2 = (s n3')

is

ds1: n2 + n1' = n3' by induction hypothesis on dsp
ds2: n2 + (s n1') = (s n3') by theorem sum-s-rh on ds1

end case
end induction
end theorem


and theorem sum-z-rh: forall n exists n + (z) = n.

d1: n + (z) = n by induction on n:

case z is
	d2: (z) + (z) = (z)	by rule sum-z
end case

case s n' is
	d3: n' + (z) = n'	by induction hypothesis on n'
	d4: (s n') + (z) = (s n')	by rule sum-s on d3
end case

end induction

end theorem