Zulip Chat Archive

Stream: new members

Topic: Prove using the defn


view this post on Zulip Lucas Allen (Sep 24 2020 at 08:20):

This is maybe a silly question but I'm stuck. I have

def sub_Q' : list   list   list 
| P      []     := P
| []     Q      := []
| (h::t) (a::b) := (h - a) :: sub_Q' t b

lemma xxx (P Q : list ) : sub_Q' [] Q = [] :=
begin
  sorry
end

How do I prove xxx ? It's true by definition. I've tried rfl, refl, unfold sub_Q', and dsimp [sub_Q'], none of which work. I thought relf would work because of the computation thing.

view this post on Zulip Johan Commelin (Sep 24 2020 at 08:22):

What's the P doing in your hyps?

view this post on Zulip Lucas Allen (Sep 24 2020 at 08:24):

It part of a larger lemma, I really want to prove

lemma wtf (P Q : list ) : (sub_Q' P Q).length = P.length :=
begin
  sorry
end

view this post on Zulip Lucas Allen (Sep 24 2020 at 08:25):

Removing the P in the example doesn't help :(

view this post on Zulip Johan Commelin (Sep 24 2020 at 08:25):

lemma xxx :  (Q : list ), sub_Q' [] Q = []
| [] := rfl
| (h::t) := rfl

view this post on Zulip Johan Commelin (Sep 24 2020 at 08:26):

I dunno why lean isn't being smarter so that rfl works right away.

view this post on Zulip Lucas Allen (Sep 24 2020 at 08:31):

Yeah, I though it'd just work. Thanks for the solution.

view this post on Zulip Kenny Lau (Sep 24 2020 at 08:36):

If you do #print prefix sub_Q', you will see the computation rules:

sub_Q'.equations._eqn_1 : sub_Q' list.nil list.nil = list.nil
sub_Q'.equations._eqn_2 :  (hd : ) (tl : list ), sub_Q' list.nil (hd :: tl) = list.nil
sub_Q'.equations._eqn_3 :  (hd : ) (tl : list ), sub_Q' (hd :: tl) list.nil = hd :: tl
sub_Q'.equations._eqn_4 :  (h : ) (t : list ) (a : ) (b : list ), sub_Q' (h :: t) (a :: b) = (h - a) :: sub_Q' t b

view this post on Zulip Kenny Lau (Sep 24 2020 at 08:37):

since you did cases on the second input when defining the function, there is no computational rule where the second input is not destructed

view this post on Zulip Lucas Allen (Sep 24 2020 at 08:44):

Ohhhh.... I see thanks. :)

lemma xxx (P Q : list ) : sub_Q' [] Q = [] :=
begin
  cases Q, refl, refl,
end

view this post on Zulip Kevin Buzzard (Sep 24 2020 at 08:46):

This is a standard equation compiler gotcha but it's difficult to know where to flag the issue


Last updated: May 14 2021 at 02:15 UTC