Simplification

This group of tactic aims to reduce the complexity of terms in a goal. They will not solve a goal, only convert it into what is a structurally smaller (although maybe not lexically smaller!) form of the original goal.

simpl

simpl evaluates terms that are constructed of constant values - not variables. simpl can also partially evaluate partially-constant values.

Syntax

(* Simplify the goal as much as possible *)
simpl.

(* Simplify a hypothesis *)
simpl in H.

(* Simplify in the entire proof state *)
simpl in *.

(* Only simplify a specific term in a specific hypothesis *)
simpl (2 + 2) in H.

Examples

Before

-------------------------
1/1
2 + 2 = 1 + 3

simpl (2 + 2).

After

-------------------------
1/1
4 = 1 + 3

Resources

Reference Documentation

---

unfold

unfold replaces definition identifiers with the definition’s contents, simplifying along the way.

Syntax

(* Simple example *)
unfold plus.

(* Unfolding a definition in a hypothesis *)
unfold X in H.

(* Unfolding a definition in all hypotheses and the goal *)
unfold X in *.

Examples

Given

Fixpoint bitlist (n : nat) : list bool :=
    match n with
    | O =>    true  :: nil
    | S n' => false :: (bitlist n')
    end.

Before

n: nat
l: list bool
H: bitlist (S (S n)) = false :: false :: l
-------------------------
1/1
bitlist (S n) = false :: l

unfold bitlist in *.

After

n: nat
l: list bool
H: false
     :: false
        :: (fix bitlist (n : nat) : list bool :=
              match n with
              | 0 => true :: nil
              | S n' => false :: bitlist n'
              end) n =
    false :: false :: l
-------------------------
1/1
false
 :: (fix bitlist (n0 : nat) : list bool :=
       match n0 with
       | 0 => true :: nil
       | S n' => false :: bitlist n'
       end) n = false :: l

Resources

Reference Documentation

---

---