Guidance on proof methods: pattern matching vs. induction

Stream: new members

[Newell Jensen]

Questions/guidance on proof methods

I am trying to prove that the boolean AND of two boolean palindromes of the same length are also a palindrome.

I feel a bit lost with the proof method because I am unsure if I am even using the best approach or if there are other approaches that would be better for the way I have things set up. That being said, if there is a better way to set things up I am also interested in what people have to say.

Some uncertainties I have are:

1. Should I define List.And differently to make this type of proof easier?
2. Instead of pattern matching on the boolean lists A and B, should I be pattern matching on something else? Should I be pattern matching at all?
3. If not pattern matching, is using induction in some form or another a better method? Why?

The idea for the proof that I am trying here is pattern matching and then would like to try and show that since A and B are boolean palindromes of the same length then both ends of these lists are the same, making the boolean AND of both the ends also the same.

Here is what I have so far:

import Mathlib.Tactic
import Mathlib.Data.List.Palindrome

open List

def List.And : List Bool → List Bool → List Bool
  | [], [] => []
  | _, [] => []
  | [], _ => []
  | a::as, b::bs => (a && b) :: List.And as bs

#eval List.And [] [true, true] -- []
#eval List.And [true, false] [true, true] -- [true, false]
#eval List.And [true, false] [true, true, false] -- [true, false]
#eval Palindrome <| List.And [true] [false] -- true
#eval Palindrome <| List.And [true,true] [false,false] -- true
#eval Palindrome <| List.And [true,false,true] [false,true,false] -- true
#eval Palindrome <| List.And [true,true,true] [false,true,true] -- false

theorem reverse_eq' {A B : List Bool} (p : Palindrome (List.And A B))
    : reverse (List.And A B) = List.And A B := by
  exact Palindrome.reverse_eq p

theorem of_reverse_eq' {A B : List Bool} : reverse (List.And A B) = (List.And A B) → Palindrome (List.And A B) := by
  exact Palindrome.of_reverse_eq

theorem iff_reverse_eq' {A B : List Bool} : Palindrome (List.And A B) ↔ reverse (List.And A B) = List.And A B :=
  Iff.intro reverse_eq' of_reverse_eq'

lemma bool_palindrome_and_bool_palindrome_is_palindrome {A B : List Bool} (h : A.length = B.length)
   : Palindrome A → Palindrome B → Palindrome (List.And A B) := by
  intro hA hB
  match A, B with
  | [], [] => simp
  | A, []  =>
    have h1 : A = [] := Iff.mp length_eq_zero h
    rw [h1]; simp
  | [], B =>
    have h2 : B = [] := Iff.mp length_eq_zero (id (Eq.symm h))
    rw [h2]; simp
  | a::as, b::bs =>
    have h3 : (a::as) ≠ [] := cons_ne_nil a as
    have h4 : (b::bs) ≠ [] := cons_ne_nil b bs
    by_cases hn : as = [] ∧ bs = []
    · -- as = [] ∧ bs = []
      have h5 : (a::as) = (a::[]) := congrArg (cons a) hn.1
      have h6 : (b::bs) = (b::[]) := congrArg (cons b) hn.2
      rw [h5, h6]
      exact of_reverse_eq' rfl
    · -- as ≠ [] ∨ bs ≠ []
      rw [not_and_or] at hn; push_neg at hn
      rcases hn with (hn1 | hn2)
      · sorry
      · sorry

[Damiano Testa]

I'm not at a computer, so my suggestions will be very coarse. I think that List.And is List.zipWith (And \. \.) _ _ (docs#List.zipWith).

Also, do you really need to do all the trivial cases separately? Couldn't you do the cons, cons case first and then lump together all the rest in a single case?

[Newell Jensen]

Yes, List.zipWith (and \. \.) _ _ does replace what I have for List.And.

In terms of making the proof more concise, yes I probably can do something as you mention with cons, cons. I am more interested in seeing what the preferred proof method is between pattern matching, induction, or some other way.

For example, I tried a bunch of different things such as regular induction and bidirectionalRecOn etc. but I kept running into the issue that I need to be able to iterate over A and B (at least afaict).

[Newell Jensen]

So I have thought about this some more and this question is probably rather trivial for most of the bright minds here. This is what I have come up with (which in hindsight I feel I should have known but sometimes asking stupid questions will make you realize it faster) as a rule of thumb, which may be helpful to any other beginners who come upon this in the future:

1. Pattern matching is basically doing cases on inductive types in your hypothesis during the proof.
2. If you need an actual induction step in your proof, use induction or one its variants. Which one is best for you will depend on the proof at hand.

Basically main difference between the two is the induction step since cases deconstructs the inductive data types just like we get with induction, but with induction we get that added induction hypothesis to help us with the induction step if needed.

[Henrik Böving]

There is no actual difference between pattern matching and induction. You can emulate induction with the cases tactic by doing a recursive call to your theorem and calling the resulting value ih

theorem Nat.example_zero_add (n : Nat) : 0 + n = n := by
  cases n with
  | zero => rfl
  | succ m =>
    let ih := Nat.example_zero_add m
    rw[Nat.add_succ]
    rw[ih]

induction basically "just" automates this concept for you by using a certain kind of induction scheme (and it has a default one that is automatically generated for each inductive type). That said if you are not willing to come up with the generalized scheme for the proof that you are doing you can still just resolve to using a case + recursive call.

[Newell Jensen]

@Henrik Böving thanks for the response. In addition, the example you gave, from what I understand, is strong or complete induction, correct?

[Henrik Böving]

I guess you can call it that if you want to yes.