Zulip Chat Archive

Stream: new members

Topic: Prove using the defn


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.

Johan Commelin (Sep 24 2020 at 08:22):

What's the P doing in your hyps?

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

Lucas Allen (Sep 24 2020 at 08:25):

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

Johan Commelin (Sep 24 2020 at 08:25):

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

Johan Commelin (Sep 24 2020 at 08:26):

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

Lucas Allen (Sep 24 2020 at 08:31):

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

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

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

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

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: Dec 20 2023 at 11:08 UTC