Creating common tactics in Coq from scratch

tactics_from_scratch.v

(* Showing how to create new tactics only using refine *)

Inductive equal {A : Type} (x : A) : A -> Prop := equal_refl : equal x x.

Check equal_refl.

(* equal_refl *)
(*      : forall x : ?A, equal x x *)
(* where *)
(* ?A : [ |- Type] *)

Notation "x '==' y" := (equal x y) (at level 60) : type_scope.
Theorem equal_sym : forall {A} {x y : A}, x == y -> y == x.
Proof.
  refine (fun A x y H => match H with
                      | equal_refl _ => _
                      end).
  refine (equal_refl x).
Qed.

Theorem equal_trans : forall {A} {x y z : A}, x == y -> y == z -> x == z.
Proof.
  refine (fun A x y z H H0 => match H, H0 with
                           | equal_refl _, equal_refl _ => _
                           end).
  refine (equal_refl x).
Qed.

Theorem equal_cong : forall {A B} {x y : A} (f : A -> B), x == y -> f x == f y.
Proof.
  refine (fun A B x y f eqxy => _).
  refine (match eqxy with
          | equal_refl _ => _
          end).
  refine (equal_refl _).
Qed.

(* Let’s introduce some tactics of our own to capture repeated
   patterns *)

Ltac introduce x := refine (fun x => _).
Ltac destruct_equal H := refine (match H with
                                 | equal_refl _ => _
                                 end).

Ltac equal_reflexivity := refine (equal_refl _).

Theorem equal_sym' : forall {A} (x y : A), x == y -> y == x.
Proof.
  introduce A.
  introduce x.
  introduce y.
  introduce H.
  destruct_equal H.
  equal_reflexivity.
Qed.

Ltac introduce1 :=
  match goal with
  | |- _ -> _ => refine (fun x => _)
  end.

Theorem equal_sym'' : forall {A} (x y : A), x == y -> y == x.
Proof.
  introduce1.
  introduce1.
  introduce1.
  introduce1.
  destruct_equal x.
  equal_reflexivity.
Qed.

(* Recursion in ltac *)

Ltac do_nothing := refine _.
(* Keep introducing things until not needed *)
Ltac introduces := (introduce1; introduces) || do_nothing.

Theorem equal_sym''' : forall {A} (x y : A), x == y -> y == x.
Proof.
  introduces.
  destruct_equal x.
  equal_reflexivity.
Qed.

Print nat.
(* Inductive nat : Set :=  O : nat | S : nat -> nat *)

(* Arguments S _%nat_scope *)

(* Induction principle for natural numbers *)
Fixpoint nat_induction
         (P : nat -> Prop) (H0 : P 0) (Hn' : forall n', P n' -> P (S n'))  (n : nat) : P n :=
  match n with
  | 0 => H0
  | S n' => Hn' n' (nat_induction P H0 Hn' n')
  end.

Lemma add_0_r : forall (n : nat), n + 0 == n.
Proof.
  refine (nat_induction _ _ _).
  - equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    refine (equal_cong S IHn').
Qed.

(* tactic for induction *)
Ltac induction_nat := refine (nat_induction _ _ _).

Lemma add_assoc : forall (a b c : nat),  ((a + b) + c) == (a + (b + c)).
Proof.
  induction_nat.
  - introduce b.
    introduce c.
    equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    introduce b.
    introduce c.
    refine (equal_cong S (IHn' _ _)).
Qed.

Lemma add_succ_r : forall (a b : nat), a + S b == S (a + b).
Proof.
  induction_nat.
  - introduce b.
    equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    introduce b.
    refine (equal_cong _ (IHn' _)).
Qed.

Ltac applying H := refine (H _).

Lemma add_comm : forall (a b : nat), a + b == b + a.
Proof.
  introduce a.
  induction_nat.
  - applying add_0_r.
  - introduce n'.
    introduce H.
    refine (equal_trans (add_succ_r _ _) _).
    refine (equal_cong _ H).
Qed.

(* Let’s make a tactic for rewriting stuff *)
(* Rewriting on the left *)
Ltac rewrite_l H := refine (equal_trans H _).
(* Rewriting on the right *)
Ltac rewrite_r H := refine (equal_trans _ H).

Lemma add_comm' : forall (a b : nat), a + b == b + a.
Proof.
  introduce a.
  induction_nat.
  - applying add_0_r.
  - introduce n'.
    introduce H.
    rewrite_l (add_succ_r a n').
    refine (equal_cong _ H).
Qed.

Lemma mul_0_r : forall (a : nat), a * 0 == 0.
Proof.
  induction_nat.
  - equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    rewrite_l IHn'.
    equal_reflexivity.
Qed.

Lemma mul_1_r : forall (a : nat), a * 1 == a.
Proof.
  induction_nat.
  - equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    refine (equal_cong _ IHn').
Qed.

Lemma add_swap : forall (a b c : nat), a + (b + c) == b + (a + c).
Proof.
  introduce a.
  introduce b.
  introduce c.
  refine (equal_sym _).
  rewrite_r (add_assoc a b c).
  refine (equal_sym _).
  rewrite_r (add_assoc b a c).
  rewrite_r (equal_cong (fun x => x + c) (add_comm a b)).
  equal_reflexivity.
Qed.

Lemma mul_succ_r : forall (a b : nat), a * S b == a + a * b.
Proof.
  induction_nat.
  - introduce b.
    equal_reflexivity.
  - introduce n'.
    introduce IHn'.
    introduce b.
    simpl.
    refine (equal_cong S _).
    rewrite_l (equal_cong (fun x => b + x) (IHn' b)).
    refine (add_swap _ _ _).
Qed.

Lemma mul_comm : forall (a b : nat), a * b == b * a.
Proof.
  introduce a.
  induction_nat.
  - refine (mul_0_r _).
  - introduce n'.
    introduce IHn'.
    simpl.
    rewrite_l (mul_succ_r a n').
    refine (equal_cong _ IHn').
Qed.

(* Those last two were pretty involved... if only there was an easier
   way to rewrite. *)

(* This was modelled on the basic tactics in the lbirary:

- introduce         => intro
- destruct_equal H  => destruct H
- equal_reflexivity => reflexivity
- introduce1 x      => intro x
- introduces        => intros
- induction_nat     => induction
- rewrite_l H       => rewrite H
- applying H        => apply H

 *)

Lemma mul_succ_r' : forall (a b : nat), a * S b == a + a * b.
Proof.
  induction a.
  - intros b. reflexivity.
  - intros b.
    simpl.
    rewrite IHa.
    rewrite add_swap.
    reflexivity.
Qed.

Lemma mul_comm' : forall (a b : nat), a * b == b * a.
Proof.
  intros a.
  induction b.
  - apply mul_0_r.
  - simpl.
    rewrite <- IHb.
    apply mul_succ_r'.
Qed.

Lemma mul_dist_l : forall (a b c : nat), a * (b + c) == a * b + a * c.
Proof.
  induction a.
  - intros b c. reflexivity.
  - intros b c.
    simpl.
    rewrite IHa.
    rewrite <- add_assoc.
    rewrite <- add_assoc.
    rewrite (add_assoc b c (a * b)).
    rewrite (add_comm c (a * b)).
    rewrite <- add_assoc.
    reflexivity.
Qed.

Lemma mul_dist_r : forall (a b c : nat), (b + c) * a == b * a + c * a.
Proof.
  intros a b c.
  rewrite (mul_comm (b + c) a).
  rewrite (mul_comm b a).
  rewrite (mul_comm c a).
  apply mul_dist_l.
Qed.