Zulip Chat Archive

Stream: general

Topic: reflexive-transitive closure and recursion


view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 15:47):

Lean has a transitive closure but I want a reflexive-transitive one. So I wrote the following definition:

variable {D : Type}
variable R : D -> D -> Prop

inductive rtc : D -> D -> Prop
| refl :  s, rtc s s
| step :  (s u t), R s u  rtc u t  rtc s t

I was happy that without knowing much Lean upfront, I was able to prove a simple theorem.

theorem rtc_trans : forall (s u t : D), rtc R s u -> rtc R u t -> rtc R s t :=
  begin
    intros s u t H1 H2, induction H1, { exact H2 },
    { apply rtc.step, apply H1_a, apply H1_ih, apply H2 }
  end

The proof utilizes rtc.drec. Which is fine. But it would be very illustrative to carry out the same proof via a recursive definition. This, however, requires a match, and I was not able to destructure rtc R s t in any way:

def hmm (s t : D) (H : rtc R s t) : true :=
  match H with
  | rtc.refl _ _ := true.intro
  | rtc.step R u _ su ut := λ h, true.intro

This fails to typecheck because rtc.refl _ _ gets the type rtc R _x _x, which does not unify with rtc R s t. While the error message sounds reasonable, it sounds weird that there is an inductive type that cannot be matched on. Is there any way around that?

view this post on Zulip Kenny Lau (Jun 12 2018 at 15:52):

put the hypothesis after the colon and use the equation compiler instead of match

view this post on Zulip Kenny Lau (Jun 12 2018 at 15:52):

put everything after the colon

view this post on Zulip Johannes Hölzl (Jun 12 2018 at 15:53):

In mahlib we have the reflexive transitive closure: https://github.com/leanprover/mathlib/blob/master/logic/relation.lean#L61

view this post on Zulip Johannes Hölzl (Jun 12 2018 at 15:55):

match can do cases on rtc but you need to give it the allowance, e.g. one of s and t in rtc s t should be a variable, and you need to pass this variable into match so that it can change it, a.l.a match s, h : rtc s t where _, rtc.refl _ := ... end

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:23):

Thanks... I know nothing about the equation compiler and I am still struggling with dependent match but at least fixing one side of the rtc to a variable makes sense to me. I am trying to encode a system that has both unfolding rules --- one that unfolds the first step of the path, and one that unfolds the last step. I will probably define those as two inductive Props and prove their equivalence.

What is the meaning of the refl constructor having an empty implicit parameter list {}?

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:27):

it is an instruction to lean to infer the implicit argument from the return type

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:27):

consider

inductive sum (α : Type u) (β : Type v)
| inl {} : α  sum
| inr {} : β  sum

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:27):

here the empty implicit parameter list is an annotation to infer the type alpha in inl and beta in inr

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:31):

hrm, maybe not the greatest example since the definition goes through without the brackets anyway...

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:35):

ok, if you paste this

inductive sum' (α β : Type)
| inl : α  sum'
| inr {} : β  sum'

#print sum'

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:35):

then you'll see a difference in how lean evaluates the expression

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:36):

Ok, so in fact the {} is for beta in inl (since alpha is already there).

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:37):

oops, haha

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:37):

yes

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:37):

How does Lean know that alpha has to be implicit, in inl without the {}?

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:38):

Oh silly me, of course the first parameter is of type alpha.

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:43):

Ok, this was immaterial to the discussion of matches, back to struggling with match s, h : rtc R s t then. Can anyone explain that cryptic line above?

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 22:53):

I didn't manage to put the type annotation H : rtc R s t but the match seemed to work even without it, by virtue of having s available to the equation compiler perhaps?

def hmm (s t : D) (H : rtc R s t) : true :=
  match s, H with
  | _, rtc.refl := fun h, trivial
  | _, rtc.step _ _ _ := fun h, trivial

I am a bit perplexed still by the fact that the match branches have type ?? -> true rather than just true...

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 22:59):

if you had to write out the definition by hand using rtc.drec_on or rtc.rec_on, how would you avoid the first argument? (match uses those under the hood iirc, but somebody correct me if I'm mistaken)

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 23:00):

def hmm' (s t : D) (H : rtc R s t) : true :=
rtc.rec_on H
  (λ _, true.intro)
  (by intros; exact true.intro)

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 23:05):

Yes, it looks like it does — it just clashes somehow with my understanding of Type Theory and CIC (where there is a fix construct).

view this post on Zulip Shachar Itzhaky (Jun 12 2018 at 23:09):

BTW the compiler seems to make quite a monster out of my small match:

def ReflexiveTransitiveClosure.hmm._match_1 :  {D : Type} (R : D  D  Prop) (t _a : D), rtc R _a t  true :=
λ {D : Type} (R : D  D  Prop) (t _a : D) (_a_1 : rtc R _a t),
  rtc.dcases_on _a_1
    (λ (H_1 : t = _a), eq.rec (λ (_a : rtc R t t) (H_2 : _a == rtc.refl), id_rhs true trivial) H_1 _a_1)
    (λ (u : D) {t_2 : D} (a : rtc R _a u) (a_1 : R u t_2) (H_1 : t = t_2),
       eq.rec (λ (a_1 : R u t) (H_2 : _a_1 == rtc.step u a a_1), id_rhs true trivial) H_1 a_1)
    (eq.refl t)
    (heq.refl _a_1)

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 23:13):

i don't know if this is any prettier to you

def hmm' :  (s t : D) (H : rtc R s t), true
| _ _ (rtc.refl _ _ ) := true.intro
| _ _ (rtc.step _ _ _ _ _) := true.intro

#print hmm'._main

view this post on Zulip Andrew Ashworth (Jun 12 2018 at 23:16):

when I want a definition that unfolds nicely I tend to write it out by hand using the appropriate recursion lemma. If you use the equation compiler as I did above, the main def is somewhat ugly but it generates quite nice ._eqn1, ._eqn2 branches

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 08:04):

Yes, I ended up doing that myself, eventually. I found hmm'._main but what are ._eqn1, ._eqn2?

At any rate, the purpose of this mental exercise was to demonstrate that explicit induction and "normal" recursion coincide, so of course I could write it with rec_on but that would miss the point...

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:20):

You can try #print prefix hmm' to see everything starting hmm'.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:20):

although in the back of my mind I think there might be an easier way of just seeing the equation lemmas...

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 10:52):

I somehow get no declaration starting with prefix 'hmm''.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:56):

In lean, type ascriptions have required parentheses, it should be (H : rtc R s t) not H : rtc R s t

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 10:58):

I was convinced I tried that when the original suggestion didn't work... but yeah, parenthesis do the trick! Although, as I said, the definition goes through without the ascription as well.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 10:58):

Lean is a bit limited in its ability to do induction on inductive predicates using the equation compiler. I recommend using the induction tactic instead if you have any problems with writing it the way Andrew suggested

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 10:59):

Yes, I will reiterate: using tactic mode as well as rec_on were pretty smooth. The reason I am in this discussion is that I wanted to demonstrate to my students how induction is just a form of recursion that they know from programming.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 11:00):

I usually point at the type of rec_on, remark that it looks a lot like induction, and then use it to define a recursive function and also prove some property about it

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 11:01):

:thumbs_up: I assume this is "the Lean way" then.

view this post on Zulip Mario Carneiro (Jun 13 2018 at 11:03):

In the case of an inductive predicate like rtc, it actually can't be used for recursion, since it has small elimination

view this post on Zulip Mario Carneiro (Jun 13 2018 at 11:03):

it can only be used to prove props

view this post on Zulip Mario Carneiro (Jun 13 2018 at 11:04):

If you put the inductive type in Type though it could

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 11:05):

Of course. The analogue that I can refer to is that in Coq I wrote the same proof, once with induction, and once with Fixpoint -- of course, since you destructure the Prop inside the def, the function must return a Prop.

view this post on Zulip Shachar Itzhaky (Jun 13 2018 at 11:05):

I still see that as a form of recursion though, since it's expressed via Fixpoint.


Last updated: May 13 2021 at 19:20 UTC