Zulip Chat Archive

Stream: new members

Topic: intuitionistic logic


Michael Beeson (Jan 25 2021 at 05:48):

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 (Jan 25 2021 at 05:58):

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 (Jan 25 2021 at 08:03):

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 (Jan 25 2021 at 14:35):

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 (Jan 25 2021 at 14:44):

@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 (Jan 25 2021 at 14:58):

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 (Jan 25 2021 at 15:00):

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 (Jan 25 2021 at 15:02):

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 (Jan 25 2021 at 15:07):

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 (Jan 25 2021 at 15:07):

fixed

Lars Ericson (Jan 25 2021 at 15:08):

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

Mario Carneiro (Jan 25 2021 at 15:09):

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

Kevin Buzzard (Jan 25 2021 at 15:09):

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 (Jan 25 2021 at 15:09):

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

Mario Carneiro (Jan 25 2021 at 15:10):

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

Kevin Buzzard (Jan 25 2021 at 15:12):

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 (Jan 25 2021 at 15:12):

I think you mean not (p iff not p)

Kevin Buzzard (Jan 25 2021 at 15:13):

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 (Jan 25 2021 at 15:15):

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 (Jan 25 2021 at 15:15):

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 (Jan 25 2021 at 15:15):

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

Kevin Buzzard (Jan 25 2021 at 15:16):

lol there are no counterexamples

Mario Carneiro (Jan 25 2021 at 15:16):

the counterexamples are actually more mindbending than the proofs

Mario Carneiro (Jan 25 2021 at 15:16):

You need kripke frames

Kevin Buzzard (Jan 25 2021 at 15:16):

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

Anne Baanen (Jan 25 2021 at 15:16):

If you believe Brouwer, they are real counterexamples.

Mario Carneiro (Jan 25 2021 at 15:16):

It's a godel completeness kind of situation

Kevin Buzzard (Jan 25 2021 at 15:17):

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

Mario Carneiro (Jan 25 2021 at 15:17):

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

Kevin Buzzard (Jan 25 2021 at 15:17):

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

Mario Carneiro (Jan 25 2021 at 15:18):

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

Mario Carneiro (Jan 25 2021 at 15:18):

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

Mario Carneiro (Jan 25 2021 at 15:19):

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

Kevin Buzzard (Jan 25 2021 at 15:19):

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

Kevin Buzzard (Jan 25 2021 at 15:20):

or is it p iff not p

Mario Carneiro (Jan 25 2021 at 15:20):

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

Mario Carneiro (Jan 25 2021 at 15:20):

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

Kevin Buzzard (Jan 25 2021 at 15:21):

I think I'll go back to condensed sets

Mario Carneiro (Jan 25 2021 at 15:23):

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 (Jan 25 2021 at 15:23):

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

Mario Carneiro (Jan 25 2021 at 15:24):

in particular lean is also hostile to modal logic

Mario Carneiro (Jan 25 2021 at 15:25):

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

Lars Ericson (Jan 25 2021 at 15:26):

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 (Jan 25 2021 at 15:26):

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

Mario Carneiro (Jan 25 2021 at 15:27):

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 (Jan 25 2021 at 15:29):

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 (Jan 25 2021 at 15:29):

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 (Jan 25 2021 at 15:30):

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

Kevin Buzzard (Jan 25 2021 at 15:30):

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 (Jan 25 2021 at 15:56):

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 (Jan 25 2021 at 15:57):

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

Yakov Pechersky (Jan 25 2021 at 15:59):

by_cases assumes LEM

Floris van Doorn (Jan 25 2021 at 16:09):

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 (Jan 25 2021 at 16:12):

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 (Jan 25 2021 at 16:14):

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 (Jan 25 2021 at 16:15):

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

Mario Carneiro (Jan 25 2021 at 16:15):

I assure you that lattices are not involved

Mario Carneiro (Jan 25 2021 at 16:17):

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 (Jan 25 2021 at 16:36):

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 (Jan 25 2021 at 16:37):

Nope, check the axioms

Mario Carneiro (Jan 25 2021 at 16:38):

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

yes, ifinish is broken (#1922)

Michael Beeson (Jan 25 2021 at 17:02):

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 (Jan 25 2021 at 17:11):

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 (Jan 25 2021 at 17:12):

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 (Jan 25 2021 at 17:14):

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 (Jan 25 2021 at 17:17):

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 (Jan 25 2021 at 17:19):

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 (Jan 25 2021 at 17:21):

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 (Jan 25 2021 at 17:23):

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 (Jan 25 2021 at 17:24):

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

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 (Jan 25 2021 at 17:24):

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 (Jan 25 2021 at 17:24):

Constructivism is a thing

Mario Carneiro (Jan 25 2021 at 17:25):

you can literally run proofs that don't use choice

Mario Carneiro (Jan 25 2021 at 17:25):

#reduce will do this in lean

Mario Carneiro (Jan 25 2021 at 17:26):

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

Mario Carneiro (Jan 25 2021 at 17:27):

it's interesting to use less axioms when you can

Mario Carneiro (Jan 25 2021 at 17:29):

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 (Jan 25 2021 at 17:34):

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 (Jan 25 2021 at 17:35):

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 (Jan 25 2021 at 17:36):

It's as decidable as any arbitrary proposition

Mario Carneiro (Jan 25 2021 at 17:36):

which is to say, not in general

Mario Carneiro (Jan 25 2021 at 17:36):

specifically, nonempty (plift p) <-> p

Mario Carneiro (Jan 25 2021 at 17:38):

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

Yakov Pechersky (Jan 25 2021 at 17:42):

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  : nonempty α then by letI := classical.inhabited_of_nonempty ;
  exact of_surjective (inv_fun f) (inv_fun_surjective H)
else , λ x, ( x⟩).elim

Yakov Pechersky (Jan 25 2021 at 17:42):

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

Mario Carneiro (Jan 25 2021 at 17:46):

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

Mario Carneiro (Jan 25 2021 at 17:46):

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

Lars Ericson (Jan 25 2021 at 17:47):

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 (Jan 25 2021 at 17:48):

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

Mario Carneiro (Jan 25 2021 at 17:50):

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 (Jan 25 2021 at 17:51):

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 (Jan 25 2021 at 18:20):

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 (Jan 25 2021 at 18:21):

there is some discussion about this on the issue

Mario Carneiro (Jan 25 2021 at 18:21):

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

Kevin Buzzard (Jan 25 2021 at 18:22):

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

Kevin Buzzard (Jan 25 2021 at 18:24):

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 (Jan 25 2021 at 18:25):

and the obligatory golfed version:

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

Lars Ericson (Jan 25 2021 at 18:25):

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 (Jan 25 2021 at 18:26):

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 (Jan 25 2021 at 18:27):

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 (Jan 25 2021 at 18:28):

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

Lars Ericson (Jan 25 2021 at 18:28):

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

Mario Carneiro (Jan 25 2021 at 18:29):

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 (Jan 25 2021 at 18:29):

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 (Jan 25 2021 at 18:30):

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 (Jan 25 2021 at 21:17):

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 (Jan 25 2021 at 21:22):

@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 (Jan 26 2021 at 02:06):

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 (Jan 26 2021 at 04:26):

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 (Jan 26 2021 at 04:48):

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 (Jan 26 2021 at 04:49):

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 (Jan 26 2021 at 06:19):

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 (Jan 26 2021 at 09:15):

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 (Jan 26 2021 at 11:04):

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 (Jan 26 2021 at 11:11):

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

Eric Wieser (Jan 26 2021 at 11:14):

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 (Jan 26 2021 at 11:15):

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 (Jan 26 2021 at 11:19):

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 (Jan 26 2021 at 11:25):

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 (Jan 26 2021 at 11:28):

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 (Jan 26 2021 at 11:33):

See also #5897.

Kevin Buzzard (Jan 26 2021 at 12:37):

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 (Jan 26 2021 at 12:49):

"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 (Jan 26 2021 at 12:50):

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 (Jan 26 2021 at 12:51):

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 (Jan 26 2021 at 12:52):

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 (Jan 26 2021 at 12:52):

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

Mario Carneiro (Jan 26 2021 at 12:53):

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 (Jan 26 2021 at 12:54):

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 (Jan 26 2021 at 12:55):

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

Mario Carneiro (Jan 26 2021 at 12:55):

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

Eric Wieser (Jan 26 2021 at 12:56):

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 (Jan 26 2021 at 12:57):

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 (Jan 26 2021 at 13:50):

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 (Jan 26 2021 at 13:52):

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 (Jan 26 2021 at 13:52):

Lean 4 is actually less flexible in this regard

Patrick Massot (Jan 26 2021 at 13:54):

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 (Jan 26 2021 at 13:55):

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 (Jan 26 2021 at 13:56):

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

Kevin Buzzard (Jan 26 2021 at 13:57):

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

Mario Carneiro (Jan 26 2021 at 13:57):

I'm not sure most computer scientists care about intuitionism

Mario Carneiro (Jan 26 2021 at 13:57):

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

Mario Carneiro (Jan 26 2021 at 13:59):

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 (Jan 26 2021 at 13:59):

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 (Jan 26 2021 at 13:59):

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

Mario Carneiro (Jan 26 2021 at 14:00):

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

Eric Wieser (Jan 26 2021 at 14:01):

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 (Jan 26 2021 at 14:02):

I guess that would violate proof irrelevance

Mario Carneiro (Jan 26 2021 at 14:03):

No, I'm answering your question

Mario Carneiro (Jan 26 2021 at 14:04):

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 (Jan 26 2021 at 14:04):

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

Mario Carneiro (Jan 26 2021 at 14:04):

get_witness would be inconsistent

Mario Carneiro (Jan 26 2021 at 14:05):

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

Mario Carneiro (Jan 26 2021 at 14:08):

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 (Jan 26 2021 at 14:10):

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

Mario Carneiro (Jan 26 2021 at 14:10):

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 (Jan 26 2021 at 14:10):

however it's inconsistent

Mario Carneiro (Jan 26 2021 at 14:11):

just like quotient.unquot

Mario Carneiro (Jan 26 2021 at 14:12):

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 (Jan 26 2021 at 14:16):

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 (Jan 26 2021 at 14:22):

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 (Jan 26 2021 at 14:57):

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 (Jan 26 2021 at 15:22):

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

Mario Carneiro (Jan 26 2021 at 15:23):

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

Yakov Pechersky (Jan 26 2021 at 15:23):

@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 (Jan 26 2021 at 15:37):

@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 (Jan 26 2021 at 15:46):

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 (Jan 26 2021 at 15:50):

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 (Jan 26 2021 at 19:59):

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 (Jan 26 2021 at 22:42):

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 (Jan 27 2021 at 04:42):

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 (Jan 27 2021 at 05:46):

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

Michael Beeson (Jan 27 2021 at 18:47):

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 (Jan 27 2021 at 18:52):

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 (Jan 27 2021 at 18:55):

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 (Jan 27 2021 at 18:59):

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 (Jan 27 2021 at 19:19):

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

Mario Carneiro (Jan 27 2021 at 20:08):

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 (Jan 27 2021 at 20:08):

Maybe an attribute can do something similar though

Michael Beeson (Jan 28 2021 at 17:33):

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 (Jan 28 2021 at 17:34):

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

Michael Beeson (Jan 28 2021 at 17:35):

No, output does not change with a full stop.

Eric Wieser (Jan 28 2021 at 17:40):

What is the output?

Mario Carneiro (Jan 28 2021 at 17:41):

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 (Jan 28 2021 at 17:45):

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

Mario Carneiro (Jan 28 2021 at 17:45):

right, you need

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

Eric Wieser (Jan 28 2021 at 17:46):

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

Eric Wieser (Jan 28 2021 at 17:46):

Answer: yes, @@mul_assoc is an example

Mario Carneiro (Jan 28 2021 at 17:46):

also @@list.rec

Eric Wieser (Jan 28 2021 at 17:47):

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

Mario Carneiro (Jan 28 2021 at 17:48):

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

Mario Carneiro (Jan 28 2021 at 17:48):

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

Mario Carneiro (Jan 28 2021 at 17:48):

probably just trace decl is sufficient

Mario Carneiro (Jan 28 2021 at 17:51):

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 (Jan 28 2021 at 17:56):

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

Mario Carneiro (Jan 28 2021 at 17:56):

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 (Jan 28 2021 at 17:57):

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 (Jan 28 2021 at 17:59):

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

Eric Wieser (Jan 28 2021 at 18:00):

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

Mario Carneiro (Jan 28 2021 at 18:00):

not that I know of

Mario Carneiro (Jan 28 2021 at 18:01):

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

Eric Wieser (Jan 28 2021 at 18:01):

Can you do something dumb like vm_override trace?

Mario Carneiro (Jan 28 2021 at 18:02):

#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 (Jan 28 2021 at 18:02):

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

Mario Carneiro (Jan 28 2021 at 18:03):

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

Michael Beeson (Jan 28 2021 at 18:08):

#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 (Jan 28 2021 at 18:08):

yeah, that's the idea

Michael Beeson (Jan 28 2021 at 18:09):

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

Mario Carneiro (Jan 28 2021 at 18:09):

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

Michael Beeson (Jan 28 2021 at 18:10):

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

Michael Beeson (Jan 28 2021 at 18:10):

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

Mario Carneiro (Jan 28 2021 at 18:10):

If you use funext then quot.sound will get involved

Mario Carneiro (Jan 28 2021 at 18:37):

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 (Jan 28 2021 at 18:43):

@[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 (Jan 28 2021 at 19:15):

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

Michael Beeson (Jan 28 2021 at 19:17):

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 (Jan 29 2021 at 20:14):

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 (Jan 29 2021 at 20:17):

square brackets are only for typeclass arguments

Mario Carneiro (Jan 29 2021 at 20:18):

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

Mario Carneiro (Jan 29 2021 at 20:19):

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 (Jan 29 2021 at 20:21):

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 (Jan 29 2021 at 20:22):

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 (Jan 29 2021 at 20:22):

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 (Jan 29 2021 at 20:24):

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 (Jan 29 2021 at 20:25):

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 (Jan 29 2021 at 20:25):

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 (Jan 29 2021 at 20:26):

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

Michael Beeson (Jan 29 2021 at 20:27):

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

Mario Carneiro (Jan 29 2021 at 20:27):

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 (Jan 29 2021 at 20:28):

Nah, the a bug is dead and gone

Mario Carneiro (Jan 29 2021 at 20:28):

long live the alpha-vrachy bug

Michael Beeson (Jan 29 2021 at 20:29):

OK!

Michael Beeson (Jan 29 2021 at 20:30):

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

Michael Beeson (Jan 29 2021 at 20:46):

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 (Jan 29 2021 at 20:53):

dsimp only

Michael Beeson (Jan 29 2021 at 20:58):

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 (Jan 29 2021 at 21:00):

dsimp without only means dsimp with all definitional simp lemmas

Mario Carneiro (Jan 29 2021 at 21:00):

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

Mario Carneiro (Jan 29 2021 at 21:02):

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 (Feb 13 2021 at 19:20):

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 (Feb 13 2021 at 19:21):

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

Michael Beeson (Feb 13 2021 at 19:34):

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 (Feb 13 2021 at 19:55):

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 (Feb 13 2021 at 19:56):

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

Michael Beeson (Feb 16 2021 at 00:55):

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.


Last updated: Dec 20 2023 at 11:08 UTC