## 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: May 14 2021 at 02:15 UTC