logical-foundations/Induction.v

From LF Require Export Basics.

Theorem add_0_r : forall n : nat,
    n + 0 = n.
Proof.
  intros n.
  induction n as [| n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem minus_n_n : forall n,
    n - n = 0.
Proof.
  intros.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem mul_0_r : forall n : nat,
    n * 0 = 0.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem plus_n_Sm : forall n m : nat,
    S (n + m) = n + (S m).
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - intros m.
    simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem add_comm : forall n m : nat,
    n + m = m + n.
Proof.
  induction n as [ | n' IHn'].
  - intros m.
    rewrite add_0_r.
    reflexivity.
  - intros m.
    simpl.
    rewrite plus_n_Sm.
    rewrite IHn'.
    simpl.
    rewrite plus_n_Sm.
    reflexivity.
Qed.

Theorem sn_eq_sm_n_eq_m : forall n m : nat,
    S n = S m -> n = m.
Proof.
  intros n m H.
  inversion H.
  reflexivity.
Qed.

Theorem n_eq_m_sn_eq_sm : forall n m : nat,
    n = m -> S n = S m.
Proof.
  intros n m H.
  rewrite H.
  reflexivity.
Qed.
  
Theorem add_assoc : forall n m p : nat,
    n + (m + p) = (n + m) + p.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    intros m p.
    apply n_eq_m_sn_eq_sm.
    rewrite IHn'.
    reflexivity.
Qed.

Fixpoint double (n : nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Lemma double_plus : forall n, double n = n + n.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    apply n_eq_m_sn_eq_sm.
    rewrite IHn'.
    apply plus_n_Sm.
Qed.

Theorem eqb_refl : forall n : nat,
    (n =? n) = true.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem even_S : forall n : nat,
    even (S n) = negb (even n).
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - rewrite IHn'.
    rewrite negb_involutive.
    reflexivity.
Qed.

Theorem mult_0_plus' : forall n m : nat,
    (n + 0 + 0) * m = n * m.
Proof.
  intros n m.
  assert (H : n + 0 + 0 = n).
  - rewrite add_comm.
    simpl.
    rewrite add_comm.
    reflexivity.
  - rewrite H.
    reflexivity.
Qed.

Lemma n_zero_zero : forall n : nat,
    n * 0 = 0.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem add_shuffle3 : forall n m p : nat,
    n + (m + p) = m + (n + p).
Proof.
  intros n m p.
  rewrite add_assoc.
  assert (H: n + m = m + n).
  { rewrite add_comm. reflexivity. }
  rewrite H.
  rewrite add_assoc.
  reflexivity.
Qed.

Lemma shuffle_4 : forall (a b c d : nat),
    (a + b) + (c + d) = (a + c) + (b + d).
Proof.
  intros a b c d.
  assert (H: a + b + (c + d) = a + ((b + c) + d)).
  { rewrite add_assoc. rewrite add_assoc. rewrite add_assoc. reflexivity. }
  rewrite H.
  assert (H1: b + c = c + b).
  { rewrite add_comm. reflexivity. }
  rewrite H1.
  rewrite add_assoc.
  rewrite add_assoc.
  rewrite add_assoc.
  reflexivity.
Qed.
  
Theorem distributivity : forall (n m k : nat),
    n * (m + k) = n * m + n * k.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - intros m k.
    simpl.
    rewrite IHn'.
    rewrite shuffle_4.
    reflexivity.
Qed.

Theorem n_one_n : forall n : nat,
    n * 1 = n.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem mul_comm : forall m n : nat,
    m * n = n * m.
Proof.
  induction n as [ | n' IHn'].
  - rewrite n_zero_zero.
    reflexivity.
  - simpl.
    assert (H: S n' = n' + 1).
    { rewrite add_comm. reflexivity. }
    rewrite H.
    rewrite distributivity.
    rewrite n_one_n.
    rewrite IHn'.
    rewrite add_comm.
    reflexivity.
Qed.

Theorem plus_leb_compact_l : forall n m p : nat,
    n <=? m = true -> (p + n) <=? (p + m) = true.
Proof.
  induction p as [ | p' IHp'].
  - auto.
  - intros H.
    simpl.
    apply IHp'.
    rewrite H.
    reflexivity.
Qed.

Theorem leb_refl : forall n : nat,
    (n <=? n) = true.
Proof.
  induction n as [ | n' IHn'].
  - reflexivity.
  - simpl.
    rewrite IHn'.
    reflexivity.
Qed.

Theorem zero_neqb_S : forall n : nat,
    0 =? (S n) = false.
Proof.
  reflexivity.
Qed.