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

source
@[protected, instance]
meta def tactic.itauto.and_kind.has_reflect  :
has_reflect tactic.itauto.and_kind
source
@[protected, instance]
def tactic.itauto.and_kind.decidable_eq  :
decidable_eq tactic.itauto.and_kind
source
inductive tactic.itauto.and_kind  :
Type

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

source
@[protected, instance]
def tactic.itauto.and_kind.inhabited  :
inhabited tactic.itauto.and_kind
Equations
source
@[protected, instance]
def tactic.itauto.prop.decidable_eq  :
decidable_eq tactic.itauto.prop
source
inductive tactic.itauto.prop  :
Type

A reified inductive type for propositional logic.

source
@[protected, instance]
meta def tactic.itauto.prop.has_reflect  :
has_reflect tactic.itauto.prop
source
def tactic.itauto.prop.and  :
tactic.itauto.prop → tactic.itauto.prop → tactic.itauto.prop

Constructor for p ∧ q.

Equations
source
def tactic.itauto.prop.iff  :
tactic.itauto.prop → tactic.itauto.prop → tactic.itauto.prop

Constructor for p ↔ q.

Equations
source
def tactic.itauto.prop.eq  :
tactic.itauto.prop → tactic.itauto.prop → tactic.itauto.prop

Constructor for p = q.

Equations
source
def tactic.itauto.prop.not (a : tactic.itauto.prop) :
tactic.itauto.prop

Constructor for ¬ p.

Equations
source
def tactic.itauto.prop.xor (a b : tactic.itauto.prop) :
tactic.itauto.prop

Constructor for xor p q.

Equations
source
@[protected, instance]
def tactic.itauto.prop.inhabited  :
inhabited tactic.itauto.prop
Equations
source
def tactic.itauto.and_kind.sides  :
tactic.itauto.and_kind → tactic.itauto.prop → tactic.itauto.prop → tactic.itauto.prop × tactic.itauto.prop

Given the contents of an and variant, return the two conjuncts.

Equations
source
meta def tactic.itauto.prop.to_format  :
tactic.itauto.prop → format

Debugging printer for propositions.

source
@[protected, instance]
meta def tactic.itauto.prop.has_to_format  :
has_to_format tactic.itauto.prop
source
def tactic.itauto.and_kind.cmp (p q : tactic.itauto.and_kind) :
ordering

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

Equations
source
def tactic.itauto.prop.cmp (p q : tactic.itauto.prop) :
ordering

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

Equations
source
@[protected, instance]
def tactic.itauto.prop.has_lt  :
has_lt tactic.itauto.prop
Equations
source
@[protected, instance]
def tactic.itauto.has_lt.lt.decidable_rel  :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
meta def tactic.itauto.proof.has_reflect  :
has_reflect tactic.itauto.proof
source
inductive tactic.itauto.proof  :
Type

A reified inductive proof type for intuitionistic propositional logic.

source
@[protected, instance]
def tactic.itauto.proof.inhabited  :
inhabited tactic.itauto.proof
Equations
source
meta def tactic.itauto.proof.to_format  :
tactic.itauto.proof → format

Debugging printer for proof objects.

source
@[protected, instance]
meta def tactic.itauto.proof.has_to_format  :
has_to_format tactic.itauto.proof
source
meta def tactic.itauto.proof.exfalso  :
tactic.itauto.prop → tactic.itauto.proof → tactic.itauto.proof

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

source
meta def tactic.itauto.proof.app  :
tactic.itauto.proof → tactic.itauto.proof → tactic.itauto.proof

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.)

source
meta def tactic.itauto.fresh_name {m : Type → Type u_1} [monad m] :
state_t ℕ m name

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

source
meta def tactic.itauto.context  :
Type

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

source
meta def tactic.itauto.context.to_format (Γ : tactic.itauto.context) :
format

Debug printer for the context.

source
@[protected, instance]
meta def tactic.itauto.context.has_to_format  :
has_to_format tactic.itauto.context
source
meta def tactic.itauto.context.add  :
tactic.itauto.prop → tactic.itauto.proof → tactic.itauto.context → except (tactic.itauto.prop → tactic.itauto.proof) tactic.itauto.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).

source
meta def tactic.itauto.context.with_add {m : Type → Type u_1} [monad m] (Γ : tactic.itauto.context) (A : tactic.itauto.prop) (p : tactic.itauto.proof) (B : tactic.itauto.prop) (f : tactic.itauto.context → tactic.itauto.prop → m tactic.itauto.proof) :
m tactic.itauto.proof

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.

source
meta def tactic.itauto.search (prove : tactic.itauto.context → tactic.itauto.prop → state_t ℕ option tactic.itauto.proof) :
tactic.itauto.context → tactic.itauto.prop → state_t ℕ option tactic.itauto.proof

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.

source
meta def tactic.itauto.prove  :
tactic.itauto.context → tactic.itauto.prop → state_t ℕ option tactic.itauto.proof

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.

source
meta def tactic.itauto.reify_atom (atoms : tactic.ref (buffer expr)) (e : expr) :
tactic tactic.itauto.prop

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.

source
meta def tactic.itauto.reify (atoms : tactic.ref (buffer expr)) :
expr → tactic tactic.itauto.prop

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

source
meta def tactic.itauto.apply_proof  :
name_map expr → tactic.itauto.proof → tactic unit

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.)

source
meta def tactic.interactive.itauto  :
tactic unit

A decision procedure for intuitionistic propositional logic. Unlike finish and tauto! this tactic never uses the law of excluded middle, and the proof search is tailored for this use case.

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