# Zulip Chat Archive

## 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