Unfolding carefully

Stream: general

[Moses Schönfinkel]

Suppose I have the following goal f a = c (f (d a)). What I am looking to do is to unfold1 f but only on the left hand side. Currently I do generalize hack : f (d a) = x, unfold1 f, rw <- hack. Apart from the fact that it's a hack, the generalize takes a couple of seconds to execute. I tried using conv { to_lhs ... } but unfold1 is not an option in conv (and simp fails with deterministic timeout). a) Why on Earth is generalize so slow in this case - is it because c is some horrible dependently typed function with explicit well founded termination proofs? b) Is there a nicer trick to invoke unfold1 on left hand side only?

[Kenny Lau]

use change?

[Moses Schönfinkel]

that would involve me having to explicitly state the effect of unfolding if I understand your suggestion; right?

[Simon Hudon]

What about using transitivity instead of generalize?

[Moses Schönfinkel]

ooh that is actually brilliant! what I ended up doing is something I'm ashamed of but it saves me 15 seconds on each recompile - I reformulated the lemma such that it contains a pre-generalized expression and an equality (which I will, of course, change now :P)

[Simon Hudon]

Great! Glad to be of help! So, the way I use transitivity to protect parts of my formulas is to do transitivity, blah, blah, refl

[Moses Schönfinkel]

Yeah I have never thought of that. Thanks a lot. I wish conv was a bit less constrained.

[Moses Schönfinkel]

if this worked, then conv { to_lhs, dsimp1 f } would be just fine for me - but interactive.conv.* only has a bunch of tactics for reasons I'm not sure I want to know about :P

[Simon Hudon]

If you have something more specific that you want to use, let's say g instead of =, you can also make your own protection lemmas:

lemma protect (x y : α) (z : β)
  (h : x = y)
  (h : g y z)
: g x z := ...

This allows you to select exactly what part of the formula you want to rewrite when you expect something very specific. And z is protected.

[Moses Schönfinkel]

ah, right; this is basically the general version that I ended up doing, but I think the transitivity is such a neat hack :P

[Simon Hudon]

if this worked, then conv { to_lhs, dsimp1 f } would be just fine for me - but interactive.conv.* only has a bunch of tactics for reasons I'm not sure I want to know about :P

I think Coq is more targeted like that rewrite h at 1,3. I found I missed that at first but I'm not sure it makes for stable proofs

[Moses Schönfinkel]

yes, in Coq I can rewrite where I want

[Moses Schönfinkel]

I can also rewrite under binders

[Moses Schönfinkel]

(with setoid rewrites)

[Moses Schönfinkel]

in Lean I've only used simp to rewrite under binders, not sure how else it can be even done

[Simon Hudon]

simp helps there with binders and congruence lemmas but it's a bit less controlled

[Simon Hudon]

... yeah, exactly

[Moses Schönfinkel]

stability of proofs has never been an issue for me, because, I, urm... write them once and then I... forget about them...

[Moses Schönfinkel]

I may need to try to write Coq in "industrial" settings :P

[Simon Hudon]

Question: I've only used Coq as a noob so I never experienced scaling up proofs that uses the at 1,3 notation. Do you find that your proofs breaks a lot when you do that?

[Moses Schönfinkel]

yes, they do

[Moses Schönfinkel]

it's the absolute worst thing one can do

[Simon Hudon]

In my temporal logic tactics language, I have played with a tactic you call as rw_using : f x = g x, { /- proof -/ }. For some reason, I liked not clearing a temporary assumption.

[Simon Hudon]

In temporal logic, that was doubly useful because the proof of equality was typically done in normal Lean logic

[Simon Hudon]

Otherwise, I really haven't found a drop in replacement for that Coq notation

[Moses Schönfinkel]

I wish I understood exactly how simp works but I have never had the willpower to look at it

[Moses Schönfinkel]

I believe it's been modeled to resemble the Isabelle heuristics you get when you're within a single theory section thing

[Moses Schönfinkel]

where theory just aggregates a set of related constants, definitions, proofs, etc. and you abuse this implicit relation in automation

[Simon Hudon]

I feel like I really don't understand what Isabelle does with any given proof. It's hard for me to understand that comparison

[Moses Schönfinkel]

you basically help guide automation in Isabelle by aggregating related stuff together in "theories", which is something like making a hint database in Coq

[Moses Schönfinkel]

(so like a beefy namespace that implicitly provides hints for automation)

[Simon Hudon]

Ah I see. Does it make things clearer to use the theories or the databases?

[Moses Schönfinkel]

databases are less implicit so you have to go over the trouble of creating them

[Moses Schönfinkel]

so in Isabelle you get nice behaviour by default but it's less controlled because it's just "whatever you put in this theory"

[Moses Schönfinkel]

I think people with purely math background would have easier time using Isabelle, simply because you get nice implicit heuristic-guided behaviour out of the box (+ the Sledgehammer)

[Moses Schönfinkel]

if I understand Kevin correctly, he uses Lean because he wants dependent types

[Moses Schönfinkel]

(or I should say, he's not using Isabelle because he wants dependent types)

[Moses Schönfinkel]

and simp in Lean takes after Isabelle default simplifier, I believe

[Simon Hudon]

Any chance that something like sledgehammer would work with dependent types? Or is it more of a matter of structuring databases like Isabelle?

[Moses Schönfinkel]

it would work, Sledgehammer is almost like an outside tool that ships proof obligations to SMT solvers and ATPs

[Moses Schönfinkel]

Sledgehammer is really the most unimpressive piece of Isabelle; it just tries to invoke every automating algorithm it can get its grabby mittens on

[Sebastian Ullrich]

That may be the understatement of the century

[Moses Schönfinkel]

:D

[Sebastian Ullrich]

Sledgehammer is the result of a multi-year research project that produced a good amount of papers http://www.cl.cam.ac.uk/~lp15/papers/Automation/

[Sebastian Ullrich]

The hard parts are relevance filtering of lemmas to pass to the external solver, and of course translating between HOL and FOL

[Moses Schönfinkel]

ok ok I will change it to 2 out of 10 on the scale of impressiveness, making it the second least impressive Isabelle feature right after its bundled development IDE :grinning:

[Kevin Buzzard]

I use Lean because when I had never heard of any theorem provers apart from Coq, and never used any at all, I watched a live stream of Tom Hales in Cambridge talking about (amongst other things) FAbstracts, and someone asked him which language he would be using, and he said "...Lean?" and I thought "OK that'll do for me"

[Kevin Buzzard]

and I certainly didn't know what a dependent type was at that point

[Kevin Buzzard]

I just decided to jump in

[Kevin Buzzard]

I wish I understood exactly how simp works but I have never had the willpower to look at it

I wish I understood more about how simp works but I learnt a couple of set_option options and wrote https://github.com/leanprover/mathlib/blob/master/docs/extras/simp.md

[Kevin Buzzard]

Looking at the output of set_option trace.simplify true gave me some sort of idea about the absolute inanity of what simp was doing

[Chris Hughes]

I wish I understood exactly how simp works but I have never had the willpower to look at it

I wish I understood more about how simp works but I learnt a couple of set_option options and wrote https://github.com/leanprover/mathlib/blob/master/docs/extras/simp.md

That bit at the end sounds interesting. Does that mean if I had a + b ≡ c [MOD n] and h : a ≡ d [MOD n] I could rewrite to get a + d ≡ c [MOD n]? How would that work with complicated examples, with lots of addition and multiplication?

[Kevin Buzzard]

I have never used that MOD business so I'm not sure

[Kevin Buzzard]

Oh, Gabriel said that

[Kevin Buzzard]

I didn't understand it so I didn't use it

[Kevin Buzzard]

[and you mean d + b = c of course]

[Kevin Buzzard]

Aah but I do remember that this might work in calc mode.

[Kevin Buzzard]

If your relation is tagged with trans then I think calc supports it

[Chris Hughes]

Can I mix equality and an congruences in calc?

[Kevin Buzzard]

I haven't ever seen this done

[Kevin Buzzard]

I think that either in the reference manual or in TPIL they are pretty formal about what you can do with calc

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#calculational-proofs

[Kevin Buzzard]

searching TPIL for calc doesn't find that

[Kevin Buzzard]

so I always look at https://github.com/kbuzzard/mathlib/blob/WIP_docs/docs/WIPs/calc.md

[Kevin Buzzard]

and indeed there is an example with different operators, = and < and <=

[Patrick Massot]

searching TPIL for calc doesn't find that

It does actually, but you don't recognize it

[Patrick Massot]

3rd result

[Patrick Massot]

I know this because I filled a Sphinx bug report before understanding this :flushed:

[Kevin Buzzard]

Oh! So "It's somewhere in Chapter 4" is the best I get?

[Patrick Massot]

yes

[Kevin Buzzard]

"PS here's the first occurrence of the string Calc"

[Kevin Buzzard]

"feel free to look and see if there are any others"

[Patrick Massot]

Web pages of TPIL are too big

[Patrick Massot]

from this point of view

[Kevin Buzzard]

That's one interpretation

[Kevin Buzzard]

Another is "search is crap"

[Kevin Buzzard]

I know we've all been spoilt by Google...

[Patrick Massot]

google would show you the same

[Kevin Buzzard]

or maybe section 4.3 should be tagged calc

[Kevin Buzzard]

and the search should prioritise tags

[Patrick Massot]

one hit for this page, and not all occurences on the search result page

[Kevin Buzzard]

is that possible in Sphinx?

[Kevin Buzzard]

Google might have a better idea about moving the "right" answer to #1 in the list...

[Chris Hughes]

Can I mix equality and an congruences in calc?

I tried it and you can.

[Patrick Massot]

Go to google and typein search bar: site:https://leanprover.github.io/theorem_proving_in_lean/ calc

[Patrick Massot]

Google is smarter than Sphynx

[Kevin Buzzard]

Can I mix equality and an congruences in calc?

@[trans] protected theorem trans : a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n] := eq.trans

[Kevin Buzzard]

and lo and behold

[Kevin Buzzard]

import data.nat.modeq
variables (a b c d m : ℕ)

example (H1 : a ≡ b [MOD m]) (H2 : b = c) (H3 : c ≡ d [MOD m]) : a ≡ d [MOD m] :=
calc a ≡ b [MOD m] : H1
... = c : H2
... ≡ d [MOD m] : H3

[Kevin Buzzard]

Google is smarter than everything :-/

[Chris Hughes]

what if I have two relations that are "co transitive" in the same sense that le and lt are. Can I make them work with calc?

[Kevin Buzzard]

Right, e.g. a congruence mod 8 might imply a congruence mod 4

[Kevin Buzzard]

I have no idea how Lean is doing the < and <= thing

[Patrick Massot]

calc knowing about that would be pretty cool

[Chris Hughes]

I thought that was a useless question, but obviously not.

[Kevin Buzzard]

I know from experience that it will let you prove a < d by writing a <= b < c <= d

[Kevin Buzzard]

so it knows lt_of_le_of_lt

[Patrick Massot]

yes, this is already really cool

[Kevin Buzzard]

but it wouldn't surprise me if this were hard wired in somehow

[Kevin Buzzard]

as a common use case

[Patrick Massot]

but I suspect this special case is hard-wired

[Chris Hughes]

lt_of_lt_of_le is tagged with trans. So it might just be a case of doing that.

[Kevin Buzzard]

Oh well spotted!

[Patrick Massot]

indeed

[Chris Hughes]

def r : ℕ → ℕ → Prop := sorry
def s : ℕ → ℕ → Prop := sorry

local infix `r'`:50 := r
local infix `s'`:50 := s

@[trans] lemma r.trans {a b c : ℕ} : r a b → r b c → r a c := sorry
@[trans] lemma rs.trans {a b c : ℕ} : r a b → s b c → r a c := sorry

@[trans] lemma rs.trans1 {a b c : ℕ} (h₁ : r a b) (h₂ : s b c) : r a c := calc
  a r' b : h₁
  ... s' c : h₂

[Chris Hughes]

That pasted from VScode without any extra spaces.

[Patrick Massot]

:hushed:

[Kevin Buzzard]

import data.nat.modeq
variables (a b c d m : ℕ)

@[trans] theorem helpful (a b c : ℕ) : a ≡ b [MOD 8] → b ≡ c [MOD 16] → a ≡ c [MOD 4] := sorry
example (H1 : a ≡ b [MOD 8]) (H2 : b = c) (H3 : c ≡ d [MOD 16]) : a ≡ d [MOD 4] :=
calc a ≡ b [MOD 8] : H1
... = c : H2
... ≡ d [MOD 16] : H3

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

so did that

[Kevin Buzzard]

So it's really not hard coded in, there is some dark art with trans tags

[Patrick Massot]

Let's keep that in Lean 4

[Kevin Buzzard]

Conclusion in my example must be a = c mod 8 after second line

[Kevin Buzzard]

it uses this:

[Kevin Buzzard]

#check trans_rel_left -- ∀ (r : ?M_1 → ?M_1 → Prop), r ?M_2 ?M_3 → ?M_3 = ?M_4 → r ?M_2 ?M_4

[Kevin Buzzard]

(I know because some messing around gave me some explicit error messages)

[Kevin Buzzard]

and then it uses my trans-tagged theorem for 3rd line

[Patrick Massot]

To the docs/extras/calc!

[Kevin Buzzard]

Yes, this deserves to be better known

[Kevin Buzzard]

I mean it's mentioned in TPIL but somehow it hadn't dawned on me how far you could push this

[Chris Hughes]

So now I know the point of @[trans] and @[refl] but I'm still not sure why you would tag something @[symm]

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20is.20amazing

[Kevin Buzzard]

Gabriel's comment is in that thread

[Kevin Buzzard]

but I don't know any longer if it was about simp

[Kevin Buzzard]

If you tag something symm then there's some tactic called symmetry which will work ;-)

[Patrick Massot]

We need to formalize something using this calc power

[Patrick Massot]

What about some version of Hensel's lemma?

[Patrick Massot]

There should be chains of congruence modulo different stuff there

[Patrick Massot]

And it may even be useful for perfectoids, who knows?

[Kevin Buzzard]

theorem X (a b m : ℕ) (H : a ≡ b [MOD m]) : b ≡ a [MOD m] := by symmetry;assumption

[Chris Hughes]

theorem X (a b m : ℕ) (H : a ≡ b [MOD m]) : b ≡ a [MOD m] := H.symm

[Kevin Buzzard]

symmetry tactic replaces a hypothesis with another one if the fact that one implies the other is marked with symm

[Chris Hughes]

I know what it does, but it seems fairly useless.

[Kevin Buzzard]

Simon's cool use of transivity is above, and refl is used everywhere, but who knows what symmetry is for :-)

[Chris Hughes]

Simon's cool use of transivity is above, and refl is used everywhere, but who knows what symmetry is for :-)

What's Simon's cool use of transitivity?

[Kevin Buzzard]

At the start of this thread

[Kevin Buzzard]

To the docs/extras/calc!

https://github.com/kbuzzard/mathlib/blob/WIP_docs/docs/WIPs/calc.md

[Chris Hughes]

Can I use calc if I haven't defined an infix for my relation?

[Kevin Buzzard]

I don't know!

[Kevin Buzzard]

As you can see I defined infixes for mine.

[Kevin Buzzard]

@Mario Carneiro I wrote some calc docs (see link above) extending what is written in TPIL, together with some notes for things I struggled with myself after reading TPIL (e.g. I would sometimes get into a real mess with some syntax error or proof error manifesting itself as a red squiggle under a random ...). Three questions:

[Kevin Buzzard]

1) Shall I PR to mathlib?

[Kevin Buzzard]

2) Chris asks if calc can be used with operators that aren't infix

[Kevin Buzzard]

3) I made some guesses as to how calc works. In particular I note that trans_rel_right and trans_rel_left are not tagged [trans]. Are these special cases which are tried first?

[Kevin Buzzard]

And an idle question -- would it be possible to break calc by proving e.g. a < b -> b < c -> a <= c and tagging with [trans]?

[Kevin Buzzard]

And @Patrick Massot After Mario accepted my last mathlib PRs I just nuked the entire repo and forked it again (do you remember I had a bad commit history because I never branched?). Now I have a branch with my WIPs. I know I can google for how to do this but I'm sure you will know instantly -- what is the best way to just PR the calc.md file? Sorry to bother you.

[Patrick Massot]

Since you have only one file to PR and don't care about keeping the history of this file, here the simplest route: copy that calc.md somewhere else (say /home/kevin/), then, inside mathlib,

git checkout master
git checkout -b docs-calc
cp /home/kevin/calc.md docs/extras/

then edit docs/extras.md to add a link to docs/extra/calc.md

git add docs/extras.md docs/extra/calc.md
git commit
git push

The last command will complain you should explicitly say to create an upstream branch. Copy-paste the suggested command (I never remember the syntax since git always helps me here).

[Patrick Massot]

I forgot: don't forget to make sure your master is in sync with Mario's before git check-out -b docs-calc

[Patrick Massot]

assuming you followed conventional names, that would mean git pull upstream master after git checkout master

[Mario Carneiro]

It's not a big problem if you PR off an old version of mathlib, since I usually rebase it on the current head when I merge the PR anyway

[Mario Carneiro]

unless there's a conflict of course

[Mario Carneiro]

but docs don't usually cause conflicts if they are new

[Patrick Massot]

sure

[Patrick Massot]

I'm only trying to explain good practice

[Mario Carneiro]

I agree with everything you said.

I would add that if you intend to PR some addition, you should write it "in place", i.e. with the file located in mathlib where you want it to be, by first checking out master then checking out a new branch (i.e. the first two lines of Patrick's script), then making any modifications there. Then any commits you make will branch from master nicely. If you need to set the work aside, you can just commit what you have to the branch and move to the current master or somewhere else, and come back to your PR when you are ready to resume work with git checkout my-pr.

[Patrick Massot]

No -b in your last sentence

[Patrick Massot]

Otherwise of course this is the correct way. I was explaining how to fix the mess.

[Mario Carneiro]

oops, typo (copy-o?)

[Kevin Buzzard]

OK done. Thanks both for the advice. Mario -- it's a bit of a WIP because I guessed how the transitivity worked in calc mode. First I guessed that Lean went from A op1 B op2 C op3 D to A op4 D via "reading from left to right", i.e. first attempting to figure out how A op1 B op2 C can become A op5 C and then merging this with C op3 D (i.e. I don't know if it does anything clever like trying to merge two random consecutive theorems in the middle), and secondly I guessed that when trying to merge two ops to become another one it first uses rw if one is = and then tries lemmas tagged trans if neither op is =. These are just plain guesses.

[Chris Hughes]

I did some testing and I don't think it tries to do anything clever with changing the order. L2 doesn't work below, but the rest do. You can also state that three relations are transitive together.

def r : ℕ → ℕ → Prop := sorry
def s : ℕ → ℕ → Prop := sorry
def t : ℕ → ℕ → Prop := sorry

local infix `r'`:50 := r
local infix `s'`:50 := s
local infix `t'`:50 := t
variables {a b c d : ℕ}

@[trans] lemma rrr.trans {a b c : ℕ} : r a b → r b c → r a c := sorry
@[trans] lemma srr.trans {a b c : ℕ} : s a b → r b c → r a c := sorry
@[trans] lemma sts.trans {a b c : ℕ} : s a b → t b c → s a c := sorry
@[trans] lemma rss.trans {a b c : ℕ} : r a b → s b c → r a c := sorry
@[trans] lemma trs.trans {a b c : ℕ} : t a b → r b c → s a c := sorry

lemma L1 (h₁ : s a b) (h₂ : t b c) (h₃ : r c d) : r a d :=
calc a s' b : h₁
   ... t' c : h₂
   ... r' d : h₃

lemma L2 (h₁ : r a b) (h₂ : s b c) (h₃ : t c d) : r a d :=
calc a r' b : h₁
   ... s' c : h₂
   ... t' d : h₃

lemma L2' (h₁ : r a b) (h₂ : s b c) (h₃ : t c d) : r a d :=
rss.trans h₁ (sts.trans h₂ h₃)

lemma L3 {a b c : ℕ} (h₁ : t a b) (h₂ : r b c) : s a c :=
calc a t' b : h₁
   ... r' c : h₂

[Kevin Buzzard]

Thanks for checking. That was one way of doing it. The other way is to read the source code, but I sort-of suspect (perhaps incorrectly) that it will be in C++ not Lean.