Binary tree inversion in Coq

Question

I'm trying to prove that inverting a binary tree twice produces the same binary tree.

So I have written the following inductive type:

Inductive tree : Type :=
| Leaf (x : Type)
| Node (t1 : tree) (t2 : tree).

And here's the inversion function:

Fixpoint invertTree (t : tree) :=
  match t with
  | Leaf x => Leaf x
  | Node l r => Node (invertTree r) (invertTree l)
  end.

The theorem is pretty simple:

Theorem involution_of_invert : forall t : tree,
    (invertTree (invertTree t)) = t.

The base case is pretty easy to prove, we start with a proof by induction and just compute -> reflexivity. I'm having a hard time understanding the induction step. Here's as far as I got:

Proof.
  induction t.
  compute.
  reflexivity.
  induction t1, t2.
  compute.
  reflexivity.

And my remaining goals:

3 subgoals (ID 57)
  
  x : Type
  t2_1, t2_2 : tree
  IHt1 : invertTree (invertTree (Leaf x)) = Leaf x
  IHt2 : invertTree (invertTree (Node t2_1 t2_2)) = Node t2_1 t2_2
  ============================
  invertTree (invertTree (Node (Leaf x) (Node t2_1 t2_2))) =
  Node (Leaf x) (Node t2_1 t2_2)

subgoal 2 (ID 74) is:
 invertTree (invertTree (Node (Node t1_1 t1_2) (Leaf x))) =
 Node (Node t1_1 t1_2) (Leaf x)
subgoal 3 (ID 81) is:
 invertTree (invertTree (Node (Node t1_1 t1_2) (Node t2_1 t2_2))) =
 Node (Node t1_1 t1_2) (Node t2_1 t2_2)

Would be glad if any hint could be provided. I'm pretty new to Coq (as should be pretty clear from the question heh).

Thanks

Using induction on variables while you already have an induction hypothesis seems like something very weird to do, and indeed removing this step works out, as you found. — Meven Lennon-Bertrand

Felipe Balbi Felipe Balbi · Accepted Answer · 2021-09-13T20:22:18

Found a solution to this, here it is:

Inductive tree : Type :=
| Leaf (x : Type)
| Node (t1 : tree) (t2 : tree).

Fixpoint invertTree (t : tree) :=
  match t with
  | Leaf x => Leaf x
  | Node l r => Node (invertTree r) (invertTree l)
  end.

Theorem involution_of_invert : forall t : tree,
    (invertTree (invertTree t)) = t.
Proof.
  induction t.
  compute.
  reflexivity.
  simpl.
  rewrite -> IHt1.
  rewrite -> IHt2.
  reflexivity.
Qed.

Binary tree inversion in Coq

1 Answers