# 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, →, Not, Iff, Xor', as well as Eq and Ne on propositions. Anything else, including definitions and predicate logical connectives (∀ and ∃), 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. Using itauto!, one can enable the selective use of LEM for case splitting on specified propositions.

## Implementation notes #

The core logic of the prover is in three functions:

• prove : Context → IProp → StateM Nat (Bool × Proof): The main entry point. Gets a context and a goal, and returns a proof object or fails, using StateM Nat for the name generator.
• search : Context → IProp → StateM Nat (Bool × Proof): Same meaning as proof, called during the search phase (see below).
• Context.add : IProp → Proof → Context → Except (IProp → Proof) Context: Adds a proposition with its proof into the context, but it also does some simplifications on the spot while doing so. It will either return the new context, or if it happens to notice a proof of false, it will return a function to compute a proof of any proposition in the original context.

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.
• Context.add:
• simplify Γ, ⊤ ⊢ B to Γ ⊢ B
• Γ, ⊥ ⊢ B is true
• simplify Γ, A ∧ B ⊢ C to Γ, A, B ⊢ C
• simplify Γ, ⊥ → A ⊢ B to Γ ⊢ B
• simplify Γ, ⊤ → A ⊢ B to Γ, A ⊢ B
• simplify Γ, A ∧ B → C ⊢ D to Γ, A → B → C ⊢ D
• simplify Γ, A ∨ B → C ⊢ D to Γ, A → C, B → C ⊢ D
• prove:
• Γ ⊢ ⊤ is true
• simplify Γ ⊢ A → B to Γ, A ⊢ B
• search:
• Γ, P ⊢ P is true
• simplify Γ, P, P → A ⊢ B to Γ, P, A ⊢ B
• level 2: Splitting rules, validity preserving: apply after level 1 rules. Done in prove
• simplify Γ ⊢ A ∧ B to Γ ⊢ A and Γ ⊢ B
• simplify Γ, A ∨ B ⊢ C to Γ, A ⊢ C and Γ, B ⊢ C
• level 3: Splitting rules, not validity preserving: apply only if nothing else applies. Done in search
• Γ ⊢ A ∨ B follows from Γ ⊢ A
• Γ ⊢ A ∨ B follows from Γ ⊢ B
• Γ, (A₁ → A₂) → C ⊢ B follows from Γ, A₂ → C, A₁ ⊢ A₂ and Γ, C ⊢ B

This covers the core algorithm, which only handles True, False, And, Or, and →. For Iff and Eq, we treat them essentially the same as (p → q) ∧ (q → p), although we use a different IProp 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 IProp grammar if it matters.)

## Tags #

propositional logic, intuitionistic logic, decision procedure

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

Instances For
Equations
Equations
• = if h : x.toCtorIdx = y.toCtorIdx then else

A reified inductive type for propositional logic.

Instances For
Equations
@[match_pattern]

Constructor for p ∧ q.

Equations
Instances For
@[match_pattern]

Constructor for p ↔ q.

Equations
Instances For
@[match_pattern]

Constructor for p = q.

Equations
Instances For
@[match_pattern]

Constructor for ¬ p.

Equations
• a.not =
Instances For
@[match_pattern]

Constructor for xor p q.

Equations
• a.xor b = (a.and b.not).or (b.and a.not)
Instances For

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

Equations
Instances For

Debugging printer for propositions.

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

A reified inductive proof type for intuitionistic propositional logic.

• sorry: Mathlib.Tactic.ITauto.Proof

⊢ A, causes failure during reconstruction

• hyp:

(n: A) ⊢ A

• triv: Mathlib.Tactic.ITauto.Proof

⊢ ⊤

• exfalso':

(p: ⊥) ⊢ A

• intro:

(p: (x: A) ⊢ B) ⊢ A → B

• andLeft:
• ak = .and: (p: A ∧ B) ⊢ A
• ak = .iff: (p: A ↔ B) ⊢ A → B
• ak = .eq: (p: A = B) ⊢ A → B
• andRight:
• ak = .and: (p: A ∧ B) ⊢ B
• ak = .iff: (p: A ↔ B) ⊢ B → A
• ak = .eq: (p: A = B) ⊢ B → A
• andIntro:
• ak = .and: (p₁: A) (p₂: B) ⊢ A ∧ B
• ak = .iff: (p₁: A → B) (p₁: B → A) ⊢ A ↔ B
• ak = .eq: (p₁: A → B) (p₁: B → A) ⊢ A = B
• curry:
• ak = .and: (p: A ∧ B → C) ⊢ A → B → C
• ak = .iff: (p: (A ↔ B) → C) ⊢ (A → B) → (B → A) → C
• ak = .eq: (p: (A = B) → C) ⊢ (A → B) → (B → A) → C
• curry₂:

This is a partial application of curry.

• ak = .and: (p: A ∧ B → C) (q : A) ⊢ B → C
• ak = .iff: (p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C
• ak = .eq: (p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C
• app':

(p: A → B) (q: A) ⊢ B

• orImpL:

(p: A ∨ B → C) ⊢ A → C

• orImpR:

(p: A ∨ B → C) ⊢ B → C

• orInL:

(p: A) ⊢ A ∨ B

• orInR:

(p: B) ⊢ A ∨ B

• orElim':

(p₁: A ∨ B) (p₂: (x: A) ⊢ C) (p₃: (x: B) ⊢ C) ⊢ C

• decidableElim:

(p₁: Decidable A) (p₂: (x: A) ⊢ C) (p₃: (x: ¬ A) ⊢ C) ⊢ C

• em:
• classical = false: (p: Decidable A) ⊢ A ∨ ¬A
• classical = true: (p: Prop) ⊢ p ∨ ¬p
• impImpSimp:

The variable x here names the variable that will be used in the elaborated proof.

• (p: ((x:A) → B) → C) ⊢ B → C
Instances For
Equations

Debugging printer for proof objects.

Equations
Instances For

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

Equations
Instances For

A variant on Proof.orElim' that performs opportunistic simplification.

Equations
• x✝².orElim x✝¹ x✝ x = match x✝², x✝¹, x✝, x with | , x, q, r => | p, x, q, r => p.orElim' x q r
Instances For

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

Instances For
@[inline]

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

Equations
Instances For

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

Equations
Instances For

Debug printer for the context.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

@[inline]

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.

Equations
Instances For

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

Equations
• = match x with | (b, p) => (b, f p)
Instances For

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

Equations
• = match x with | ((false, snd), snd_1) => none | ((true, p), n) => some (p, n)
Instances For

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

Equations
• = match x✝¹, x✝, x with | false, x, x_1 => | true, x, f => f
Instances For

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.

partial def Mathlib.Tactic.ITauto.reify (e : Q(Prop)) :

Reify an Expr into a IProp, allocating anything non-propositional as an atom in the AtomM state.

partial def Mathlib.Tactic.ITauto.applyProof (g : Lean.MVarId) (Γ : ) :

Once we have a proof object, we have to apply it to the goal.

def Mathlib.Tactic.ITauto.itautoCore (g : Lean.MVarId) (useDec : Bool) (useClassical : Bool) (extraDec : ) :

A decision procedure for intuitionistic propositional logic.

• useDec will add a ∨ ¬ a to the context for every decidable atomic proposition a.
• useClassical will allow a ∨ ¬ a to be added even if the proposition is not decidable, using classical logic.
• extraDec will add a ∨ ¬ a to the context for specified (not necessarily atomic) propositions a.
Equations
• One or more equations did not get rendered due to their size.
Instances For

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For