## Stream: maths

### Topic: avoiding subtype.eq

#### Kevin Buzzard (Aug 21 2018 at 20:52):

import data.real.basic

example (p : ℝ → Prop) (a b : ℝ) (ha : p (a / 2)) (hb : p (b / 2)) (hab : a / 2 = b / 2) :
@eq {x : ℝ // p x} ⟨a/2,ha⟩ ⟨b/2,hb⟩ :=
begin
rw hab -- fails
end
-- rewrite tactic failed, motive is not type correct

example (p : ℝ → Prop) (a b : ℝ) (ha : p (a / 2)) (hb : p (b / 2)) (hab : a / 2 = b / 2) :
@eq {x : ℝ // p x} ⟨a/2,ha⟩ ⟨b/2,hb⟩ :=
begin
subst hab -- fails
end
-- subst tactic failed, hypothesis 'hab' is not of the form (x = t) or (t = x)
-- would have worked if hab was a = b

example (p : ℝ → Prop) (a b : ℝ) (ha : p (a / 2)) (hb : p (b / 2)) (hab : a / 2 = b / 2) :
@eq {x : ℝ // p x} ⟨a/2,ha⟩ ⟨b/2,hb⟩ :=
begin
apply subtype.eq,
exact hab,
end
-- do I have to do it like this?


#### Kevin Buzzard (Aug 21 2018 at 20:53):

Is there any way of doing the rewrite without using subtype.eq? i.e. some high-powered tactic? I've had some luck with subst in the past but not here.

#### Kevin Buzzard (Aug 21 2018 at 20:54):

dammit simp works this time :-) It didn't work in my real world example!

#### Mario Carneiro (Aug 21 2018 at 20:55):

by congr'

#### Patrick Massot (Aug 21 2018 at 20:57):

Makes me think: shouldn't lemma subtype.ext be marked as an extensionality lemma?

#### Kevin Buzzard (Aug 21 2018 at 21:02):

I'm trying to reproduce the problem that @Luca Gerolla has. He had rw failing because of the motive issue, subst failing because the hypothesis wasn't variable=term, and simp timing out. I have simp taking ages:

example (p : ℝ → Prop) (a b : ℝ) (ha : p ((a / 2) / ( 1 / 2)))
(hb : p ((b / 2) / (1 / 2)))
(hab : a / 2 = b / 2)
(X : {x : ℝ // p x} → ℝ) :
X ⟨(a/2)/(1/2),ha⟩ = X ⟨(b/2)/(1/2),hb⟩ :=
begin
simp [hab]
end


but not timing out yet.

#### Kevin Buzzard (Aug 21 2018 at 21:09):

import data.real.basic

example (p : ℝ → Prop) (a b : ℝ) (ha : p ((a / 2) / ( 1 / 2)))
(hb : p ((b / 2) / (1 / 2)))
(hab : a / 2 = b / 2)
(f : {x : ℝ // p x} → ℝ) :
f ⟨(a/2)/(1/2),ha⟩ = f ⟨(b/2)/(1/2),hb⟩ :=
begin
simp [hab]
end

example (p : ℝ → Prop) (a b : ℝ) (ha : p ((a / 2) / ( 1 / 2)))
(hb : p ((b / 2) / (1 / 2)))
(hab : a / 2 = b / 2)
(X : equiv {x : ℝ // p x} ℝ) :
X ⟨(a/2)/(1/2),ha⟩ = X ⟨(b/2)/(1/2),hb⟩ :=
begin
simp [hab]
end


For me, the yellow bars take far longer for the f version than the X version. Is that expected? I still haven't got the timeout but I get quite a long pause with the f version.

#### Mario Carneiro (Aug 21 2018 at 21:10):

use congr'

#### Kevin Buzzard (Aug 21 2018 at 21:17):

fair enough. I used apply congr_arg.

#### Luca Gerolla (Aug 21 2018 at 21:20):

Was the fact that ha and hab were "lost" (i.e. left with _) that caused the deterministic timeout with simp?

#### Luca Gerolla (Aug 21 2018 at 21:21):

Thanks for this, I was completely unaware of the congr tactic - another good learning!

#### Kevin Buzzard (Aug 21 2018 at 21:23):

Luca I've failed to reproduce your timeout in a controlled setting so far and I don't really want to post a 1300 line file :-)

#### Kevin Buzzard (Aug 21 2018 at 21:23):

congr unfolds as many layers as it can (i.e. reduces $f(g(x))=f(g(y))$ to $x=y$ and congr' 1 just removes one layer.

#### Luca Gerolla (Aug 21 2018 at 21:24):

I completely understand! :-)

#### Luca Gerolla (Aug 21 2018 at 21:25):

congr unfolds as many layers as it can (i.e. reduces $f(g(x))=f(g(y))$ to $x=y$ and congr' 1 just removes one layer.

That's quite helpful, probably I should implement congr also in other similar proofs

#### Mario Carneiro (Aug 21 2018 at 21:26):

also with congr' if at any point a subgoal matches a hypothesis the subgoal will be closed

#### Mario Carneiro (Aug 21 2018 at 21:27):

hence why a / 2 = b / 2 |- X ⟨(a/2)/(1/2),ha⟩ = X ⟨(b/2)/(1/2),hb⟩ is provable by congr'

#### Patrick Massot (Aug 21 2018 at 21:32):

also with congr' if at any point a subgoal matches a hypothesis the subgoal will be closed

Good to know. https://github.com/leanprover/mathlib/pull/270

#### Kevin Buzzard (Aug 21 2018 at 21:53):

simp is taking far longer than the profiler says. If I write this:

import data.real.basic

set_option profiler true

set_option trace.simplify true

theorem X234 (p : ℝ → Prop) (a b : ℝ) (ha : p ((a / 2) / ( 1 / 3)))
(hb : p ((b / 2) / (1 / 3)))
(hab : a / 2 = b / 2)
(f : {x : ℝ // p x} → ℝ) :
f ⟨(a/2)/(1/3),ha⟩ = f ⟨(b/2)/(1/3),hb⟩ :=
by simp [hab]


then the profiler says that elaboration takes under 0.5 seconds, but if I change the name of the theorem then I see the orange bars for around 4 seconds (on a reasonable machine).

Possibly unrelated: I'd never seen this sort of thing in the simp trace debugging output before:

[simplify] iff: function.injective f
[simplify] eq: function.injective f
[simplify] eq: f
[simplify] eq: function.injective
[simplify.failure] proof stuck at: function.injective f
[simplify.failure] failed to prove: ?x_3 : function.injective f
1. [simplify.failure] fail to instantiate emetas: 'function.injective.eq_iff' at
f (@subtype.mk ℝ (λ (x : ℝ), p x) (b / 2 / 3⁻¹) _) = f (@subtype.mk ℝ (λ (x : ℝ), p x) (b / 2 / 3⁻¹) _)
partially instantiated lemma:
@function.injective.eq_iff {x // p x} ℝ f ?x_3
(@subtype.mk ℝ (λ (x : ℝ), p x) (b / 2 / 3⁻¹)
(@eq.rec ℝ (a / 2 / (1 / 3)) (λ (val : ℝ), (λ (x : ℝ), p x) val) ha (b / 2 / 3⁻¹)
(@(λ [c : has_div ℝ] (a a_1 : ℝ) (e_2 : a = a_1) (a_2 a_3 : ℝ) (e_3 : a_2 = a_3),
@congr ℝ ℝ (@has_div.div ℝ c a) (@has_div.div ℝ c a_1) a_2 a_3
(@congr_arg ℝ (ℝ → ℝ) a a_1 (@has_div.div ℝ c) e_2)
e_3)
(@division_ring_has_div ℝ real.division_ring real.division_ring)
(a / 2)
(b / 2)
hab
(1 / 3)
3⁻¹
(@one_div_eq_inv ℝ real.division_ring 3))))
(@subtype.mk ℝ (λ (x : ℝ), p x) (b / 2 / 3⁻¹)
(@eq.rec ℝ (b / 2 / (1 / 3)) (λ (val : ℝ), (λ (x : ℝ), p x) val) hb (b / 2 / 3⁻¹)
(@(λ [c : has_div ℝ] (a a_1 : ℝ) (e_2 : a = a_1) (a_2 a_3 : ℝ) (e_3 : a_2 = a_3),
@congr ℝ ℝ (@has_div.div ℝ c a) (@has_div.div ℝ c a_1) a_2 a_3
(@congr_arg ℝ (ℝ → ℝ) a a_1 (@has_div.div ℝ c) e_2)
e_3)
(@division_ring_has_div ℝ real.division_ring real.division_ring)
(b / 2)
(b / 2)
(@eq.refl ℝ (b / 2))
(1 / 3)
3⁻¹
(@one_div_eq_inv ℝ real.division_ring 3))))


Last updated: May 12 2021 at 07:17 UTC