Proof Kinds

⚠️ Work in Progress: This section is under development.

This chapter covers different types of proofs used in Ursus verification.

Topics to be Covered

Direct Proofs

Forward reasoning
Backward reasoning
Proof by construction
Proof by calculation

Inductive Proofs

Structural induction
Well-founded induction
Mutual induction
Nested induction

Simulation Proofs

Forward simulation
Backward simulation
Bisimulation
Refinement proofs

Data refinement
Operation refinement
Protocol refinement
System refinement

Automated Proofs

Auto tactics
Decision procedures
SMT solvers
Proof search

Proof Strategies

When to Use Each

Direct Proofs: Simple properties, straightforward logic

Inductive Proofs: Recursive structures, iterative processes

Simulation Proofs: Implementation vs specification

Refinement Proofs: Abstraction levels

Automated Proofs: Routine properties, large proofs

Proof Techniques

Tactics

Basic tactics
Advanced tactics
Custom tactics
Tactical combinators

Lemmas

Helper lemmas
Inversion lemmas
Rewrite lemmas
Automation lemmas

Coming Soon

This section will include:

Proof examples
Tactic tutorials
Proof patterns
Automation strategies

See Also

Advanced Topics - Overview
Direct Proofs - Basic proofs
Tactics - Tactic reference
Verification Principles - Verification basics