theorem vs axiom elaborating difference

Stream: general

[Mikhail Mayorov]

Hi, here's a snippet to illustrate the problem I have(apologies if it's not as minimal as it could've been)

variable {α : Type _} {unit : α}

axiom unit_yes {as : Array α} (h : ∀ i, (hi : i < as.size) → as[i] = as[i]) : True
#check @unit_yes

theorem unit_no {as : Array α} (h : ∀ i, (hi : i < as.size) → as[i] = as[i]) : True := trivial
#check @unit_no

This outputs

@unit_yes : ∀ {α : Type u_1} {unit : α} {as : Array α}, (∀ (i : Nat) (hi : i < as.size), as[i] = as[i]) → True

and then almost the same type for unit_no but without the {unit : α} part. You could say that this happens because h is unused but I have some examples that show it's not the case.

Instead, it seems to me that the issue is that axioms and theorems get elaborated in 2 different ways, the former with "mkForallFVars with usedOnly := true" and the latter with "collectFVars on the already-elaborated header type, then removeUnused to restrict the local context"(this was explained to me by an LLM agent, but does seem at least somewhat close to the truth).

Is this intentional?

(why this is a problem for me: for my project I wanted to try replacing theorems with axioms, I thought this would be alwsys safe, but because of the issue described, a proof that was apply ing the original theorem now creates an additional goal)

[Edward van de Meent]

this is essentially the same as the difference between def and theorem/lemma. I'm reasonably sure this is intentional.

[Edward van de Meent]

i believe the reasoning for this was that for lemmas you usually only want to include variables which are somehow related to the type of the lemma

[Robin Arnez]

I wanted to try replacing theorems with axioms

For which reason? Note that under the module system, theorems already become axioms when imported.

[Edward van de Meent]

(not literally, although lean indeed doesn't inspect the proof of imported lemmas)

[Snir Broshi]

It might be literally, per #lean4 > Accessing `Expr` of a def across modules @ 💬
The ConstantInfo of defs/theorems becomes ConstantInfo.axiomInfo

[Mirek Olšák]

I don't understand how this can be intentional. Only axiom behaves differently from others (I tried def, lemma, theorem, opaque), and usual Lean users use at most 6 axioms altogether, so I don't see a good reason to give it a special treatment.

[Mirek Olšák]

I guess the reason for this to happen is that in the axiom, the tactic for a valid index for a[i] finds a different proof in axiom than in the other cases.

[Robin Arnez]

No, it doesn't seem like that's the case. My guess is that there was just an oversight

[Edward van de Meent]

Snir Broshi said:

It might be literally, per #lean4 > Accessing `Expr` of a def across modules @ 💬
The ConstantInfo of defs/theorems becomes ConstantInfo.axiomInfo

and yet, #print axioms will not report them... so they are not in every aspect the same as though they are axioms

[Robin Arnez]

#print axioms doesn't currently work though in the module system?

[Robin Arnez]

To be precise: If you remove that error, then #print axioms with the current implementation would report every theorem, opaque and non-exposed definition in modules.

[Snir Broshi]

Oh wow that makes sense, I couldn't figure out why I couldn't shake any axioms when trying to come up with a counterexample for #Type theory > Equality without axioms
Maybe we can add a temporary warning until they fix it

[Mirek Olšák]

What is going on?

variable {α : Type} (unit : α)
axiom unit_nah (as : Array α) (h : ∀ i, (hi : i < as.size) → as[i]'hi = as[i]'hi) : True
axiom unit_yes (as : Array α) (h : ∀ i, (hi : i < as.size) → as[i]'hi = as[i]'(by assumption)) : True
#check unit_nah
#check unit_yes

[Mikhail Mayorov]

Robin Arnez said:

I wanted to try replacing theorems with axioms

For which reason? Note that under the module system, theorems already become axioms when imported.

What I want to achieve is, given some computer-generated proof, make sure it does not depend on a given theorem. And #print axioms already does all the heavy lifting for this.

(+ the program that generates the proofs isn't written in lean, so just adding a line to the proof and checking compiler diagnostics sounded like an elegant solution).

I am very interested in any other approaches for this, but they should be accessible for lean beginner :D
upd: I found a good solution now

[Robin Arnez]

Back to the original topic, it seems like the problem was indeed the proof for a[i] but not because it is different for axiom but because it gets instantiateMVarsed too late:

/- Bad code (how we currently have it) -/
let type ← instantiateMVars type -- only mvars in the type get instantiated
let type ← mkForallFVars xs type -- but not in the binder types
-- so we have mvars depending on the entire context
-- so `mkForallFVars` can't remove any binder
let type ← mkForallFVars vars type (usedOnly := true)
-- another `instantiateMVars` happens somewhere later

/- Good code (fix) -/
let type ← mkForallFVars xs type
-- instantiates mvars everywhere including the binders
let type ← instantiateMVars type
-- mvars are gone so no more dependency!
let type ← mkForallFVars vars type (usedOnly := true)

[Mirek Olšák]

Nice! So you could again submit a fix to hear from FRO that they are afraid it could be a breaking change :sweat_smile: .

[Robin Arnez]

Here it is: lean4#12497

[Edward van de Meent]

Supposedly, it's ok to be liberal with instantiateMVars (says the metaprogramming book), so we could use it before and after mkForallFVars?