Simple Imperative Programs¶

Arithmetic and Boolean Expressions¶

Syntax¶

Evaluation¶

Optimization¶

Lean Automation¶

Tacticals¶

Defining New Tactic Notations¶

The `cooper` Tactic¶

A Few More Handy Tactics¶

Evaluation as a Relation¶

Inference Rule Notation¶

Equivalence of the Definitions¶

Computational vs. Relational Definitions¶

Expressions With Variables¶

States¶

Syntax¶

Notations¶

Evaluation¶

Commands¶

Syntax¶

More Examples¶

Evaluating Commands¶

Evaluation as a Function (Failed Attempt)¶

Evaluation as a Relation¶

Determinism of Evaluation¶

Reasoning About Imp Programs¶

Additional Exercises¶