Prove using the defn

Stream: new members

[Lucas Allen]

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]

What's the P doing in your hyps?

[Lucas Allen]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Lucas Allen]

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

[Kenny Lau]

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]

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]

Ohhhh.... I see thanks. :)

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

[Kevin Buzzard]

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