Zulip Chat Archive

Stream: maths

Topic: linarith failure


view this post on Zulip Kevin Buzzard (Jan 17 2019 at 19:47):

I've started doing basic analysis in Lean with the undergraduates and I'm really using linarith a lot, it's really handy for this sort of thing. I was trying to prove that 1/n tended to zero using it, and I ran into this:

example (a b c : ) (h1 : 1 / a < b) (h2 : b < c) : 1 / a < c := by linarith -- fails

Is that a bug, or am I asking too much?

view this post on Zulip Mario Carneiro (Jan 17 2019 at 19:48):

that looks like a bug

view this post on Zulip Mario Carneiro (Jan 17 2019 at 19:49):

does generalize : 1/a = x; linarith work?

view this post on Zulip Rob Lewis (Jan 17 2019 at 19:50):

Yeah, that should be within scope. I'm guessing it's still too aggressive about ignoring nonlinear things, instead of trying to work with the linear parts. I fixed something related a while back iirc, but maybe not enough.

view this post on Zulip Mario Carneiro (Jan 17 2019 at 19:54):

linarith h1 h2 should work if it's a filtering problem

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 19:54):

Yes, generalizing works.

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 19:54):

linarith takes arguments??

view this post on Zulip Mario Carneiro (Jan 17 2019 at 19:54):

apparently (reading the src now)

view this post on Zulip Rob Lewis (Jan 17 2019 at 19:54):

It might reject it at the parsing step though.

view this post on Zulip Rob Lewis (Jan 17 2019 at 19:55):

I'll look into it soon.

view this post on Zulip Rob Lewis (Jan 17 2019 at 19:55):

linarith takes arguments, in case you have lots of hypotheses and know which ones are contradictory.

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:12):

PS this was great:

example (x y : ) : abs (x + y)  abs x + abs y :=
begin
  unfold abs, unfold max,
  -- goal with three ite's in
  split_ifs,
  -- 8 goals
  repeat {linarith},
end

view this post on Zulip Johan Commelin (Jan 17 2019 at 20:12):

You can replace that , repeat with a ;

view this post on Zulip Johan Commelin (Jan 17 2019 at 20:12):

But that's less readable

view this post on Zulip Patrick Massot (Jan 17 2019 at 20:13):

It requires knowing what ; does, but then it's readable

view this post on Zulip Rob Lewis (Jan 17 2019 at 20:34):

This is buried a little deeper than I expected. It's a mistake in the part of linarith that normalizes non-integer coefficients (in norm_hyp_aux I think). I'll fix it, but not tonight.

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:35):

Thanks for chasing this up! I really want to let undergraduates see that doing basic analysis in Lean is really easy, the triangle inequality proof went down really well!

view this post on Zulip Patrick Massot (Jan 17 2019 at 20:37):

I'm also very interested in this. Do you have files to share?

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:37):

I've only given one lecture so far and I've done barely anything.

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:39):

https://github.com/ImperialCollegeLondon/M1P1-lean

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:40):

I proved a sequence has at most one limit; I used ring to prove things like e + e = 2 * e and Kenny was in the front row exploding.

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:40):

But I can't teach all the students the 100 lemmas each of which can be proved by ring

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:40):

I want to just teach them ring instead

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:43):

My plan is to track their lectures and prove the interesting theorems as they're proved in class.

view this post on Zulip Mario Carneiro (Jan 17 2019 at 20:44):

wow, you really jumped right in

view this post on Zulip Mario Carneiro (Jan 17 2019 at 20:44):

in the ITP class Jeremy and I are teaching we've barely got to what a def is, how variable and section work and so on

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:45):

I asked the lecturer. He said that he was going to assume that the reals were a complete archimedean field and develop everything from that.

view this post on Zulip Patrick Massot (Jan 17 2019 at 20:45):

This is why we need mathematicians to teach proof assistants

view this post on Zulip Kevin Buzzard (Jan 17 2019 at 20:46):

so my plan was to spend the term trying to prove the things he proved, but in Lean. I would imagine that many of them are in mathlib already, but I didn't even look at the definition of a sequence tending to a limit in case it used cofinite filters. Of course I used the epsilon / N definition, because that's what they're told.

view this post on Zulip Rob Lewis (Jan 17 2019 at 22:24):

Never mind, I fixed it tonight. There could be some similar cases that this fix misses though.

view this post on Zulip Kevin Buzzard (Jan 24 2019 at 13:14):

I have another linarith failure. The hypotheses involving N and n are irrelevant to the goal, and if you comment out the line with them in then linarith succeeds, but if you leave them in then it fails.

example
(N : ) (n : ) (Hirrelevant : n > N) -- comment out this line to fix
(A : ) (l : ) (h : A - l  -(A - l)) (h_1 : ¬A  -A) (h_2 : ¬l  -l)
(h_3 : -(A - l) < 1) :  A < l + 1 := by linarith
/-
done tactic failed, there are unsolved goals
...
⊢ ↑(2 * -1) + 2 = 0
-/

view this post on Zulip Rob Lewis (Jan 24 2019 at 14:52):

Yeah, I know what's going on here. linarith is actually "succeeding," but Hirrelevant convinced it it was working over int instead of real, so it builds the wrong proof of contradiction. I'm on it.

view this post on Zulip Rob Lewis (Jan 24 2019 at 14:52):

In the meantime, you can help it out by calling linarith {restrict_type := ℝ} instead.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:13):

Is this expected behaviour?

import tactic.linarith

example (a : ) (b : ) (h : a < b) : a < b :=
begin
  let c := b,
  show a < c,
  linarith, -- fails
/-
linarith failed to find a contradiction
state:
a b : ℤ,
h : a < b,
c : ℤ := b,
a_1 : a ≥ c
⊢ false
-/
  sorry
end

In practice I have some positive real eps := (b - a) / 2 which is mentioned in several hypotheses and the conclusion. I can close my goal with lots of change or show commands removing all the eps's and then running linarith after, but my understanding of the internals of linarith is sufficiently poor that I don't know whether I should expect the tactic to handle these variables defined in terms of other variables or whether they're my problem.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:16):

Aah, I can do have Heps : eps = (b - a) / 2 := rfl, rw Heps at * as a workaround :-) I don't know any other way of doing multiple substitutions at once.

view this post on Zulip Reid Barton (Jan 28 2019 at 21:18):

Do you need the rw? After all eps = (b - a) / 2 is also a linear constraint

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:19):

Well spotted :-) Yes, it works fine in my (quite complicated) use case. Excellent trick!

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:23):

import tactic.linarith

example (a : ) (b : ) (h : a < b) : a < b :=
begin
  let c := b,
  show a < c,
  -- linarith, -- fails
  have : c = b := rfl,
  linarith, -- works
end

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:25):

It's funny that c := b shows up in my local context, but the hypothesis that c = b is apparently not in it. If the let were syntactic sugar, I wouldn't need the have, right? I'm not entirely sure what's going on here. Hmm, oh OK, maybe c is defined to be b, and Lean knows this but the fact isn't in the local context. I guess I'm showing my ignorance of how things really work here. I was hoping unfold eps would work in my case but it didn't.

view this post on Zulip Reid Barton (Jan 28 2019 at 21:42):

It seems like tactics like rw and simp sometimes "see through" let-bound variables, and I never understood exactly when or why

view this post on Zulip Rob Lewis (Jan 28 2019 at 21:45):

maybe c is defined to be b

This is roughly right, a let is like a local def. It's not syntactic sugar.

but the fact isn't in the local context

The information is in the type context, which is why you see c : Z := b. There's no term of type c = b until you add it manually. I don't think linarith should unfold let bindings, since they can be used to hide arbitrarily large terms. It's analogous to unfolding definitions (which linarith doesn't do and shouldn't do).

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:56):

Thanks for the clarification Rob. I didn't like my original solution (lots of 'change') but I'm happy to add the hypothesis that c equals its definition to the context and then let linarith take over. I have over 20 occurrences of linarith in https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/limits.lean so far; it's an essential tactic for this sort of thing.

view this post on Zulip Patrick Massot (Jan 28 2019 at 21:58):

Did you tried also using mono?

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:59):

I don't know what that does.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 21:59):

Isn't it some disease in the US?

view this post on Zulip Patrick Massot (Jan 28 2019 at 22:01):

https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#mono

view this post on Zulip Patrick Massot (Jan 28 2019 at 22:02):

There is also https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#apply_rules

view this post on Zulip Patrick Massot (Jan 28 2019 at 22:06):

but apply_rules seems very slow

view this post on Zulip Patrick Massot (Jan 28 2019 at 22:08):

You can try to stick the following into your limits file:

-- Next lemma could be either hidden of given a user-friendly proof
lemma zero_of_abs_lt_all (x : ) (h :  ε > 0, |x| < ε) : x = 0 :=
eq_zero_of_abs_eq_zero $ eq_of_le_of_forall_le_of_dense (abs_nonneg x) $ λ ε ε_pos, le_of_lt (h ε ε_pos)

-- The next few things should be hidden
@[user_attribute]
meta def ineq_rules : user_attribute :=
{ name := `ineq_rules,
  descr := "lemmas usable to prove inequalities" }

attribute [ineq_rules] add_lt_add le_max_left le_max_right

meta def obvious_ineq := `[linarith <|> apply_rules ineq_rules]
run_cmd add_interactive [`obvious_ineq]
-- end of scary things

-- We're ready to prove the theorem.
theorem limits_are_unique (a :   ) (l m : ) (hl : is_limit a l)
(hm : is_limit a m) : l = m :=
begin
  -- Let prove |l - m| is smaller than any positive number, since that will easily imply l = m
  suffices :  ε : , ε > 0  |l - m| < ε,
    from eq_of_sub_eq_zero (zero_of_abs_lt_all _ this),
  -- Let ε be any positive number, and let's prove |l - m| < ε
  intros ε ε_pos,
  -- Because aₙ → l, there exists Nₗ such that n ≥ Nₗ → |aₙ - l| < ε/2
  cases hl (ε/2) (by obvious_ineq) with Nₗ Hₗ,
  -- Because aₙ → m, there exists Nₘ such that n ≥ Nₘ → |aₙ - m| < ε/2
  cases hm (ε/2) (by obvious_ineq) with Nₘ Hₘ,
  -- The trick is to let N be the max of Nₗ and Nₘ
  let N := max Nₗ Nₘ,
  -- Now clearly N ≥ Nₗ...
  have H₁ : Nₗ  N := by obvious_ineq,
  -- ... so |a_N - l| < ε/2
  have H : | a N - l| < ε/2 := Hₗ N H₁,
  -- similarly N ≥ Nₘ...
  have H₂ : Nₘ  N := by obvious_ineq,
  -- ... so |a_N - m| < ε/2 too
  have H' : | a N - m| < ε/2 := Hₘ N H₂,
  -- We now combine
  exact calc |l - m|  |a N - m| + |a N - l| : triangle' _ _ _
   ... < ε/2 + ε/2 : by obvious_ineq
   ... = ε : by ring,
end

view this post on Zulip Patrick Massot (Jan 28 2019 at 22:10):

Note that you can put triangle' into the list of obvious inequalities and get all inequalities proved for free, but this would probably be cheating

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 22:27):

Can this do the product of limits is limit of product?

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 22:27):

That was horrible

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 22:27):

https://github.com/ImperialCollegeLondon/M1P1-lean/blob/87f2b5b4dc741c5d44751678e37229c1964799e3/src/limits.lean#L299 That was where it started going wrong

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:00):

linarith seems to know add_lt_add for the reals.

view this post on Zulip Kevin Buzzard (Jan 28 2019 at 23:45):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/nonlinarith/near/157067630 Got it, thanks to you and Reid.

view this post on Zulip Patrick Massot (Jan 29 2019 at 08:27):

Actually I also don't like your triangle'. Remembering 10 versions of the triangle inequality is not how we teach this. You can do:

  calc
    |l - m| = |(l - a N) + (a N - m)| : by ring
        ...  |l - a N| + |a N - m|   : by obvious_ineq
        ... = |a N - l | + |a N - m|  : by rw abs_sub
        ... < ε/2 + ε/2               : by obvious_ineq
        ... = ε                       : by ring,

where the only painful part is this rw abs_sub. I added abs_add, which is the regular triangle inequality for abs, to the obvious_ineq rules, but it's probably better to explicitly use it since it's a key part of the argument

view this post on Zulip Patrick Massot (Jan 29 2019 at 08:27):

simply replace that by obvious_ineq with abs_add _ _

view this post on Zulip Patrick Massot (Jan 29 2019 at 08:28):

I'll do limits of products tonight if I have time, and if I'm not too depressed about trying to use Lean for teaching (my first lecture using Lean will be at the end of this afternoon)

view this post on Zulip Johan Commelin (Jan 29 2019 at 09:01):

Good luck Patrick!

view this post on Zulip Johan Commelin (Jan 29 2019 at 09:01):

And I really like your little tactics!

view this post on Zulip Jeremy Avigad (Jan 29 2019 at 13:26):

A thought: it might be useful to have a tactic set that does what Kevin wants, i.e. a version of let that puts an equality in the context. For example, set h : a = t would create a new variable a, and put h : a = t into the context. Under the hood, set changes the goal G to forall a, a = t -> G, and then introduces the hypotheses. It's a combination of noting t = t, reverting, generalizing, and introducing. (But maybe there is already a nice way to do this?)

view this post on Zulip Rob Lewis (Jan 29 2019 at 13:59):

It seems more natural to use a let to do that. Why not preserve the definitional equality?

open tactic lean.parser interactive interactive.types

meta def tactic.set (a h : name) (v : expr) : tactic unit :=
do tp  infer_type v,
   nv  definev a tp v,
   to_expr ``(%%nv = %%v) >>= assert h,
   reflexivity

meta def tactic.interactive.set (h : parse ident) (_ : parse (tk ":")) (a : parse ident)
  (_ : parse (tk ":=")) (v : parse texpr) :=
i_to_expr v >>= tactic.set a h

example (x y : ) : x + y + x + y + x + y = 5 :=
begin
  set h : n := x + y,
end

view this post on Zulip Jeremy Avigad (Jan 29 2019 at 14:27):

Looks good to me!

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 14:42):

The syntax looks a bit funny, it looks like h has type n :-/

view this post on Zulip Rob Lewis (Jan 29 2019 at 14:43):

It is unfortunately not analogous to let h : n := x + y. Better suggestion?

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 14:44):

I remember always being muddled by generalize...

view this post on Zulip Rob Lewis (Jan 29 2019 at 14:45):

set n := x + y using h?

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 14:45):

maybe that's better!

view this post on Zulip Kevin Buzzard (Jan 29 2019 at 14:45):

cool little parser exercise to do now :-)

view this post on Zulip Johan Commelin (Jan 29 2019 at 15:03):

set n := x + y with h in analogy with cases ... with etc.
I think using will "use" one of your current hypotheses, or some expression (like in simpa),
whereas with gives names for new hypotheses.

view this post on Zulip Sebastien Gouezel (Jan 29 2019 at 17:18):

Is it possible to even get let n := x + y with h?

view this post on Zulip Patrick Massot (Jan 29 2019 at 19:41):

In addition to syntax discussions, the question is whether this tactic should replace x+y by n everywhere, or only in the goal, or nowhere.

view this post on Zulip Johan Commelin (Jan 29 2019 at 19:44):

In the example that Rob posted, associativity would prevent a naive replacement to yield n+n+n = 5, right? So then the replacement algorithm needs to know about associativity, and it becomes complicated.

view this post on Zulip Rob Lewis (Jan 29 2019 at 20:17):

Yeah, the example doesn't illustrate this very well. Maybe a variant set! n := x + y with h could try simp only [h.symm] at * at the end. But I think it's better not to do this by default, to match the behavior of let.

view this post on Zulip Rob Lewis (Jan 29 2019 at 20:18):

@Sebastien Gouezel tactic.interactive.let is defined in core, so I'm afraid not.

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:18):

I've added this. The basic syntax is set n := x + y with h. Alternatives: set! n := x + y with h will rewrite x + y to n everywhere it can. set n := x + y with h⁻¹ will make the equality proof face the other direction.

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:19):

I ended up needing this tactic for something I was doing yesterday, heh. It also led me to another bug in linarith.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:35):

how is this different from let?

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:36):

It adds a hypothesis that states the new definition propositionally.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:36):

is it also a let?

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:36):

Yes.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:37):

I think the set n := x + y variant may also be useful - no equality assumption, but x + y gets replaced by n

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:38):

I think that set! should be the default behavior, I'm not sure where the set behavior is better

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:39):

also I suggest <- h instead of h⁻¹ for the reversed proof - we haven't used the inverse symbol for symmetry since lean 2

view this post on Zulip Kenny Lau (Feb 01 2019 at 11:41):

Next time could we discuss the details before making changes to the mathlib in order to minimize changes to tactic/interactive.lean?

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:42):

I chose this as the default because set! sometimes reorders hypotheses, which is a little annoying if you don't care. It's not a big deal though, I can change it. Sure, the behavior without an equality hypothesis sounds good, as well as the notation.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:43):

I hope that the changes can be obtained by change rather than rw

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:43):

change at * seems to have a bug, it fails completely.

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:43):

Or rather, it succeeds without doing anything.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:44):

you have to do it somewhat manually with the noninteractive change

view this post on Zulip Mario Carneiro (Feb 01 2019 at 11:44):

you revert the relevant hypotheses then use tactic.change

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:46):

I'll give it another shot. I tried this first, but it was behaving strangely.

view this post on Zulip Rob Lewis (Feb 01 2019 at 11:46):

Gotta run, lunchtime.

view this post on Zulip Sebastien Gouezel (Feb 01 2019 at 16:01):

set-related question, although indirectly. I have an element of fin n given by a complicated formula, to which I would like to give a name for clarity. let x := complicated_expression works fine, but it would even be more useful for me to give a name to the fields of x directly, i.e., to write let ⟨i, hi⟩ := complicated_expression. This does not work. I can define x, and then let i := x.1, let hi := x.2, but then the fact that ⟨i, hi⟩ = complicated_expression is not refl, it requires a proof based for instance on fin.ext_iff. All this looks like useless plumbing to me. Is there a nice syntax to do this that I am unaware of?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:45):

Sebastien's question above deserves some expert comment but perhaps it's not in the right thread.

Independent of all this, here's an interesting session:

import tactic.linarith

example (α : Type*) [linear_ordered_ring α] (r s : α) :
-s + (r - (r - s)) = 0 := by ring -- fails, I think because α is not commutative

example (α : Type*) [linear_ordered_ring α] (r s : α) :
-s + (r - (r - s)) = 0 := by simp -- works

example (α : Type*) [linear_ordered_ring α] (r s : α) (h : s  0) :
r - s  r := by linarith -- fails because of unsolved goal -s + (r - (r - s)) = 0

example (α : Type*) [linear_ordered_ring α] (r s : α) (h : s  0) :
r - s  r := by linarith {discharger := simp} -- "unknown identifier 'simp'"

I have been building the theory of decimal expansions so that I can formalise last year's M1F final exam in Lean, and I was surprised to find that linear_ordered_rings were not commutative! Does anyone know an example of a linearly ordered ring which is not commutative? It is not even entirely impossible that they are all commutative, although I've not thought about this; it's probably more likely that there are pathological examples. Is every linearly ordered floor ring commutative though?? Hmm, I seem to have wandered off topic myself.

Anyway, of course I could just take the lame way out and restrict to linear_ordered_comm_rings, which ultimately I will surely end up doing, but I tried to work my way around this using simp and realised that I could not get the discharger argument to linarith working. Unfortunately my knowledge of meta lean is still sufficiently poor that I basically grind to a halt here when trying to debug why {discharger := simp} fails. Did I do something wrong or is there a bug?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:49):

To sebastian's question: it is impossible to achieve exactly the defeqs that he would want. In general it is not possible to get ⟨i, hi⟩ = complicated_expression to be defeq, unless complicated_expression has a particular form that allows reduction to a constructor

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:50):

However rcases complicated_expression with ⟨i, hi⟩ will often achieve the desired result, provided you don't need to refer back to any more properties of complicated_expression after this point. (If you do, you can make sure to state them before the cases)

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:51):

Would cases complicated_expression with i hi be any different?

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:51):

no

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:51):

rcases just looks a bit closer to the other syntax

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:53):

does abel work on those goals?

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:54):

I'm going to move the floor_ring discussion elsewhere.

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:54):

abel -> r + gsmul (-1) s ≤ r

view this post on Zulip Mario Carneiro (Feb 04 2019 at 10:55):

My bet is that there are noncomm linear ordered rings

view this post on Zulip Rob Lewis (Feb 04 2019 at 10:56):

For the discharger question, use `[simp] instead.

view this post on Zulip Sebastien Gouezel (Feb 04 2019 at 11:01):

However rcases complicated_expression with ⟨i, hi⟩ will often achieve the desired result, provided you don't need to refer back to any more properties of complicated_expression after this point. (If you do, you can make sure to state them before the cases)

This is not an option in my case, I need to keep all information on complicated_expression. Fine, I'll go with my basic ugly (but working) solution, letting the components separately and proving the equality.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:01):

you should be able to get the equality on the components if you use set

view this post on Zulip Sebastien Gouezel (Feb 04 2019 at 11:02):

To try this, I have to rebase on a recent mathlib version :)

view this post on Zulip Mario Carneiro (Feb 04 2019 at 11:03):

I need to keep all information on complicated_expression.

This is almost certainly not true, it's just a question of how much information about the expression you need to retain. Of course the limiting case is where you keep the fact that the expression is equal to complicated_expression, in which case you get that equality ⟨i, hi⟩ = complicated_expression you said originally


Last updated: May 12 2021 at 07:17 UTC