mathlib documentation

tactic.itauto

Intuitionistic tautology (itauto) decision procedure #

The itauto tactic will prove any intuitionistic tautology. It implements the well known G4ip algorithm: Dyckhoff, Contraction-free sequent calculi for intuitionistic logic.

All built in propositional connectives are supported: true, false, and, or, implies, not, iff, xor, as well as eq and ne on propositions. Anything else, including definitions and predicate logical connectives (forall and exists), are not supported, and will have to be simplified or instantiated before calling this tactic.

The resulting proofs will never use any axioms except possibly propext, and propext is only used if the input formula contains an equality of propositions p = q.

Implementation notes #

The core logic of the prover is in three functions:

The intuitionistic logic rules are separated into three groups:

This covers the core algorithm, which only handles true, false, and, or, and implies. For iff and eq, we treat them essentially the same as (p → q) ∧ (q → p), although we use a different prop representation because we have to remember to apply different theorems during replay. For definitions like not and xor, we just eagerly unfold them. (This could potentially cause a blowup issue for xor, but it isn't used very often anyway. We could add it to the prop grammar if it matters.)

Tags #

propositional logic, intuitionistic logic, decision procedure

inductive tactic.itauto.and_kind  :
Type

Different propositional constructors that are variants of "and" for the purposes of the theorem prover.

Constructor for xor p q.

Equations

Debugging printer for propositions.

A comparator for and_kind. (There should really be a derive handler for this.)

Equations

A comparator for propositions. (There should really be a derive handler for this.)

Equations

Debugging printer for proof objects.

A variant on proof.exfalso' that performs opportunistic simplification.

A variant on proof.or_elim that performs opportunistic simplification.

A variant on proof.app' that performs opportunistic simplification. (This doesn't do full normalization because we don't want the proof size to blow up.)

Get a new name in the pattern h0, h1, h2, ...

meta def tactic.itauto.context  :
Type

The context during proof search is a map from propositions to proof values.

Debug printer for the context.

Insert a proposition and its proof into the context, as in have : A := p. This will eagerly apply all level 1 rules on the spot, which are rules that don't split the goal and are validity preserving: specifically, we drop and A → ⊤ hypotheses, close the goal if we find a hypothesis, split all conjunctions, and also simplify ⊥ → A (drop), ⊤ → A (simplify to A), A ∧ B → C (curry to A → B → C) and A ∨ B → C (rewrite to (A → C) ∧ (B → C) and split).

Add A to the context Γ with proof p. This version of context.add takes a continuation and a target proposition B, so that in the case that is found we can skip the continuation and just prove B outright.

Map a function over the proof (regardless of whether the proof is successful or not).

Equations
def tactic.itauto.is_ok {α : Type u_1} :
bool × αoption α

Convert a value-with-success to an optional value.

Equations

Skip the continuation and return a failed proof if the boolean is false.

Equations

The search phase, which deals with the level 3 rules, which are rules that are not validity preserving and so require proof search. One obvious one is the or-introduction rule: we prove A ∨ B by proving A or B, and we might have to try one and backtrack.

There are two rules dealing with implication in this category: p, p → C ⊢ B where p is an atom (which is safe if we can find it but often requires the right search to expose the p assumption), and (A₁ → A₂) → C ⊢ B. We decompose the double implication into two subgoals: one to prove A₁ → A₂, which can be written A₂ → C, A₁ ⊢ A₂ (where we used A₁ to simplify (A₁ → A₂) → C), and one to use the consequent, C ⊢ B. The search here is that there are potentially many implications to split like this, and we have to try all of them if we want to be complete.

The main prover. This receives a context of proven or assumed lemmas and a target proposition, and returns a proof or none (with state for the fresh variable generator). The intuitionistic logic rules are separated into three groups:

  • level 1: No splitting, validity preserving: apply whenever you can. Left rules in context.add, right rules in prove
  • level 2: Splitting rules, validity preserving: apply after level 1 rules. Done in prove
  • level 3: Splitting rules, not validity preserving: apply only if nothing else applies. Done in search

The level 1 rules on the right of the turnstile are Γ ⊢ ⊤ and Γ ⊢ A → B, these are easy to handle. The rule Γ ⊢ A ∧ B is a level 2 rule, also handled here. If none of these apply, we try the level 2 rule A ∨ B ⊢ C by searching the context and splitting all ors we find. Finally, if we don't make any more progress, we go to the search phase.

Reifies an atomic or otherwise unrecognized proposition. If it is defeq to a proposition we have already allocated, we reuse it, otherwise we name it with a new index.

Reify an expr into a prop, allocating anything non-propositional as an atom in the atoms list.

Once we have a proof object, we have to apply it to the goal. (Some of these cases are a bit annoying because applyc gets the arguments wrong sometimes so we have to use to_expr instead.)

meta def tactic.itauto (use_dec use_classical : bool) (extra_dec : list expr) :

A decision procedure for intuitionistic propositional logic.

  • use_dec will add a ∨ ¬ a to the context for every decidable atomic proposition a.
  • use_classical will allow a ∨ ¬ a to be added even if the proposition is not decidable, using classical logic.
  • extra_dec will add a ∨ ¬ a to the context for specified (not necessarily atomic) propositions a.

A decision procedure for intuitionistic propositional logic. Unlike finish and tauto! this tactic never uses the law of excluded middle (without the ! option), and the proof search is tailored for this use case. (itauto! will work as a classical SAT solver, but the algorithm is not very good in this situation.)

example (p : Prop) : ¬ (p  ¬ p) := by itauto

itauto [a, b] will additionally attempt case analysis on a and b assuming that it can derive decidable a and decidable b. itauto * will case on all decidable propositions that it can find among the atomic propositions, and itauto! * will case on all propositional atoms. Warning: This can blow up the proof search, so it should be used sparingly.