Zulip Chat Archive

Stream: general

Topic: cc is so powerful


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 13:42):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 13:43):

but it doesn't say how it achieves it

view this post on Zulip 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))))

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 21 2018 at 13:53):

It's a very algorithmic proof technique

view this post on Zulip Kenny Lau (Apr 21 2018 at 13:53):

very interesting

view this post on Zulip Kenny Lau (Apr 21 2018 at 13:53):

but the transitive closure isn't necessarily decidable?

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 21 2018 at 13:54):

hmm

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:07):

is there any paper regarding this?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:09):

thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:12):

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

view this post on Zulip 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))-/

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:13):

Wow

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:13):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:22):

Thanks

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:23):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:24):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:27):

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

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Apr 21 2018 at 14:31):

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

view this post on Zulip Gabriel Ebner (Apr 21 2018 at 14:31):

rsimp is in the core library

view this post on Zulip Simon Hudon (Apr 21 2018 at 14:32):

What does rsimp do?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:37):

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

view this post on Zulip Simon Hudon (Apr 21 2018 at 14:38):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 21 2018 at 14:41):

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

view this post on Zulip 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).

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:43):

I found that cc automatically does intros

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:43):

I was wondering if it rewrote the conditions like simp does

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:44):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:44):

so I like cc more :P

view this post on Zulip 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"?

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:44):

so the goal is A -> B

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:44):

simp would rewrite A to C without intro right

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 14:50):

I see


Last updated: May 07 2021 at 00:30 UTC