propext contamination

Stream: new members

[Jun Yoshida]

Hi there, I recently found that some of my theorems written in Lean 3 accidentally depend on propext.
After some research, I discovered that one source of the dependency is simplification of ite; the following is MWE:

lemma test3 : ite (3=3) 1 0 = 1 := by simp *

#print axioms test3

I wonder why this happens and how to void it.
In fact, test3 above can be proved simply by rfl.

[Marcus Rossel]

You can see which lemmas were used by simp by using simp?. In this case it's:

if_congr
if_true
eq_self_iff_true

I'm guessing one of those uses propext.

[Marcus Rossel]

---

Well, apparently not ^^

[Marcus Rossel]

Doing:

lemma test3 : ite (3=3) 1 0 = 1 := by simp only [if_pos]

doesn't involve propext. So I'm guessing it just turns up as part of whatever simp is doing.

[Marcus Rossel]

---

If you #print your version of test3 it also shows you where the propext is used:

theorem test3 : ite (3 = 3) 1 0 = 1 :=
(id
   (((λ (a a_1 : ℕ) (e_1 : a = a_1) (ᾰ ᾰ_1 : ℕ) (e_2 : ᾰ = ᾰ_1), congr (congr_arg eq e_1) e_2)
       (ite (3 = 3) 1 0)
       1
       ((if_congr (eq_self_iff_true 3) (eq.refl 1) (eq.refl 0)).trans (if_true 1 0))
       1
       1
       (eq.refl 1)).trans
      (propext (eq_self_iff_true 1)))).mpr
  trivial

[Mario Carneiro]

simp uses propext to turn iff theorems into rewrite rules

[Mario Carneiro]

that is, when you give it a lemma like eq_self_iff_true i.e. x = x <-> true and mark it @[simp] it treats it like (x = x) = true

[Mario Carneiro]

this is a matter of implementation convenience - simp could work with multiple relations but it's more complicated to do so (I think it has limited support for this but for the most part rewrites only use =)

[Mario Carneiro]

rw will do the same thing

[Jun Yoshida]

Thank you guys for valuable information.
I found that tactic.simp_config has use_axioms field with default value tt, so setting it to ff does the trick.
e.g.

lemma test3 : ite (3=3) 1 0 = 1 := by simp * {use_axioms := ff}
#print axioms test3   -- no axioms

[Jun Yoshida]

By the way, is it possible to set this configuration to be default in local?

[Mario Carneiro]

No, but you can make your own simp' tactic that defers most arguments to simp but sets the configuration differently

[Jun Yoshida]

Ah, that makes sense. Thanks :smile:

[Mario Carneiro]

namespace tactic
namespace interactive
open tactic interactive lean.parser interactive.types
local postfix `?`:9001 := optional
local postfix *:9001 := many

meta def simp' (use_iota_eqn : parse $ (tk "!")?) (trace_lemmas : parse $ (tk "?")?)
  (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
  (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
simp use_iota_eqn trace_lemmas no_dflt hs attr_names locat {cfg with use_axioms := ff}

end interactive
end tactic

lemma test3 : ite (3=3) 1 0 = 1 := by simp' *
#print axioms test3   -- no axioms