intuitionistic logic

Stream: new members

[Michael Beeson]

lemma notnotLEM: ∀ (x t:M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
  assume x t,
  begin
       intro h,
      /-  now what? -/


  end

push_neg takes a non-intuitionistic step. How can I push the negation into h but don't erase the resulting double negation.
I wrote a couple of such rules myself. The tactic 'finish' can't do this one, which I really expected it to do. It is about as
hard to predict as Alexa--sometimes it works very well and other times it is lame.

[Mario Carneiro]

it's a tricky proof, and mathlib doesn't have any tactics that do intuitionistic proof search so you'll have to prove it yourself. The hint is to prove \neg x \in t

[Patrick Massot]

Michael, push_neg is the opposite of what you are doing. This tactic was written explicitly for teaching mathematics without any focus on exotic logic. For your specific need you can either create specific tools or go back to basics (here that would probably be rw not_or_distrib).

[Lars Ericson]

Doesn't it need a bit more setup prior to attempting the proof? For example M is not declared and you have t m : M followed by x ∈ t which is a little bit problematic unless M is some kind of lattice. In any event M needs to have ∈ defined, which it doesn't so far. In this slight elaboration of the above sketch:

import tactic

lemma notnotLEM (M: Type*): ∀ (x t:M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
begin
sorry,
end

we get the error

failed to synthesize type class instance for
M : Type ?,
x t : M
⊢ has_mem M M

Suppose we were to alter it slightly so that `M` is a set:

import tactic

universe u

lemma notnotLEM1 (α: Type u) (M: set α):
∀ (x t:M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
begin
sorry,
end

it's still complaining that the underlying type doesn't have membership constructed.

So let's let `M` be sets of natural numbers:

import tactic

lemma notnotLEM2 (M: set ℤ):
∀ (x t:M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
begin
sorry,
end

it's still complaining because you have `x ∈ t ` i.e. trying to show one member of `M` is an element of another member of `M`.

We could try using `lattice` instead of `set`:

import tactic
import order.lattice

lemma notnotLEM3 (M: lattice ℤ):
∀ (x t:M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
begin
sorry,
end

This then resolves the problem with `x ∈ t ` but leads to a new and confusing to me error that for type `M` we can no longer use the type notation `(x:M)`.  We get this error at the colen in `x t:M`:

type expected at
M
term has type
lattice ℤ

At this point you'd have to call an expert.

My point being just that the types have to be set up to support the language of membership that you are using before you can prove anything about that language.

I am a beginner, just guessing on above.  The drill for newcomers is to read and do the exercises closely in these two sites before trying to do anything complicated:

* #nng
* #tpil

[Eric Wieser]

@Lars Ericson, I think the correction you were trying to make is

lemma notnotLEM (M : Type*) : ∀ (x : M) (t : set M), ¬¬ (x ∈ t ∨ ¬ x ∈ t):=
begin
  sorry,
end

that is, changing t to be a set but leaving x alone.

[Mario Carneiro]

You don't need a lattice for this to typecheck, but you do need has_mem M M. The original statement is not self contained though so it's possible something equivalent to this is above the lemma in Michael Beeson's version (which is why #mwe's are important)

[Mario Carneiro]

For example based on this I expect that he has (M : Type*) [Model M] in the variables and instance [Model M] : has_mem M M

[Mario Carneiro]

In any case, x \in t is just window dressing in this theorem. It may as well be

lemma notnotLEM (p : Prop) : ¬¬ (p ∨ ¬ p):=
  begin
       intro h,
      /-  now what? -/


  end

[Lars Ericson]

Mario, not to be a pain, but can you make your sketch into an #mwe? How do you assume x t when they are not declared?

[Mario Carneiro]

fixed

[Lars Ericson]

So we already have intuitionistic logic by default. Just don't open classical?

[Mario Carneiro]

actually that doesn't do very much besides make it easier to refer to some theorems that you shouldn't use here

[Kevin Buzzard]

It's not as simple as that. Some tactics are classical. Try to find a proof and then at the end #print axioms notnotLEM and check that the output is empty.

[Mario Carneiro]

or at least that it doesn't use classical.choice

[Mario Carneiro]

whether quotient types and/or propext are considered intuitionistic depend on your denomination of intuitionism

[Kevin Buzzard]

I've just done this one. It's the same trick as the not (p and not p) question which comes up on a semi-regular basis. Are there any harder ones? My favourite so far was proving that various things were equivalent to LEM -- there's a list in the Software Foundations book and the question was marked super-hard.

[Mario Carneiro]

I think you mean not (p iff not p)

[Kevin Buzzard]

yeah, my one is much easier isn't it. Shows how little feeling I have for this stuff.

#print axioms notnotLEM -- no axioms

is what you're after Lars.

[Mario Carneiro]

Given that intuitionistic logic actually has an infinite lattice of truth values (even with only one indeterminate), I would think that there are actually long and interesting intuitionistic theorems, but these two examples are the hardest I know and they are pretty easy, objectively speaking

[Kevin Buzzard]

Bottom of https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html is the challenge I remember enjoying as a beginner. My strategy was to knock off four very easy proofs that LEM implied all of them, and then prove LEM from each of them.

[Mario Carneiro]

It's fun to come up with proofs and counterexamples for all the basic logic theorems

[Kevin Buzzard]

lol there are no counterexamples

[Mario Carneiro]

the counterexamples are actually more mindbending than the proofs

[Mario Carneiro]

You need kripke frames

[Kevin Buzzard]

all the theorems are true, you just can't prove them because you're missing some axioms

[Anne Baanen]

If you believe Brouwer, they are real counterexamples.

[Mario Carneiro]

It's a godel completeness kind of situation

[Kevin Buzzard]

Never trust a mathematician who doesn't believe their own theorems

[Mario Carneiro]

you just need more advanced models to capture the intuitionistic theorems instead of the classical ones

[Kevin Buzzard]

oh wait, I started on this whole Lean thing because I was worried about my own theorems...

[Mario Carneiro]

Learning about the models also gives you a better sense for how to predict that a theorem won't be intuitionistically provable

[Mario Carneiro]

for example topological models, where truth values are open sets and negation is the interior of the complement

[Mario Carneiro]

it makes it easy to see why p \/ ~p should not hold

[Kevin Buzzard]

how come nobody from paraconsistent logic ever shows up here? Don't they believe p and not p, or something?

[Kevin Buzzard]

or is it p iff not p

[Mario Carneiro]

Relevance logic is fun, that's a paraconsistent logic that you see sometimes on the FOM mailing list

[Mario Carneiro]

it rejects A -> ~A -> B because B comes "out of nowhere"

[Kevin Buzzard]

I think I'll go back to condensed sets

[Mario Carneiro]

But lean really isn't a playground for arbitrary logics, intuitionistic logic just has a special place here because MLTT is a direct descendent of intuitionism a la brouwer

[Lars Ericson]

Can we please prove that if God possibly exists, then God necessarily exists?

[Mario Carneiro]

in particular lean is also hostile to modal logic

[Mario Carneiro]

(also in that paraphrasing of the argument you forgot the six or so questionable axioms about goodness used in the proof)

[Lars Ericson]

Don't leave temporal logic out. Any kind of logic should be expressible in Lean as a new mathematical structure, it just won't proof automation tuned to that logic. A new logic should be like any other structured like ring or lattice. You just add the axioms for that logic in the structure definition. Am I right?

[Mario Carneiro]

I think there is an isabelle formalization of that argument (or was it a different one?)

[Mario Carneiro]

Sure, lean can do natural numbers so it can represent any logic as a deep embedding. I'm talking about the shallow embedding, where the actual axioms of lean matter

[Mario Carneiro]

In a deep embedding, it doesn't really matter what axioms the meta logic has. PA can model ZFC, ZFC can model HOTT, HOTT can model modal logic, and you can freely mix and match

[Kevin Buzzard]

If I've translated the software foundations exercises correctly, then these four theorems should all be provable constructively:

def lem : Prop := ∀ (P : Prop), P ∨ ¬ P

theorem lem_of_peirce : (∀ P Q : Prop,
  ((P → Q) → P) → P) → lem := sorry

theorem lem_of_double_negation_elimination :
  (∀ P : Prop, ¬¬P → P) → lem := sorry

theorem lem_of_de_morgan_not_and_not :
  (∀ P Q : Prop, ¬(¬P ∧ ¬Q) → P ∨ Q) → lem := sorry

theorem lem_of_implies_to_or :
  (∀ P Q : Prop, (P → Q) → (¬P ∨ Q)) → lem := sorry

[Mario Carneiro]

that's correct (those are all iffs, although the reverse implication is just the classical proof)

[Kevin Buzzard]

Given that it's trivial to show all the things applying LEM are true classically (just check the truth tables), these things are all hence constructively equivalent to LEM.

[Lars Ericson]

These are easy. They all have about the same proof. Am I doing something wrong? I didn't open classical. Is this intuitionist? Or are we missing a lattice and a typeclass of intuitionistic_logic?

import tactic

def lem : Prop := ∀ (P : Prop), P ∨ ¬ P

theorem lem_of_peirce : (∀ P Q : Prop,
  ((P → Q) → P) → P) → lem :=
begin
  intro P,
  intro Q,
  by_cases hQ: Q,
  exact or.inl hQ,
  exact or.inr hQ,
end

theorem lem_of_double_negation_elimination :
  (∀ P : Prop, ¬¬P → P) → lem :=
begin
  intro P1,
  rw lem,
  intro P,
  by_cases hP: P,
  exact or.inl hP,
  exact or.inr hP,
end

theorem lem_of_de_morgan_not_and_not :
  (∀ P Q : Prop, ¬(¬P ∧ ¬Q) → P ∨ Q) → lem :=
begin
  intro P1,
  rw lem,
  intro P,
  by_cases hP: P,
  exact or.inl hP,
  exact or.inr hP,
end

theorem lem_of_implies_to_or :
  (∀ P Q : Prop, (P → Q) → (¬P ∨ Q)) → lem :=
begin
  intro h,
  rw lem,
  intro P,
  by_cases hP: P,
  exact or.inl hP,
  exact or.inr hP,
end

[Lars Ericson]

That is, does the above respond to the original problem, or is it something fancier?

[Yakov Pechersky]

by_cases assumes LEM

[Floris van Doorn]

Lars Ericson said:

That is, does the above respond to the original problem, or is it something fancier?

You can ask Lean this question by writing #print axioms lem_of_peirce. Since it outputs classical.choice, you did use choice in your proof.

[Lars Ericson]

Yes,

#print axioms lem_of_peirce

gives

classical.choice
quot.sound
propext

So is it fair to say that if @Michael Beeson rewrites the above proofs without by_cases, then his original problem is addressed? I.e., no need to define intuitionistic_logic as a structure with lattice-valued propositions or something like that?

[Mario Carneiro]

You just need to prove this theorem using intro, apply, and things like or.inl and or.inr (or left and right), and have if you want. Such a proof will be intuitionistic.

[Mario Carneiro]

also cases and/or and.left and and.right on the one with conjunction

[Mario Carneiro]

I assure you that lattices are not involved

[Mario Carneiro]

Also, you should notice that in your proof you never use any of the assumptions, you are just proving lem outright, which should give you a hint that something is wrong

[Michael Beeson]

Here's an answer to my own question:

lemma notnotLEM: ∀ (P:Prop), ¬¬ (P ∨ ¬ P):=
  assume P,
  begin
    intro h,
    have h2: ¬ P ∧ ¬¬ P:= begin ifinish end,
    ifinish,
  end

In short, ifinish can do this in two steps.

[Mario Carneiro]

Nope, check the axioms

[Mario Carneiro]

#print axioms notnotLEM
-- propext
-- classical.choice
-- quot.sound

yes, ifinish is broken (#1922)

[Michael Beeson]

OK. I have 30,000 lines of Lean code with hundreds of applications of the 'ifinish' tactic to finish off small goals. I knew already
that 'ifinish' will sometimes prove something that is not intuitionistically valid. But what I have now learned is that it also will
prove an intuitionistically valid theorem by a classical proof. That means that my proofs are not intuitionistically valid after all.
Since I am not skilled in meta programming I don't think I'll be able to fix the broken tactic myself. It looks like I will have to
supply a list of basic intuitionistic logic theorems and use them myself by hand to fix all those proofs.

[Mario Carneiro]

The manual proof of this theorem is not difficult, and most theorems are even easier than this one - generally intuitionistically valid theorems will have an "obvious" proof that is intuitionistic

[Mario Carneiro]

in general you should just be using the theorems in logic.basic, which are all intuitionistic where possible and use decidable hypotheses otherwise

[Mario Carneiro]

If you want to know that your theorems are intuitionistic, always use #print axioms because you never know if a tactic snuck one past you (especially if you are using high powered tactics like finish)

[Lars Ericson]

This may sound like a joke, but...are there any software applications whose verification requires intuitionistic logic for physical safety?

If there were, then the matter of strictly being able to control what axioms are available in the namespace would take on more importance. For example, in addition to open classical, you might want to introduce a directive prohibit classical which forces tactics to throw an error if they use LEM or try to open that namespace.

[Eric Wieser]

Probably a @[restrict_axioms [axioms, here]] attribute is the best way to achieve that goal, if it's a goal anyone really has - it can then just do the equivalent of #print axioms and verify that it contains only the provided axioms.

[Mario Carneiro]

are there any software applications whose verification requires intuitionistic logic for physical safety?

It depends on how the logic is interpreted. If it is used to express things that are true and false about the behavior of a program or physical system, then I would say no - classical logic is admissible for such applications. If however there is some other aspect of the logic being invoked, for example the "computability" of the proofs or the inability to make certain kinds of statements a la HoTT, enabling more unusual models that don't literally read the theorems as stated, then these alternate logics can in fact capture something beyond classical logic

[Mario Carneiro]

One way to do it would be a command like #lint that checks all theorems in the current file for intuitionism unless they have @[classical] or some such

[Lars Ericson]

Not strictly analogous but a few examples of connections of logical modelling to real-world:

• Chee Yap's zero project, using real algebraic number arithmetic to never confuse left and right.
• Ed Clarke's temporal logic applied to VLSI design

So what I'm asking, loosely, is if there is a real-world application and rationale for excluding LEM. Or in general why is it an interesting project to exclude LEM. Not being facetious. I just don't honestly know why it's a thing.

[Mario Carneiro]

When I did this a few months ago with the core library, I just grepped for all theorem names in the file and edited a big list of #print axioms at the end

[Mario Carneiro]

Constructivism is a thing

[Mario Carneiro]

you can literally run proofs that don't use choice

[Mario Carneiro]

#reduce will do this in lean

[Mario Carneiro]

That said I'm not going to defend it too hard, it's mostly a puzzle game for me

[Mario Carneiro]

it's interesting to use less axioms when you can

[Mario Carneiro]

However the list of axioms strongly influences the kinds of subsystems you will try to study. In metamath, I did a lot of stuff with avoiding the axiom of choice (obvious) but also the axiom of foundation (turns out it's never needed for anything) and the axiom of replacement (this one is pretty important but you can still do a fair bit). In lean all of that is off the table because we have ZF+U right out the door even with no axioms

[Mario Carneiro]

On the other hand, in metamath (or at least set.mm), the very first axioms are the 3 axioms of classical logic, so intuitionism / no-LEM is not even considered, while in lean that's actually a thing you can try to pursue. (There is however an alternate axiomatization, iset.mm, that I created specifically to investigate intuitionistic and minimal logic, as well as IZF and CZF. Lean doesn't support those kinds of axiomatic investigations.)

[Yakov Pechersky]

On the topic of classical, is it the case that in general, nonempty α is not decidable? Under what constraints is it? I'm trying to see if I can make some variant of src#fintype.subtype_of_fintype lose the noncomputability.

[Mario Carneiro]

It's as decidable as any arbitrary proposition

[Mario Carneiro]

which is to say, not in general

[Mario Carneiro]

specifically, nonempty (plift p) <-> p

[Mario Carneiro]

I think the most appropriate variant on fintype.subtype_of_fintype would be to add a decidable_pred p assumption

[Yakov Pechersky]

How would you modify this then? Or avoid it entirely in the decidable_pred version of fintype.subtype_of_fintype?

noncomputable def of_injective [fintype β] (f : α → β) (H : function.injective f) : fintype α :=
by letI := classical.dec; exact
if hα : nonempty α then by letI := classical.inhabited_of_nonempty hα;
  exact of_surjective (inv_fun f) (inv_fun_surjective H)
else ⟨∅, λ x, (hα ⟨x⟩).elim⟩

[Yakov Pechersky]

Like, adding a [decidable_eq α] and using the inverse from #5872?

[Mario Carneiro]

Probably avoid it entirely. The direct proof is simpler, because you can use univ.filter p as the witness

[Mario Carneiro]

There is an analogue of this for of_injective but the decidability assumption is more complicated

[Lars Ericson]

If you're looking for decision procedures for sublanguages of set theory that you could tuck into Lean, there's a whole cottage industry for that, I linked a few papers here.

The point of my question was not really to question utility of excluding LEM but rather to point out that, if there is a material requirement for that in a program verification system (canonical example: 737MAX autopilot), then the fact that @Michael Beeson has 30,000 lines of proof that he thought were LEM-free but are not would be a significant fail in a real world application. This raises the utility of restrict axioms or similar.

[Mario Carneiro]

Decision procedures? Not really. Most of the interesting subsystems are undecidable. But a collection of theorems proved under minimal assumptions is useful

[Mario Carneiro]

Lean + mathlib is currently not geared toward intuitionistic logic. The base axiom system, dependent type theory, draws on intuitionism, but if you actually care about intuitionistic or constructive mathematics you should use coq instead

[Mario Carneiro]

The user base doesn't care about constructive logic, and as you've already pointed out it's not really needed for applications. There is the notion of noncomputable which is drawn at the (IMO much more useful) distinction of whether lean can generate executable code for the definition

[Kevin Buzzard]

Mario and I are talking about this notnotLEM as if everyone knows how to solve it constructively, but in case anyone this thread is actually hoping someone will post a solution, here's what I came up with:

lemma notnotLEM: ∀ (P:Prop), ¬¬ (P ∨ ¬ P):=
  assume P,
  begin
    intro h,
    have h2: ¬ P,
    { intro hP,
      apply h,
      left,
      assumption },
    apply h,
    right,
    assumption
  end

  #print axioms notnotLEM -- no axioms

The trick is to prove not P first. This is the same trick as the not (P iff not P) puzzle in TPIL. The four problems I posted earlier should also be solvable nonconstructively.

Regarding ifinish, everyone always says "well nobody really uses it and so what's the point fixing it" but could it be the case that there's just a one liner which makes it far more likely to be constructive? ifinish seems to call finish with {classical := ff}. Do people actually understand what the issue is or it is just WONTFIX? Edit: Oh, I see Jeremy looked at this seriously in #1922 . Hmm.

[Mario Carneiro]

there is some discussion about this on the issue

[Mario Carneiro]

some of it was oversight in the implementation but there is also a part that requires C++ changes

[Kevin Buzzard]

"Fixing this leak could be a decent medium-sized project for anyone interested in learning tactic programming."

[Kevin Buzzard]

Perhaps for someone in Michael's situation it might be easier to just write a new tactic, which blunders through some known techniques e.g. uses some simp set consisting of all the constructive lemmas in logic.basic?

[Mario Carneiro]

and the obligatory golfed version:

lemma notnotLEM (P : Prop) : ¬¬(P ∨ ¬ P) := λ h, h (or.inr $ h ∘ or.inl)

[Lars Ericson]

Mario Carneiro said:

Decision procedures? Not really. Most of the interesting subsystems are undecidable. But a collection of theorems proved under minimal assumptions is useful

It depends on the meaning of "interesting", for example "The class of unquantified formulae of set theory involving Boolean operators, the powerset and singleton operators, and the equality and membership predicates is shown to have a solvable satisfiability problem. It is shown that whenever a formula φ in the above class is satisfiable there exists a hereditarily finite model of φ, whose rank is bounded by a doubly exponential expression in the number of variables
occurring in φ. "

So if you are writing procedures like finish and ring and are permitted to embed magic widgets in them that solve certain subsets of expressions, for example the subset described above, then it is at least useful to know

• That there is a fully constructive/programmable decision procedure for that class of expression
• If the expression has more than a few variables in it, it's intractable
• Any other solution you might think of for that class of expressions is equally intractable

[Mario Carneiro]

It depends on the meaning of "interesting"

Put another way, if a theory is decidable then it is uninteresting, because a computer can solve all the problems so there is nothing left for me to do

[Lars Ericson]

Do you not want to use linarith and ring and finish when you can? There's enough heavy lifting to do out there without making trivial things hard when they don't have to be.

[Mario Carneiro]

I don't care for doubly-exponential proofs of anything

[Lars Ericson]

I know 3 people that got tenure just by cranking out papers like that. It's a living.

[Mario Carneiro]

it's nice to know these subsets are decidable in theory but it has very little practical application besides knowing that certain search strategies will terminate

[Eric Wieser]

I may be mistaken, but "decidability" in lean usually refers to the presence of a docs#decidable instance right? So @Mario Carneiro isn't talking about tactics like ring, linarith, and finish?

[Mario Carneiro]

No I mean decidable in the same sense as Lars, i.e. you can prove or disprove all problems in a class. ring is a decision procedure, as is linarith, but finish is a heuristic solving an undecidable problem

[Michael Beeson]

In case anyone cares, what I'm going to do about this is simply to go through my 16 files and manually replace all use of
ifinish with a few lines of code. This is taking about, I would guess, one minute per occurrence, and there were about forty in
the file I'm working on now, so it's a couple of days and then I'm done with it. Also for the record I did not "think these proofs were
LEM-free", I only thought "these proofs ought to be LEM-free". I always knew I needed to "check axioms" when I was done. What
I didn't anticipate is that simple, intuitionistically correct, inferences would get classical proofs via ifinish. Oh well, it's just another speed bump.

[Alex J. Best]

@Michael Beeson some time back @Reid Barton wrote some meta code for you to make this checking quite fast, I'm sure that will be useful here
Reid Barton said:

Here is a super hacky way to print all the axioms used by everything in the current file. Import it and invoke it with #axioms_all. You could grep the output for choice.

import tactic.core

section

open lean lean.parser

@[user_command] meta def axioms_all (_ : interactive.parse $ tk "#axioms_all") : parser unit :=
do e ← get_env,
   e.fold (return ()) (λ d rest, do
     when (e.in_current_file d.to_name)
       (do emit_command_here ("#check " ++ d.to_name.to_string),
           emit_command_here ("#print axioms " ++ d.to_name.to_string),
           return ()),
     rest),
   return ()

end

[Michael Beeson]

I'm using that code. Sometimes it works, sometimes it generates "not enough memory" messages. But I'm just going to
eliminate all uses of 'ifinish' and be done with it.

[Michael Beeson]

simp also produces intuitionistically incorrect results.

lemma foo: ¬¬ ∀ (P:Prop), P ↔ false:=
  begin
    intro h,
    simp at h,
  end

Of course foo is not a correct result--that's irrelevant-- the point is that simp transforms h incorrectly. Since foo is not a theorem
I can't see what #check axioms foo would report.

But one of my actual theorems makes use of simp, and in that proof simp makes an incorrect step.

[Bryan Gin-ge Chen]

That's also to be expected, since simp uses all lemmas marked with the attribute @[simp] and we tag useful lemmas with that attribute regardless of whether they are intuitionistically valid.

As a workaround, you could create a custom simp set using command#mk_simp_attribute that only contains intuitionistic lemmas. You can find some examples of its use in mathlib here.

[Michael Beeson]

Was there a way that I could have discovered that (I mean that simp is possibly not intuitionistic) by reading some piece of documentation? I naively believed that as long as I did not explicitly "turn on" classical logic, I would get only intuitionistic logic. Thanks for pointing me to mk_simp_attribute. That might be useful. I didn't make all that much use of simp so I think I'll just go through and eliminate them.

[Bryan Gin-ge Chen]

Unfortunately, the population of Lean users interested in intuitionistic logic is low (or silent) enough that most of the documentation completely ignores these (valid) concerns. So I would suggest proceeding with the opposite prior: tactics and theorems assume classical logic unless explicitly mentioned otherwise. (That the documentation of ifinish doesn't mention that it's broken is an oversight which we'll hopefully fix soon.)

[Patrick Massot]

Michael Beeson said:

Was there a way that I could have discovered that (I mean that simp is possibly not intuitionistic) by reading some piece of documentation?

The technical answer is yes: the documentation of simp says "simp simplifies the main goal target using lemmas tagged with the attribute [simp]." So, if you are interested in knowing which lemmas are used by simp you need to have a look at lemmas tagged with simp, such as docs#not_not.

But the honest answer is no: I think there is nothing we could write that you would accept to understand and make you come out of your alternate reality. We tried to tell you so many times. mathlib is 470.000 lines of normal mathematics. Each time you load a file from mathlib you're summoning some of those 470.000 lines that will try to prevent you from staying intuitionist. Why are you doing that? Why not creating your own tactics or, much easier, use a tool like the Coq standard library or mathcomp that is designed for the kind of exotic math you're doing? There is nothing wrong with intuitionism, this is simply not what mathlib is doing. Do you complain about the documentation of your car that doesn't mention on every page that you shouldn't use it as a boat?

All that being repeated, I still think we should entirely remove ifinish from mathlib. There is no point at all in keeping a tactic that is known to be so broken. I'll try to convince the other maintainers and I really apologize for the inconvenience.

[Eric Wieser]

Presumably it would be an entry-level tactic project to write a new isimp that only used simp lemmas that don't rely on choice? Obviously mathlib wouldn't use it much, but it would at least make it more viable for those looking for intuitionistic logic.

[Chris Hughes]

I think there's no easy way to check the axioms used by a declaration in meta land.

[Eric Wieser]

Oh, I didn't look at the code above for collecting axioms - indeed, it just uses emit_command_here "#print axioms". Can meta-land code capture the output of emit_command_here?

[Sebastien Gouezel]

Since mathlib is by design classical, I wouldn't see the point. A library building something seriously intuitionistic in Lean should probably be something different from mathlib.

[Eric Wieser]

It seems a shame to throw out all of mathlib when intuitionistic users object to only parts of it. I wonder what fraction of our ~50k theorems use choice. Even if it's 90%, getting a 5k theorem head-start still seems like an argument to build an intuitionistic library on top of mathlib rather than from scratch.

[Sebastien Gouezel]

A clear-cut choice seems much better from my point of view, as otherwise some people will get some expectations, and then they will be disappointed when they realize these expectations can not be met with mathlib. (This is a situation we can already see!)

[Patrick Massot]

Indeed there is no need for a thought experiment here: we know what happens when people try to use mathlib for intuitionistic maths.

[Patrick Massot]

See also #5897.

[Kevin Buzzard]

Regarding the other point Michael made, about simp -- are there any non-intuitionistic simp lemmas in core Lean 3? I ask because a proposal crystallising here is "if you want to be 100% sure you are intuitionistic in lean then do not import any mathlib modules", which sounds fair enough to me as we have made no attempt whatsoever to correctly document which tactics are intuitionistic (cf broken claims about ifinish which nobody has even bothered to fix). However if there is a single non-intuitionistic simp lemma in core then one interpretation of this is that actually lean 3 is not safe to use at all if you want to be sure you are intuitionistic. This would be a shame for Michael and others who want to use Lean in this way. Of course the converse argument is that one reason for the terrifying growth of mathlib is precisely because we are not held back by issues involving constructivism -- the deep-rooted classical foundations of mathlib have attracted more number theorists, geometers, analysts etc than the other systems.

Of course there is also the other attitude, which given Michael's situation is probably the more pragmatic one, that he simply continues to use lean as he is doing and constantly runs #print axioms to make sure he is not selling his soul to Hilbert.

[Mario Carneiro]

"if you want to be 100% sure you are intuitionistic in lean then do not import any mathlib modules"

If you want to be 100% sure you are intuitionistic in lean, a necessary and sufficient condition is to run #print axioms

[Mario Carneiro]

it's completely possible to do this while still using mathlib, and it's also possible to screw up when using core lean

[Mario Carneiro]

There is a decent amount of intuitionistic maths in mathlib, it just isn't marked in any way, you need #print axioms to see it

[Eric Wieser]

It probably wouldn't be too hard to indicate it in docgen, if somehow can show me how to get the result of #print axioms in meta code

[Mario Carneiro]

I'm not saying this is something we need to change

[Mario Carneiro]

It means that we can still have a decent intuitionistic coverage without getting in the way of the 99% of users who don't want to be bothered about it

[Mario Carneiro]

That said, pre-running #print axioms and displaying it in docgen is generally a good idea, that's been a selling point of the metamath web pages since the beginning

[Eric Wieser]

In principle this is useful to anyone who uses the axiom keyword (and uses doc-gen), not just intuitionist users

[Mario Carneiro]

well, axiom is more or less banned in mathlib, and docgen only works on mathlib AFAIK

[Eric Wieser]

I made docgen work on my own project with only a few lines of hacks in a shell script: https://github.com/pygae/lean-ga/blob/3027ba22a5698d0d2a9e4f497399a55027704aa9/.github/workflows/lean_doc.yml#L71-L73

[Mario Carneiro]

In third party projects I can definitely see the use, it means that people can see whether you've used extra axioms in your big theorem without having to boot up lean

[Lars Ericson]

How hard would it be to put a # directive in Lean which causes any proof to fail which uses a specific axiom, so

#prohibit classical.choice

This seems like an easy hack. Then it wouldn't matter if a use was buried, the proof would just fail when it got to that use, and then you could rework the proof. You wouldn't have to introspect so much on what is buried in the tactics and pre-existing proofs.

An alternate approach would be to axiomatize multiple logics and try to factor out more the underlying axiomatic system. For example, you could have system I (intuitionist), system C (classical) and system Q (whatever that is) and modal logics and temporal logics and so on. I would have thought that could just be done inside the class mechanism. However I guess there is some meta glue surrounding the process of proof checking such that the system of logic used is somewhat hard-wired. Is Lean 4 more flexible in this regard?

[Mario Carneiro]

Like I said, lean isn't cut out for this. It's not a logical foundation; the baseline axioms are already way stronger than most systems logicians care to study

[Mario Carneiro]

Lean 4 is actually less flexible in this regard

[Patrick Massot]

Shouldn't we have a new documentation page and a new Zulip magic url so that you can stop repeating all this over and over? I'm pretty sure you could enjoy doing something else.

[Mario Carneiro]

Lean 2 seriously entertained the possibility of alternate "settings" for the foundations, such as HoTT; lean 3 has a few vestigial remnants of this but is basically just one specific DTT foundation; and lean 4 is doubling down on this approach because mathlib has made the interest in this approach even less attractive

[Kevin Buzzard]

Will this scare off the computer scientists? Or are they expected to just #print axioms?

[Kevin Buzzard]

Maybe they actually run code or something? So I guess they notice then

[Mario Carneiro]

I'm not sure most computer scientists care about intuitionism

[Mario Carneiro]

Certainly the kind of mathematics you see in algorithms classes is completely classical

[Mario Carneiro]

it's just this one type theory offshoot community that cares about MLTT and its extensions that latch on to this particular notion of intuitionism

[Eric Wieser]

Am I right in thinking that one motivation behind "running proofs" is that you can extract a witness of existentials computably?

lemma foo : ∃ x, x*x = 4 := ⟨2, by norm_num⟩

#reduce foo  -- prints a term which involves `2`

Is there a way of doing this without either classical or #reduce, to get the result in a def?

[Mario Carneiro]

Yeah, just use {x // x*x = 4} instead

[Mario Carneiro]

basically in lean you decide upfront whether you care about the witness or not

[Eric Wieser]

Yeah, I understand that's a bad way to write it, I'm just asking out of curiousity.
I assume then there's no builtin computable get_witness h that requires h to be constructively proven?

[Eric Wieser]

I guess that would violate proof irrelevance

[Mario Carneiro]

No, I'm answering your question

[Mario Carneiro]

If you want to get the value without classical or #reduce, you make the lemma data-carrying by using subtype in place of Exists

[Eric Wieser]

Yeah, that was the model I already had in my head

[Mario Carneiro]

get_witness would be inconsistent

[Mario Carneiro]

that's basically classical.choice but it doesn't have the properties of a function

[Mario Carneiro]

constant get_witness {α} (p : α → Prop) : (∃ x, p x) → α
axiom get_witness_ex {α} (p : α → Prop) (x) (h : p x) : get_witness p ⟨x, h⟩ = x

example : false :=
begin
  have h1 := get_witness_ex (λ x, true) tt trivial,
  have h2 := get_witness_ex (λ x, true) ff trivial,
  exact bool.ff_ne_tt (h2.symm.trans h1)
end

[Eric Wieser]

I was thinking something like docs#quotient.unquot could exist, which works only in the vm

[Mario Carneiro]

Yeah, what I wrote could be implemented computably in the same way as quotient.unquot, although it would require propositions to carry data in the VM

[Mario Carneiro]

however it's inconsistent

[Mario Carneiro]

just like quotient.unquot

[Mario Carneiro]

The way compilation works, a proof of exists x, p x is represented as (), i.e. nothing at all, meaning that a get_witness function in the VM would have nowhere to get the data

[Eric Wieser]

So in a sense, the way to do constructive logic safely in lean is to use trunc (subtype p) (docs#trunc) instead of Exists p, and something similar for disjunctions? Then you know your proofs are intuitionist because if they weren't you'd need noncomputable?

[Reid Barton]

I think it's seriously difficult to build a good formalized math library which supports both classical and constructive logic well; more difficult than just writing two independent libraries.

[Lars Ericson]

If it's a single offending axiom (LEM), I don't get from this discussion why you can't just add a flag to throw an error when that axiom is invoked. This is a simple solution, why wouldn't it be adequate? The main complaint here is that classical.choice was invoked inadvertently. It seems easy to flag, and doesn't require a large rethink of the design.

[Mario Carneiro]

Well the obvious way to get an error on all uses of an axiom is to delete the axiom

[Mario Carneiro]

if you completely don't want it then it shouldn't be in the environment

[Yakov Pechersky]

@Lars Ericson How do you know if you've touched that "one axiom"? It's not always clear that it's invoked. For reference, there was this cool thread https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/classical.2Eem.20without.20funext.20.2F.20quot.2Esound
where there are many ways to prove em.

[Lars Ericson]

@Yakov Pechersky , the advice so far has been to #print axioms notnotLEM and if it doesn't print classical.choice, then you're blessed as intuitionist. So either that advice is wrong, or there is a fairly simple mechanism (whatever function/store accumulates results for #print axioms to inspect) which you can stick an exception/breakpoint into whenever it tries to add classical.choice to it's store.

Or the advice is wrong. But the claim above is that you know you've touched that one axiom classical.choice based on the #print.

I'm assuming here also that for the proof checking mechanism, there is a list of axioms which is explicitly declared in the same sense that we declare properties in type classes. If it's not so explicit, i.e. if it's a bunch of C++ code under the hood that encodes the axioms by hand, then that's a different story.

[Mario Carneiro]

whatever function/store accumulates results for #print axioms to inspect

There is no such store. When you use #print axioms it traverses the entire proof, and the entire proof of all referenced theorems and so on recursively, until it finds uses of axiom constants.

[Mario Carneiro]

I'm assuming here also that for the proof checking mechanism, there is a list of axioms which is explicitly declared in the same sense that we declare properties in type classes. If it's not so explicit, i.e. if it's a bunch of C++ code under the hood that encodes the axioms by hand, then that's a different story.

Lean actually has both kinds of axiom. The kind that #print axioms picks up are those that were introduced with actual axiom invocations in the source. But there are other constants like nat.rec and quot.mk and definitional equality axioms like proof irrelevance and a countable hierarchy of universes that are built in to the C++, cannot be turned off, and do not show up in #print axioms. These are the "no axioms" axioms, and it's impossible to meaningfully do proofs with a subset of these axioms.

[Lars Ericson]

Be that all as it may, if the project were to implement system Q as a class and prove theorems either in or about Q, without straying from the bounds of Q, is that doable in Lean?

In other words, just as much as a topology or a lattice is a mathematical structure, something like Q is a mathematical structure, so what are the limits to reasoning about or in Q versus say the limits of reasoning about a topology or lattice?

I hope the question isn't too fuzzy, it's a bit fuzzy in my mind, but you get the idea.

[Kyle Miller]

A model I've had in mind, but I'm not sure how accurate it is, is that if you want to be as constructive as possible then you should avoid Prop entirely. Is this more or less a reasonable model?

Something I've never been quite sure about with intuitionism is what the scope is of what needs to be constructible. At a basic level, you can give a computation for an object and in that sense the object exists, but is it generally accepted that every aspect of the proof that this is the right object needs to be constructible as well? or is that a more of an extreme position?

I like Lean's pragmatic approach where so long as a definition isn't noncomputable then that implies there's a construction. It just might use not-incorrect inferences along the way. I guess it seems meaningful to me having computable definitions (even if I'm never going to evaluate them), but avoiding choice in proofs seems more like a curiosity unless reverse mathematics is your specialty.

[Michael Beeson]

Just for the record, my files do not import mathlib and I knew that I could not expect mathlib to be intuitionistic.
I only have import tactic.basic. I had a mistaken idea about the behavior of those tactics. I did not intend to be
"complaining" (especially not that "my car is not a boat"); I'm grateful that Lean exists and I'm appreciative of the
work that has been done on it. When I asked if there was something I could/should have read to avoid my mistaken idea,
I did not mean to complain, I just wanted to know if these things are written down somewhere. The last thing I intended
was to annoy anyone. Thanks to all of you who have considered this issue.

[Lars Ericson]

We should keep an open mind.
BN-KK363_0922my_M_20150921164148.jpg

[Michael Beeson]

OK, I still want to make sure my proofs are intuitionistic. I seem to have two options.

1. continue to import tactic.basic, but avoid simp, simp_rw, and ifinish, and check which axioms are used to make sure classical choice isn't.

2. remove import tactic.basic from all my files.

Questions:
Q1: with option 2 is it correct that my proofs will all pass through an intuitionistic kernel and it won't be necessary to "check axioms"?
And, if that is the case,

Q2: I will still need to eliminate the need for tactic 'use' to call exists.intro from tactic mode and leave a goal still to solve, since
'use' is defined in tactic.basic.

Is that easy or hard?

and
Q3: with option 1, i.e. check axioms, how airtight is the guarantee that the proof is intuitionistically correct? I guess it does not quite
have the certainty of passing through the kernel? I am intending to publish a proof, and naturally I wish to be CERTAIN that it is
correct--that is why I am using Lean in the first place.

[Kevin Buzzard]

I think that the conclusion of the discussion above is that 2. is not going to solve your problems. LEM is defined as an axiom in core Lean, and this axiom cannot be overridden or removed. Having thought about this over the last few days, I personally think that the easiest path is simple: import tactic.basic, import what the heck you like. You can't make LEM go away, and nobody is able to guarantee that it won't randomly appear when you use a tactic like simp or even, unfortunately, ifinish. However I believe we _can_ guarantee that #print axioms will report on usage of nonintuitionistic things if it finds them. Apparently it's difficult to even get Lean to automatically check that no axioms are used automatically. But this kind of question can be solved. So in fact my instinct would be to continue to use both mathlib and the dubious tactics, and just keep checking that your proofs are intuitionistic. If they're not, then rewrite until they are.

[Eric Wieser]

And be aware that the fact your proofs are intuitionistic today will not guarantee that they still are after updating lean / mathlib, as the simp set may have changed

[Kevin Buzzard]

I know that Patrick was keen on just nuking ifinish, because it is dishonest to have a tactic which claims to do something that it does not do, and the user has to explicitly check that it did its job every time. Is there an example known where finish produces a non-intuitionistic proof and ifinishproduces an axiom-free one?

[Reid Barton]

Is it possible to create itheorem which will error if the proof uses axioms?

[Mario Carneiro]

itheorem is hard because it is a def-variant command, which means that you have to replicate all the parsing stuff that def does

[Mario Carneiro]

Maybe an attribute can do something similar though

[Michael Beeson]

Here is a small MWE on which checking axioms produces output I cannot interpret. What is going on here? Is there an
error in my Lean code? The example
begins with "import barton". The contents of barton.lean will be pasted in below.

import barton
reserve infix ` ∈ ` : 49

class  Model (M:Type) :=
(mem : M → M → Prop)
(infix  ∈ :=  mem )
(union: M → M)
(union_axiom:   ∀ (x y:M), (x ∈ union y ↔ ∃ (z:M), (z ∈ y ∧ x ∈ z)))
 /- end of class definition because next line doesn't declare a member -/

 #axioms_all

Here is barton.lean

import tactic.core

section

open lean lean.parser

@[user_command] meta def axioms_all (_ : interactive.parse $ tk "#axioms_all") : parser unit :=
do e ← get_env,
   e.fold (return ()) (λ d rest, do
     when (e.in_current_file d.to_name)
       (do emit_command_here ("#check " ++ d.to_name.to_string),
           emit_command_here ("#print axioms " ++ d.to_name.to_string),
           return ()),
     rest),
   return ()

end

[Kevin Buzzard]

Does putting a full stop after the definition of the class help?

[Michael Beeson]

No, output does not change with a full stop.

[Eric Wieser]

What is the output?

[Mario Carneiro]

I get four infos and an error on the #axioms_all line:

info:
Model.cases_on :
  Π (n : Model ?M_1),
    (Π (mem : ?M_1 → ?M_1 → Prop) (union : ?M_1 → ?M_1)
     (union_axiom : ∀ (x y : ?M_1), mem x (union y) ↔ ∃ (z : ?M_1), mem z y ∧ mem x z),
       ?M_2 {mem := mem, union := union, union_axiom := union_axiom}) →
    ?M_2 n

info:
no axioms

info:
Model.union_axiom : ∀ (x y : ?M_1), Model.mem x (Model.union y) ↔ ∃ (z : ?M_1), Model.mem z y ∧ Model.mem x z

info:
no axioms

error:
invalid 'Model.no_confusion' application, elaborator has special support for no_confusion
but the expected type must be known

[Eric Wieser]

I guess it emits #check Model.no_confusion, which isn't a valid application

[Mario Carneiro]

right, you need

           emit_command_here ("#check @" ++ d.to_name.to_string),

[Eric Wieser]

While we're on this topic, does #check @@f ever give a different result to #check @f?

[Eric Wieser]

Answer: yes, @@mul_assoc is an example

[Mario Carneiro]

also @@list.rec

[Eric Wieser]

Perhaps @@ is actually a good idea here to avoid noise while avoiding the error caused by no @?

[Mario Carneiro]

No, I think it's best to avoid metavariable insertion since that could cause unexpected elaboration errors

[Mario Carneiro]

You could use #print decl instead but that shows the whole function definition too

[Mario Carneiro]

probably just trace decl is sufficient

[Mario Carneiro]

or rather emit_command_here ("#eval tactic.trace `" ++ d.to_name.to_string) since otherwise it isn't sequenced properly with the #print axioms

[Michael Beeson]

Thank you Mario, once again you have made my day. One little @ sign seems to get rid of the red ink.

[Mario Carneiro]

Here's another version of that command with these adjustments:

@[user_command] meta def axioms_all (_ : interactive.parse $ tk "#axioms_all") : parser unit :=
do info ← option.is_some <$> optional (tk "?"),
  e ← get_env,
  e.fold (return ()) (λ d rest, do
    when (e.in_current_file d.to_name) (do
      when info $ emit_command_here ("#eval tactic.trace `" ++ d.to_name.to_string) $> (),
      emit_command_here ("#print axioms " ++ d.to_name.to_string) $> ()),
    rest)

[Mario Carneiro]

You can use #axioms_all and it will not print the names of things, but it should be easy to scan for the odd one out in a sea of no axioms. If you use #axioms_all? it will print the names of declarations so you can go find the offender

[Mario Carneiro]

Unfortunately #print axioms does not provide its information via tactics so it still requires some eyeball work

[Eric Wieser]

Is there no way to run a command and capture the trace messages?

[Mario Carneiro]

not that I know of

[Mario Carneiro]

It shouldn't be hard to make a hook for this in lean C++

[Eric Wieser]

Can you do something dumb like vm_override trace?

[Mario Carneiro]

#print axioms is a bit of an unusual case because it predates a lot of the tactic framework. It just writes straight to the editor, lean never sees anything

[Mario Carneiro]

trace isn't called, this is 100% C++ code

[Mario Carneiro]

the hook I'm referring to is something like constant tactic.get_axioms_used : name -> tactic (list name)

[Michael Beeson]

#axioms_all? (with question mark) produces great output, I'm happy with that.
Without the question mark it just prints "no axioms" or "propext" or occasionally "quot.sound"; so I guess
if I do not say any occurrence of "choice" I'm good to go without a question mark. The plan is to do leanproject build and
grep the output for "choice".

[Mario Carneiro]

yeah, that's the idea

[Michael Beeson]

That was working fine before you improved the code, except on the file containing the class definition. Now that works too, thanks.

[Mario Carneiro]

I suppose with the other version you might get in trouble if you happen to have a declaration called choice something

[Michael Beeson]

I don't have any such declaration so that's not a problem.

[Michael Beeson]

I wonder why quot.sound pops up now and then. I don't have any explicit quotient types.

[Mario Carneiro]

If you use funext then quot.sound will get involved

[Mario Carneiro]

meta def environment.is_builtin (env : environment) (n : name) : bool :=
env.is_inductive n || env.is_recursor n || env.is_constructor n ||
to_bool (n ∈ [``quot, ``quot.lift, ``quot.ind, ``quot.mk])

meta def tactic.get_axioms_used_aux (env : environment) : name →
  list name × name_set → tactic (list name × name_set)
| n p@(l, ns) := if ns.contains n then pure p else do
  d ← env.get n,
  let ns := ns.insert n,
  let process (v : expr) : tactic (list name × name_set) := (do
    v.fold (pure (l, ns)) $ λ e _ r, r >>= λ p,
      if e.is_constant then tactic.get_axioms_used_aux e.const_name p else pure p),
  match d with
  | (declaration.defn _ _ _ v _ _) := process v
  | (declaration.thm _ _ _ v)      := process v.get
  | _ := pure $ if env.is_builtin n then (l, ns) else (n::l, ns)
  end

meta def tactic.get_axioms_used (n : name) : tactic (list name) :=
do env ← tactic.get_env,
  prod.fst <$> tactic.get_axioms_used_aux env n ([], mk_name_set)

#eval tactic.get_axioms_used `classical.em >>= tactic.trace
-- [propext, quot.sound, classical.choice]

[Mario Carneiro]

@[user_attribute]
meta def intuit_attr : user_attribute unit unit :=
{ name   := `intuit,
  descr  := "intuit",
  after_set := some $ λ n _ _, do
    l ← tactic.get_axioms_used n,
    guard (``classical.choice ∉ l) <|>
    tactic.fail "ERROR: classical axioms used" }

@[intuit] theorem bad (p) : ¬ (p ↔ ¬ p) := -- fail
by by_cases p; simp

@[intuit] theorem good (p) : ¬ (p ↔ ¬ p) := -- ok
λ h, have ¬ p, from λ i, h.1 i i, this (h.2 this)

[Eric Wieser]

I'm not sure about the attribute, but those meta defs look worth PRing to me

[Michael Beeson]

If I understand this correctly, here is how I should use it: import the code and then tag all my theorems with @[intuit].
Is that right?

[Michael Beeson]

Here's a MWE. In this case it is really a working example, instead of a non-working example. My question is this: I first wrote it with
[M:Type] instead of {M:Type}. It didn't work. But this version, with {M}, does work. Is anybody willing to explain why? I suppose if I studied the documentation hard enough it would explain the difference between curly brackets and braces, so I'm hesitant to post, but maybe somebody can tell me easily. Also: would there be a way to write it so the final 'simp' to cause beta-reduction would be already applied?

lemma notnot_forall{M:Type}: ∀ (P: M → Prop), (¬¬ ∀ (x:M), P x) → ∀ (x:M), ¬¬ P x:=
  -- credit: Troestra 344, p. 8
  assume P,
  begin
    intros h t,
    intro h2,
    have h3:  ¬ ∀ (x:M), P x:=
      begin
        intro h4,
        specialize h4 t,
        contradiction,
      end,
   contradiction,
 end

reserve infix ` ∈ ` : 49

class  Model (M:Type) :=
(mem : M → M → Prop)
(infix  ∈ :=  mem )
(union: M → M)
(union_axiom:   ∀ (x y:M), (x ∈ union y ↔ ∃ (z:M), (z ∈ y ∧ x ∈ z))).
 /- end of class definition because next line doesn't declare a member -/

variables (M:Type) [Model M] (a b x y z u v w X R W: M)
open Model

lemma test: (¬¬ ∀ (x:M), x = x) → ∀ (x:M), x = x :=
  begin
    have h:= notnot_forall (λ (x:M), x = x),
    simp,
  end

[Mario Carneiro]

square brackets are only for typeclass arguments

[Mario Carneiro]

Usually type arguments will be in curly braces like {M : Type}, because they are not going to be supplied explicitly in lemmas

[Mario Carneiro]

Since all the variables in your variables line are explicit except for [Model M], that means that if you use test you will have to write test M h x to apply it (where h is a proof of ¬¬ ∀ (x:M), x = x, even though lean can infer M from h

[Michael Beeson]

Yes, I always supply M explicitly. If I don't type the variables in my lemmas then Lean often complains that it cannot synthesize their types so I just got in the habit of typing everything.

[Mario Carneiro]

For the variables like a b x y this is reasonable, but for type variables it's pretty rare that they can't be inferred

[Mario Carneiro]

If you use (M) instead of {M} in notnot_forall, in test you can write have h := notnot_forall _ (λ (x:M), x = x), but have h := notnot_forall (λ (x:M), x = x), won't work. If you use [M:Type], then it will attempt to use typeclass inference to infer M, which will fail because Type is not a typeclass

[Mario Carneiro]

The standard rule we use in mathlib is that if a variable appears in the types of arguments that come later, then it should be implicit, otherwise it should be explicit

[Mario Carneiro]

so if you have lemma foo (M : Type) (a : M) (h : a = a) then you could make M and a implicit because h contains a in its type and a contains M in its type

[Michael Beeson]

because the elaborator will be able to pick up the type from the later occurrences? having temporarily substituted a metavariable that it will then fill in when it encounters the correct type?

[Mario Carneiro]

right, when you apply it with say a being 3 : nat it can figure out that M := nat

[Michael Beeson]

Except your example would hit the infamous "a" bug, as it uses "a" for that metavariable, if I understand things.

[Mario Carneiro]

if you just wrote foo rfl it would have trouble though because rfl doesn't follow this rule of implicitness, it has all arguments implicit. With foo (eq.refl (3:nat)) or foo (rfl : 3 = 3) it would work

[Mario Carneiro]

Nah, the a bug is dead and gone

[Mario Carneiro]

long live the alpha-vrachy ᾰ bug

[Michael Beeson]

OK!

[Michael Beeson]

How come if I write (M) I can get away with an underscore? I don't know how that works.

[Michael Beeson]

Also: simp often uses classical choice. How can I cause beta-reduction and ONLY beta-reduction? Similar to #reduce, but in a tactic. 'simp only' works at least sometimes, maybe that is the answer.

[Yakov Pechersky]

dsimp only

[Michael Beeson]

Looking at the manual for dsimp, it looks like the "only" after dsimp would be superfluous. Or maybe not. Anyway thanks, I did not know about dsimp, even though it is right there in the manual.

[Mario Carneiro]

dsimp without only means dsimp with all definitional simp lemmas

[Mario Carneiro]

those lemmas can't use axioms so it's safe in your case, but it's more than just beta reduction

[Mario Carneiro]

How come if I write (M) I can get away with an underscore? I don't know how that works.

For the same reason that {M} works. Lean can infer it if you ask it to; you can either signal this on the definition of the function itself using {M}, in which case lean will insert the underscore unless you ask it not to, or you can do it at point of use if the function uses (M) but you have an actual _ at the application

[Michael Beeson]

I did leanproject update. Now I wish I had not, as it seems that the "broken" tactic 'finish' has been removed. But I was still using it.
Many times it DOES produce an intuitionistically correct proof. I guess now I will really have to eliminate ALL use of it. Unless there is an
easy way to revert to the previous version?

[Yury G. Kudryashov]

You can take the one-line definitions of ifinish etc from old mathlib and copy to your project.

[Michael Beeson]

I tried

open tactic expr
namespace auto

meta def ifinish (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto_config := {}) : tactic unit :=
  finish s ps {classical := ff, ..cfg}
end auto

But it produced

invalid structure value { ... }, 'classical' is not a field of structure 'auto.auto_conf

[Bryan Gin-ge Chen]

There were some other changes made to finish in that commit, so the easiest thing to do might just be to copy the entire file from the commit before and rename some of the declarations in it https://github.com/leanprover-community/mathlib/blob/c64aa1327ea3ce07673e98f9a1a33097ad377019/src/tactic/finish.lean

It looks like there's also one fix to normalize_hyp you'll have to port from the Lean 3.26.0 upgrade: https://github.com/leanprover-community/mathlib/commit/c64aa1327ea3ce07673e98f9a1a33097ad377019#diff-a0d8d6b754a5f49a85e923e6ca891150d76bd8d1e7f66f395db8a81af79f1b09

[Bryan Gin-ge Chen]

Maybe it'd be easier to rename the auto namespace rather than all of the individual declarations in it.

[Michael Beeson]

I've just gone through all my files and replaced all calls to ifinish with explicit proofs. It was kinda sorta fun and now it's done, so I can keep using the current version.