CODEWITHSUNDEEP
coq
geckos
geckos

Reputation: 6289

How to generalize a variable on both sides of an equation in Coq?

I have this goal

size (flatten (N t1 t2)) = size (N t1 t2)

N is a bin constructor, how can I replace N t1 t2 in both sides by t3 : bin?

My hypothesis are

t1, t2 : bin
IHt1 : size (flatten t1) = size t1
IHt2 : size (flatten t2) = size t2

If I can rewrite size (flatten (N t1 t2)) = size (N t1 t2) as size (flatten t3) = size t3 then I can apply my hypothesis to finish the proof.

Here is the full code

Require Import Nat.
Require Import Arith.

Inductive bin : Type :=
    L : bin
  | N : bin -> bin -> bin.

Fixpoint flatten_aux (t1 t2 : bin) : bin :=
  match t1 with
    L => N L t2
  | N t'1 t'2 => flatten_aux t'1  (flatten_aux t'2 t2)
  end.

Fixpoint flatten (t : bin) : bin :=
  match t with
    L => L
  | N t1 t2 => flatten_aux t1 (flatten t2)
  end.

Fixpoint size (t : bin) : nat :=
  match t with
    L => 1
  | N t1 t2 => 1 + size t1 + size t2
  end.


Lemma flatten_aux_size :
  forall t1 t2, size (flatten_aux t1 t2) =
    size t1 + size t2 + 1.
  induction t1.
  { intros t2.
    simpl.
    ring.
  }
  { intros t2; simpl.
    rewrite IHt1_1.
    rewrite IHt1_2.
    ring.
  }
Qed.

Lemma flatten_size : forall t, size (flatten t) = size t.
  induction t.
  { trivial.
  }
  { simpl.
    (* goal size (flatten (N t1 t2)) = size (N t1 t2) *)

In the end I use this solution

Lemma flatten_size : forall t, size (flatten t) = size t.
  induction t.
  { trivial.
  }
  { simpl.
    rewrite flatten_aux_size.
    rewrite <- IHt1.
    rewrite <- IHt2.
    rewrite Nat.add_comm.
    simpl.
    reflexivity.
  }
Qed.

Upvotes: 1

Views: 169

Answers (2)

Lolo
Lolo

Reputation: 649

you did the right thing using simpl : it partially evaluates size (flatten (N t1 t2)) and size (N t1 t2) so you can use your induction hypothesis.

Upvotes: 0

Th&#233;o Winterhalter
Th&#233;o Winterhalter

Reputation: 5108

Why would you have size (flatten t3) = size t3? Your hypotheses are not universally quantified, size (flatten t2) = size t2 holds for that particular t2 (same with t1). Without more details we cannot help you but I would expect that you rather show how flatten behaves when applied to N t1 t2 in terms of flatten t1 and flatten t2 which would then help you conclude.

Upvotes: 3

Related Questions