Is there an un-Classical version of the `tauto` tactic?

Stream: new members

[Lars Ericson]

Consider:

import Mathlib

variable (p q r : Prop)

theorem ta (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) :=
  by tauto

theorem tb (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) :=
  or_and_left.2 hpqpr

#check ta -- (p q r : Prop) (hpqpr : (p ∨ q) ∧ (p ∨ r)) : p ∨ q ∧ r
#check tb -- the same as ta

#explode ta
#explode tb

The #explode ta gives a proof which uses em:

ta : ∀ (p q r : Prop), (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

0 │          │ p                   ├ Prop
1 │          │ q                   ├ Prop
2 │          │ r                   ├ Prop
3 │          │ hpqpr               ├ (p ∨ q) ∧ (p ∨ r)
4 │          │ em✝                 │ ┌ (a : Prop) → Decidable a
5 │          │ left✝               │ │ ┌ p ∨ q
6 │          │ right✝              │ │ ├ p ∨ r
7 │          │ h✝                  │ │ │ ┌ p
8 │          │ h✝                  │ │ │ │ ┌ p
9 │          │ or_iff_not_imp_left │ │ │ │ │ p ∨ q ∧ r ↔ ¬p → q ∧ r
10│          │ a✝                  │ │ │ │ │ ┌ ¬p
11│8,10      │ absurd              │ │ │ │ │ │ q
12│8,10      │ absurd              │ │ │ │ │ │ r
13│11,12     │ And.intro           │ │ │ │ │ │ q ∧ r
14│10,13     │ ∀I                  │ │ │ │ │ ¬p → q ∧ r
15│9,14      │ Iff.mpr             │ │ │ │ │ p ∨ q ∧ r
16│8,15      │ ∀I                  │ │ │ │ p → p ∨ q ∧ r
17│          │ h✝                  │ │ │ │ ┌ r
18│          │ a✝                  │ │ │ │ │ ┌ ¬p
19│7,18      │ absurd              │ │ │ │ │ │ q
20│19,17     │ And.intro           │ │ │ │ │ │ q ∧ r
21│18,20     │ ∀I                  │ │ │ │ │ ¬p → q ∧ r
22│9,21      │ Iff.mpr             │ │ │ │ │ p ∨ q ∧ r
23│17,22     │ ∀I                  │ │ │ │ r → p ∨ q ∧ r
24│6,16,23   │ Or.casesOn          │ │ │ │ p ∨ q ∧ r
25│7,24      │ ∀I                  │ │ │ p → p ∨ q ∧ r
26│          │ h✝                  │ │ │ ┌ q
27│          │ h✝                  │ │ │ │ ┌ p
28│          │ a✝                  │ │ │ │ │ ┌ ¬p
29│27,28     │ absurd              │ │ │ │ │ │ r
30│26,29     │ And.intro           │ │ │ │ │ │ q ∧ r
31│28,30     │ ∀I                  │ │ │ │ │ ¬p → q ∧ r
32│9,31      │ Iff.mpr             │ │ │ │ │ p ∨ q ∧ r
33│27,32     │ ∀I                  │ │ │ │ p → p ∨ q ∧ r
34│          │ h✝                  │ │ │ │ ┌ r
35│          │ a✝                  │ │ │ │ │ ┌ ¬p
36│26,34     │ And.intro           │ │ │ │ │ │ q ∧ r
37│35,36     │ ∀I                  │ │ │ │ │ ¬p → q ∧ r
38│9,37      │ Iff.mpr             │ │ │ │ │ p ∨ q ∧ r
39│34,38     │ ∀I                  │ │ │ │ r → p ∨ q ∧ r
40│6,33,39   │ Or.casesOn          │ │ │ │ p ∨ q ∧ r
41│26,40     │ ∀I                  │ │ │ q → p ∨ q ∧ r
42│5,25,41   │ Or.casesOn          │ │ │ p ∨ q ∧ r
43│5,6,42    │ ∀I                  │ │ p ∨ q → p ∨ r → p ∨ q ∧ r
44│3,43      │ And.casesOn         │ │ p ∨ q ∧ r
45│4,44      │ ∀I                  │ ((a : Prop) → Decidable a) → p ∨ q ∧ r
46│45        │ letFun              │ p ∨ q ∧ r
47│0,1,2,3,46│ ∀I                  │ ∀ (p q r : Prop), (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

The #explode tb gives a more terse proof which is not Classical:

tb : ∀ (p q r : Prop), (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

0│         │ p           ├ Prop
1│         │ q           ├ Prop
2│         │ r           ├ Prop
3│         │ hpqpr       ├ (p ∨ q) ∧ (p ∨ r)
4│         │ or_and_left │ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
5│4,3      │ Iff.mpr     │ p ∨ q ∧ r
6│0,1,2,3,5│ ∀I          │ ∀ (p q r : Prop), (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

Is there a version of tauto which limits itself to what it can do without em?

[Newell Jensen]

Try itauto

[Lars Ericson]

Perhaps intuitionistic logic is no longer top of mind. itauto gives tactic 'Mathlib.Tactic.itauto' has not been implemented in

import Mathlib

variable (p q r : Prop)

theorem ta (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) :=
  by itauto -- tactic 'Mathlib.Tactic.itauto' has not been implemented

[Henrik Böving]

generally speaking the focus on having an un classical tool in Lean if there is a classical one available is very low right now.

[Lars Ericson]

In terms of what I was looking at above, I don't actually know that or_and_left.2 hpqpr is un-Classical, because it is not really exploding the or_and_left.2 in

4│         │ or_and_left │ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
5│4,3      │ Iff.mpr     │ p ∨ q ∧ r
6│0,1,2,3,5│ ∀I          │ ∀ (p q r : Prop), (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

Is there an alternative to #explode which will trace one level down into or_and_left in

import Mathlib

variable (p q r : Prop)
variable (hpqpr: (p ∨ q) ∧ (p ∨ r))

#explode or_and_left.2 hpqpr -- need trace one level deeper

[Kyle Miller]

No, #explode doesn't have any features to unfold theorems. It could be implemented, but I'm not sure what the use case is. Is following it up with #explode or_and_left not sufficient for you?

[Kyle Miller]

If you care about classical axioms, there's also #print axioms or_and_left, which gives you the answer more directly.

[Lars Ericson]

@Kyle Miller, I am going through these exercises in the Theorem Proving in Lean 4 book. The exercises are divided into un-Classical

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) := sorry

and Classical ones:

open Classical

variable (p q r : Prop)

example : (p → q ∨ r) → ((p → q) ∨ (p → r)) := sorry

I am just being obsessive-compulsive in trying to verify that the un-Classical exercise is actually un-Classical. I am stuck because I want to do this by cases, which is Classical. tauto also uses em. I am looking at #explode of or_and_left because my training so far in Theorem Proving in Lean 4 is insufficient to be able to read this definition, which has some very terse syntax which hasn't been introduced yet in the book. If I can't read it, I can't sugar it into something that I can reproduce, which is why I am looking for a trace:

import Mathlib

/-- `∨` distributes over `∧` (on the left). -/
theorem or_and_left : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) :=
  ⟨Or.rec (fun ha => ⟨.inl ha, .inl ha⟩) (.imp .inr .inr),
   And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro)⟩

[Ruben Van de Velde]

If you have a term mode proof like this and want to sugar it, you can do it step by step by adding by exact at the start of the proof and then incrementally work though it

[Ruben Van de Velde]

The pointy brackets are equivalent to constructor

[Kyle Miller]

Kyle Miller said:

If you care about classical axioms, there's also #print axioms or_and_left, which gives you the answer more directly.

Let me mention this command again, since that will tell you whether it depends on Classical.choice

[Ruben Van de Velde]

(the point is that at every step, you have a working proof you can inspect)

[Lars Ericson]

Without deconstructing or_and_left, I tried to do it again and I came down to a point where I want to do reasoning by cases on p ∨ q. I don't know if proof by cases in this instance requires em because it's not exactly saying p ∨ ¬p, it's just saying that if I know p ∨ q then either p or q must be true, which seems like a minimum expectation of ∨ . Then I asked Google Bard how to do proof by cases on disjunction in Lean 4 and it gave me rcases, but I couldn't figure out from docs#rcases how to use it in Lean 4. There are no examples of rcases in Theorem Proving in Lean 4. I did stumble on Or.by_cases in Mathlib, which seems promising but then I got another roadblock: Lean 4 gave me error failed to synthesize instance Decidable p in

import Mathlib

theorem L1l1 (hp: p) : p ∨ q := Or.inl hp

theorem L1l2 (hqr: q ∧ r) : p ∨ q := Or.inr hqr.left

theorem L1l (hpqr: p ∨ (q ∧ r)) : (p ∨ q) := Or.elim hpqr L1l1 L1l2

theorem L1r1 (hqr: q ∧ r) : p ∨ r := Or.inr hqr.right

theorem L1r (hpqr: p ∨ (q ∧ r)) : (p ∨ r) := Or.elim hpqr L1l1 L1r1

theorem L1 (hpqr: p ∨ (q ∧ r)) : (p ∨ q) ∧ (p ∨ r) :=
  And.intro (L1l hpqr) (L1r hpqr)

theorem L2 (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) :=
  have hpq : p ∨ q := hpqpr.left
  have hpr : p ∨ r := hpqpr.right
  Or.by_cases hpq -- failed to synthesize instance Decidable p

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
  Iff.intro L1 L2

Is there a way to make Or.by_cases work or another method of doing the same? I need to do a nested proof with four cases p,p, p,r, q,p and q,r, i.e. it is roughly an Or.by_cases hpq (Or.by_cases hpr) (Or.by_cases hpr).

[Mario Carneiro]

there are many examples of rcases in mathlib

[Mario Carneiro]

Did you see docs#Std.Tactic.rcases ? What in the documentation was unclear?

[Lars Ericson]

@Mario Carneiro I'm just finding this a bit hard to read, and it doesn't walk through a complete example that for example would run self-contained in Lean 4 Playground. I can look for full examples by grepping through Mathlib. It would be very hepful if the Mathlib docs had the ability to push a button to pop examples into Lean 4 Playground in the same way as the button on Zulip works for inline code examples.

I think I've made a little more progress anyway. It occurred to me that I might be able to do a nested proof using Or.elim. This is where I'm at now, with one sorry in lemmaL2b:

import Mathlib

theorem L1l1 (hp: p) : p ∨ q := Or.inl hp

theorem L1l2 (hqr: q ∧ r) : p ∨ q := Or.inr hqr.left

theorem L1l (hpqr: p ∨ (q ∧ r)) : (p ∨ q) := Or.elim hpqr L1l1 L1l2

theorem L1r1 (hqr: q ∧ r) : p ∨ r := Or.inr hqr.right

theorem L1r (hpqr: p ∨ (q ∧ r)) : (p ∨ r) := Or.elim hpqr L1l1 L1r1

theorem L1 (hpqr: p ∨ (q ∧ r)) : (p ∨ q) ∧ (p ∨ r) :=
  And.intro (L1l hpqr) (L1r hpqr)

theorem L2a (hp : p) : p ∨ q ∧ r := Or.inl hp

theorem L2b (hpq : p ∨ q) (hpr : p ∨ r) (hq : q) : p ∨ q ∧ r := sorry

theorem L2 (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) :=
  have hpq : p ∨ q := hpqpr.left
  have hpr : p ∨ r := hpqpr.right
  Or.elim hpq
    L2a
    (L2b hpq hpr)

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
  Iff.intro L1 L2

[Mario Carneiro]

There are standalone simple examples in https://github.com/leanprover/std4/blob/main/test/rcases.lean

[Mario Carneiro]

in any case, the short answer to your question is that the way to use rcases on an or hypothesis is rcases hpq with h | h

[Mario Carneiro]

here's a proof of L2 using rcases:

theorem L2 (hpqpr: (p ∨ q) ∧ (p ∨ r)): p ∨ (q ∧ r) := by
  rcases hpqpr with ⟨hp | hq, hp | hr⟩
  · exact .inl hp
  · exact .inl hp
  · exact .inl hp
  · exact .inr ⟨hq, hr⟩

[Mario Carneiro]

by the way, since you asked: case analysis on p ∨ q is intuitionistically valid, it does not require em and if you use #print axioms L2 it will verify this

[Mario Carneiro]

This is the kind of "proof by cases" that is intuitionistically okay. by_cases is not intuitionistically valid because it first uses em to magic up a proof of p ∨ ¬p and then case splits on it. The case split is not the troublesome part, it is obtaining the p ∨ ¬p to split

[Lars Ericson]

Thank you @Mario Carneiro. I will bookmark the test directory!

I am still trying to unpack the syntax of or_and_left.2. There are a lot of advanced features in this:

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c)  :=
  And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro)

First the dot notation with no left hand side. Hovering over the .recs and .inls shows that these can be expanded to

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c)  :=
  And.rec <| Or.rec (fun _ => Or.inl ·) (Or.imp_right ∘ And.intro)

Then the pipeline notation <| which is explained in the Lean Manual (now also bookmarked) here. In this case it eliminates one parenthesis, so above can be rewritten as:

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c)  :=
  And.rec (Or.rec (fun _ => Or.inl ·) (Or.imp_right ∘ And.intro))

The composition operator ∘ is documented in Logic and Proof (now bookmarked). So g ∘ f is the same as fun x => g(fx)) giving

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c)  :=
  And.rec (Or.rec (fun _ => Or.inl ·) (fun x => Or.imp_right (And.intro x)))

The center dot · is documented in Functional Programming in Lean., according to which Or.inl · is the same as fun x => Or.inl x, giving:

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c)  :=
  And.rec (Or.rec (fun _ => (fun x => Or.inl x)) (fun x => Or.imp_right (And.intro x)))

Unfortunately this doesn't work, the error is

application type mismatch
  Or.inl x
argument
  x
has type
  a ∨ c : Prop
but is expected to have type
  a : Prop

The .rec notation is also unfamiliar. It is not used in Theorem Proving in Lean, the Lean Manual, or Functional Programming in Lean, as far as I can see. I don't see it in docs#And. Where is it described? I see it used in the source.

[Mario Carneiro]

Your unpacking of the dot notation is not quite right. The way it works is that you have an expression surrounded in parentheses with a · somewhere in it, and this means to replace the · with a fresh variable x and add fun x => at the parentheses. So (fun _ => Or.inl ·) is equivalent to fun x => fun _ => Or.inl x

[Mario Carneiro]

And.rec is the recursor for And, it is defined by the inductive command (every inductive type has a T.rec function)

[Mario Carneiro]

the type of the rec function follows the definition of the inductive type in a particular way; for And this will look something like (A -> B -> C) -> (A /\ B) -> C which is the same as the And.elim function, except that it allows C to depend on the proof of A /\ B (this usually isn't used and can be ignored for the most part)

[Lars Ericson]

Thank you @Mario Carneiro I see .rec discussed now in Theorem proving in Lean 4 in the Inductive Types section.

Thanks also for the reading of ·, that is very helpful.

[Lars Ericson]

Here it is mostly un-golfed (flogged?). I will play close attention to .rec when I get to the inductive chapter:

import Mathlib

lemma L1a : a → a ∨ c → a ∨ b ∧ c :=
  fun ha: a =>
  fun _ : a ∨ c =>
  Or.intro_left (b ∧ c) ha

lemma L1b : b → a ∨ c → a ∨ b ∧ c :=
  fun hb : b =>
  Or.imp_right (And.intro hb)

lemma L1 : a ∨ b → a ∨ c → a ∨ b ∧ c := Or.rec L1a L1b

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c) :=
   And.rec L1 -- And.rec <| .rec (fun _ => .inl ·) (.imp_right ∘ .intro)

[Mario Carneiro]

Are you aware that you can use have to introduce intermediary statements? You don't need to make definitions for everything (and it's better not to, since your short names like L1 will cause name clashes)

[Mario Carneiro]

theorem or_and_left2 : (a ∨ b) ∧ (a ∨ c) →  a ∨ (b ∧ c) :=
  have L1a : a → a ∨ c → a ∨ b ∧ c :=
    fun ha: a =>
    fun _ : a ∨ c =>
    Or.intro_left (b ∧ c) ha
  have L1b : b → a ∨ c → a ∨ b ∧ c :=
    fun hb : b =>
    Or.imp_right (And.intro hb)
  have L1 : a ∨ b → a ∨ c → a ∨ b ∧ c := Or.rec L1a L1b
  And.rec L1

[Lars Ericson]

Thanks @Mario Carneiro . I wanted to use a have but it didn't occur to me I could put whole proofs under the have. In examples, have is most often used to introduce terms, like have hp : p := h.left.

[Mario Carneiro]

but those are terms

[Mario Carneiro]

    fun ha: a =>
    fun _ : a ∨ c =>
    Or.intro_left (b ∧ c) ha

is a term

[Eric Wieser]

Should hightlighting use different colors for term and tactic keywords to make this kind of thing less confusing?

[Mario Carneiro]

I'm not sure we want to draw that kind of attention to it, it is deliberate design that have and let and if and match and sorry work the same in term and tactic mode

[Kevin Buzzard]

And rfl (which used to have two spellings)

[Kevin Buzzard]

(as did sorry a very very long time ago)

[Mario Carneiro]

have and let too: the tactics used to be called note and pose respectively, I think from coq

[Mario Carneiro]

admit still exists today, although IMO we should deprecate and remove it

[ZHAO Jiecheng]

Lars Ericson said:

Thanks Mario Carneiro . I wanted to use a have but it didn't occur to me I could put whole proofs under the have. In examples, have is most often used to introduce terms, like have hp : p := h.left.

It's important to understand that "Theorem Proving in Lean 4" isn't a short cut to learn logic or math, it just help you to understand lean. It is unusual that one wants to learn non-em tactic before he established the understanding of term.

Maybe you should just follow the book first. Do not stay too long in a chapter to try to understand everything. Actually, in Chapter 5 you will learn tactics and it will give you exercises to rewrite all the exercises in Chapter 3 and 4 into tactic way. Then you may feel much better.