Theoretical Points from Michael's Lectures

Tactics: Properties of Equality

Reflexivity: t = t

Symmetry: If s = t, then t = s

Transitivity: If s = t and t = u, then s = u

Congruence: If s = t, then f(s) = f(t) (used by the f_equal tactic to strip outer functions from goal)

Tactics: Properties of Inductive Data - Disjointness

• Different constructors can never be equal

• Example: 0 ≠ S(n)

• If assumption violates this, goal can be proven via Principle of Explosion; from contradiction you can prove anything (discriminate tactic)

Tactics: Properties of Inductive Data - Injectivity

• Constructors are one-to-one

• Example: S(n) = S(m) => n = m

• Extracted using injection tactic

Tactics: Controlled Fibbing

• assert/admit tactic temporarily introduces a hypothesis without immediate evidence

• Forces you to follow through and prove later

Propositions vs. Booleans - The Universe Hierarchy

• Set (data) used for defining data

• Prop (logic) used for propositions (statements with a truth value)

• Type used for parameters or universe levels

Are Booleans propositions or data?

• bool are purely data (inhabiting Set)

• To use Boolean logically, it must be promoted to a proposition

• Example: _ = true

Can propositions be defined inductively?

• Yes; they separate their pure logical definition from their algorithmic implementation

• Makes them more flexible and powerful for complex proofs i.e. Reachability

What is Reachability?

Defining a safe system where bad states can’t be reached from start state

Why does Rocq enforce that all recursive functions (Fixpoint) terminate?

• If non-terminating functions were allowed, you can create an infinite loop to try “prove” 1 = 2

• Would never be able to check if proof is lying

• Destroys logic system reliability

Why does Rocq have to approximate termination?

• Halting Problem dictates that no program can universally decide if another program terminates

• Does this by demanding that at least 1 argument is structurally decreasing in recursive calls

If an algorithm doesn’t structurally decrease, how can you prove termination?

• By supplying a well-founded relation

• Relation is well-founded if it has no infinitely decreasing chains of elements, proving that you’re always moving towards an end point

How do you make automated theorem proving decidable?

• Restrict the language of premises and goals

• E.g. to linear arithmetic, strings, or arrays

• Problem becomes mathematically decidable

What are Equality and Uninterpreted Functions? (EUF)

• A decidable fragment with no quantifiers, only equations where functions are treated as “just symbols”

What algorithm is predominantly used to solve EUF?

• Congruence Closure (congruence tactic)

• Assigns terms to congruence classes and merges them graphically to achieve:

  • reflexive

  • symmetric

  • transitive

  • and congruent closure

How does backward chaining work as a search heuristic for undecidable problems?

• Engine starts at target goal/query

• Works backward to find matching premises

• (this is how auto tactic and Prolog work)

How does forward chaining work as a search heuristic for undecidable problems?

• Engine starts from known premises

• Derives more facts forward until it eventually reaches the goal