## Stream: general

### Topic: cc is so powerful

#### Kenny Lau (Apr 21 2018 at 13:42):

cc resolved the following:

x1 : α,
b1 : bool,
x2 : α,
b2 : bool,
H2 : (x1, b1) ≠ (x2, b2),
L : list (α × bool),
H3 : L = (x1, b1) :: L₃,
H4 : L = (x2, b2) :: L₄
⊢ red L₃ ((x1, bnot b1) :: L)


which makes me wonder how cc works

#### Kenny Lau (Apr 21 2018 at 13:42):

The docs say that it attempts to synthesize an empty inductive type

#### Kenny Lau (Apr 21 2018 at 13:43):

but it doesn't say how it achieves it

#### Kenny Lau (Apr 21 2018 at 13:43):

the printed theorem says:

false.elim
(false_of_true_eq_false
(eq.trans
(eq.symm
(eq_true_intro
(and.elim_left
(list.no_confusion (eq.trans (eq.symm H3) H4)
(λ (hd_eq : (x1, b1) = (x2, b2)) (tl_eq : L₃ = L₄), ⟨hd_eq, tl_eq⟩)))))
(eq_false_intro H2))))


#### Simon Hudon (Apr 21 2018 at 13:53):

I think it does so by building an equality matching graph. It's a graph where the vertices are terms and they are linked by edges if they are known to be equal. Once you've added all the equalities in your context, you take the transitive closure of the graph and, for each connected component (i.e. equivalence class) you can elect a term that will represent the whole class and replace every occurrence of every member of that class by that one representative.

#### Simon Hudon (Apr 21 2018 at 13:53):

It's a very algorithmic proof technique

very interesting

#### Kenny Lau (Apr 21 2018 at 13:53):

but the transitive closure isn't necessarily decidable?

#### Simon Hudon (Apr 21 2018 at 13:54):

It is because you're only considering the finite set of terms that are visible in your context (and some variation on each)

hmm

#### Gabriel Ebner (Apr 21 2018 at 14:06):

@Simon Hudon Congruence closure does one more thing: it closes these equivalences under congruence. For example if you know a=b and have two subterms f a and f b, then it will deduce f a = f b.

#### Kenny Lau (Apr 21 2018 at 14:07):

is there any paper regarding this?

#### Simon Hudon (Apr 21 2018 at 14:08):

Thanks for adding this detail! I could only think of it in algorithmic terms and that didn't seem enlightening. But your explanation is nice

#### Gabriel Ebner (Apr 21 2018 at 14:08):

I don't know a canonical citation off the top of my head, it's pretty standard stuff. Give me a sec.

thanks

#### Gabriel Ebner (Apr 21 2018 at 14:09):

Nelson, Oppen, Fast decision procedures based on congruence closure, Journal of the ACM (1980) http://www.cs.colorado.edu/~bec/courses/csci5535-s09/reading/nelson-oppen-congruence.pdf

#### Gabriel Ebner (Apr 21 2018 at 14:10):

The congruence lemmas for dependent type theory as used in Lean are described in this paper (de Moura, Selsam IJCAR 2016): https://leanprover.github.io/papers/congr.pdf

#### Patrick Massot (Apr 21 2018 at 14:11):

I'm always hesitant to try to read Lean papers because I always fear they will be outdated (say Lean 2 era or worse) and only confuse me

#### Gabriel Ebner (Apr 21 2018 at 14:11):

The cc implementation in Lean does a few more tricks: for example it derives a=b from nat.succ a = nat.succ b, and nat.succ a != nat.zero for any a.

#### Patrick Massot (Apr 21 2018 at 14:12):

Do you have something like a list of still relevant Lean papers?

#### Kenny Lau (Apr 21 2018 at 14:12):

theorem test (α : Type*) (f : α → α) (x : α)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x :=
by cc

#print test
/-of_eq_true
(eq_true_intro
(eq.trans
(eq_of_heq
((λ (a a' : α) (e_0 : a = a'), eq.rec (heq.refl (f a)) e_0) x (f (f x))
(eq.trans (eq.symm H2)
(eq_of_heq
((λ (a a' : α) (e_0 : a = a'), eq.rec (heq.refl (f a)) e_0) (f (f (f (f x)))) (f x)
(eq_of_heq
((λ (a a' : α) (e_0 : a = a'), eq.rec (heq.refl (f a)) e_0) (f (f (f x))) x H1)))))))
H1))-/


Wow

#### Kenny Lau (Apr 21 2018 at 14:13):

(taken from P.1 of the first linked paper)

#### Gabriel Ebner (Apr 21 2018 at 14:16):

@Patrick Massot Let me look through the publication list at https://leanprover.github.io/publications/. The system description is pretty high-level and only obsolete in details. The metaprogramming paper is new and describes Lean 3.2. The machine learning paper doesn't seem to talk much about Lean. The congruence closure paper seems to be still relevant. The elaboration paper is completely obsolete as it describes Lean 2.

#### Kenny Lau (Apr 21 2018 at 14:16):

The congruence lemmas for dependent type theory as used in Lean are described in this paper (de Moura, Selsam IJCAR 2016): https://leanprover.github.io/papers/congr.pdf

of course it is de moura :P

Thanks

#### Patrick Massot (Apr 21 2018 at 14:23):

So actually the obsolete one is clearly flagged Lean 2 on https://leanprover.github.io/publications/

#### Patrick Massot (Apr 21 2018 at 14:24):

It reminds me a question: what is the status of super today?

#### Patrick Massot (Apr 21 2018 at 14:27):

And these crush things mentioned in the metaprogramming paper and some slides?

#### Gabriel Ebner (Apr 21 2018 at 14:30):

super never progressed beyond a proof of concept. From my point of view, the main thing holding it back is performance. Some APIs that would be very nice to do e.g. resolution with unification (such as temporary metavariables) are simply not available from the metaprogramming side. And I have enough other things to do. Maybe I will revisit super when Lean 4 arrives.

#### Gabriel Ebner (Apr 21 2018 at 14:31):

crush is available as a package: https://github.com/leanprover/mini_crush

#### Gabriel Ebner (Apr 21 2018 at 14:31):

rsimp is in the core library

#### Simon Hudon (Apr 21 2018 at 14:32):

What does rsimp do?

#### Gabriel Ebner (Apr 21 2018 at 14:33):

Re: super. This was the first thing I did with Lean, and at the time I did not know about typeclasses, simp lemmas, the equation compiler, etc. It did not help that the Lean 3 library at the time did not even have more than a few theorems about natural numbers.

#### Gabriel Ebner (Apr 21 2018 at 14:35):

@Simon Hudon: rsimp is Leo's idea on how to do simplification with congruence closure. As you've observed, cc stores the equivalence classes of subterms. Roughly, rsimp then applies simp lemmas on the subterms, and traverses the equivalence classes to pick the smallest subterm as a result.

#### Gabriel Ebner (Apr 21 2018 at 14:37):

The main advantage compared to simp is that it doesn't loop (so easily). For example, simp* would loop on a=b, b=a :- f a = f b but rsimp would not.

#### Kenny Lau (Apr 21 2018 at 14:37):

why would it not loop on a=b b=a?

#### Simon Hudon (Apr 21 2018 at 14:38):

That is so cool :) Is there a downside to using rsimp instead of simp?

#### Gabriel Ebner (Apr 21 2018 at 14:41):

Just looked back at the paper and apparently I remembered it incorrectly, rsimp uses E-matching to instantiate lemmas instead of simp. So in the example above, rsimp is essentially cc.

#### Patrick Massot (Apr 21 2018 at 14:41):

Thanks. Indeed it sounds like super needs to wait for Lean 4.

#### Gabriel Ebner (Apr 21 2018 at 14:42):

Maybe more interestingly: if you call rsimp on a=b, a=f a :- p (f (f a)) then rsimp would simplify the goal to p a (or p b, randomly).

#### Kenny Lau (Apr 21 2018 at 14:43):

I found that cc automatically does intros

#### Kenny Lau (Apr 21 2018 at 14:43):

I was wondering if it rewrote the conditions like simp does

#### Kenny Lau (Apr 21 2018 at 14:44):

I think that's less efficient so I don't prefer it rewriting the conditions

#### Kenny Lau (Apr 21 2018 at 14:44):

so I like cc more :P

#### Gabriel Ebner (Apr 21 2018 at 14:44):

I was wondering if it rewrote the conditions like simp does

What do mean by "rewriting conditions"?

#### Kenny Lau (Apr 21 2018 at 14:44):

so the goal is A -> B

#### Kenny Lau (Apr 21 2018 at 14:44):

simp would rewrite A to C without intro right

#### Gabriel Ebner (Apr 21 2018 at 14:49):

I'm not sure if there is a meaningful difference in efficiency here. The reason why simp does not do intros is because simp may not close the goal and you don't want simp to intro stuff randomly. On the other hand, cc is an end-game tactic and can do whatever it wants.

#### Kenny Lau (Apr 21 2018 at 14:50):

I see

Last updated: May 07 2021 at 00:30 UTC