Search code examples
theorem-provinglean

Induction issue

I have defined a type of trees, together with a fusion operation as follows:

open nat

inductive tree : Type
| lf : tree
| nd : tree -> nat -> tree -> tree

open tree

def fusion : tree -> tree -> tree
| lf t2 := t2
| (nd l1 x1 r1) lf := (nd l1 x1 r1)
| (nd l1 x1 r1) (nd l2 x2 r2) :=
    if x1 <= x2
    then nd (fusion r1 (nd l2 x2 r2)) x1 l1
    else nd (fusion (nd l1 x1 r1) r2) x2 l2

Then, I have a counting function which returns the number of occurrences of a given integer in a tree:

def occ : nat -> tree -> nat
| _ lf := 0
| y (nd g x d) := (occ y g) + (occ y d) + (if x = y then 1 else 0)

I want to prove that (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2), but in the course of the proof, I have a problem as I don't know how to deal with the given induction hypotheses.

So far, I have come up to this:

theorem q5 : ∀ (x : ℕ) (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2) :=
begin
    intros x t1 t2,
    induction t1 with g1 x1 d1 _ ih1,
    simp [fusion, occ],
    induction t2 with g2 x2 d2 _ ih2,
    simp [fusion, occ],
    by_cases x1 <= x2,
    simp [fusion, h, occ],
    rw ih1,
    simp [occ, fusion, h],
    simp [occ, fusion, h],
end

but I'm desperately stuck. The ih deals with fusion d1 (nd g2 x2 d2)) while I want something about fusion (nd g1 x1 d1) d2.

I'll gladly welcome any suggestion.

Solution

  • The easiest approach to this question is to prove using the equation compiler using the same pattern match that you defined the function fusion with

    theorem q5 (x : ℕ) : ∀ (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2)
| lf t2 := by simp [fusion, occ]
| (nd l1 x1 r1) lf := by simp [fusion, occ]
| (nd l1 x1 r1) (nd l2 x2 r2) := 
begin
  simp only [fusion, occ],
  by_cases hx12 : x1 ≤ x2,
  { rw [if_pos hx12],
    simp only [fusion, occ],
    rw q5,
    simp [occ] },
  { rw if_neg hx12,
    simp only [fusion, occ],
    rw q5,
    simp [occ] }
end

    An alternative approach is

    theorem q5 : ∀ (x : ℕ) (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2) :=
begin
  intros x t1,
  induction t1 with g1 x1 d1 _ ih1,
  { simp [fusion, occ] },
  { assume t2,
    induction t2 with g2 x2 d2 _ ih2,
    simp [fusion, occ],
    by_cases x1 <= x2,
    { simp [fusion, h, occ, ih1] },
    { simp [occ, fusion, h, ih2] } },
end

    The problem with your approach is that rw ih2 is possible at the end of your proof but generates two difficult to prove subgoals due to the hypotheses before the induction hypothesis.

    A solution to this is to change the first induction hypothesis. There is no intro t2 before the induction in my second proof. That way the induction hypothesis is stronger for the first induction, because starts with ∀ t2.

    Whenever you do induction on a variable t2, every hypothesis mentioning t2 is automatically added as an assumption before your induction hypothesis.

    In your cases, the induction hypotheses for the first induction mention t2, so you end up with an awkward induction hypothesis for the second hypothesis.

    However, my induction hypotheses for the first induction start with ∀ t2, so they are not about my local constant t2, so they are not added to the induction hypothesis for the second induction, so I have a more useful induction hypothesis.

    There is usually no downside to giving yourself the most powerful induction hypothesis like this, by generalizing it ∀ t2. This is why it is the default way that the equation compiler generates induction hypotheses.