Feb6.v

Set Implicit Arguments.

Require Import Arith Omega.

Section Evenness.

  Inductive even : nat -> Prop :=
    | zero_even : even 0
    | ss_even : forall (n : nat), even n -> even (S (S n)).

  Fixpoint is_even (n : nat) : bool :=
    match n with
      | O => true
      | S O => false
      | S (S n) => is_even n
    end.

  Eval simpl in is_even 100.
  Example even10 : even 100.
  repeat constructor.
  Qed.

  Lemma even_is_even : forall n, even n -> is_even n = true.
    intros.
    induction H.
    reflexivity.
    simpl. trivial.
  Qed.

  Lemma is_even_even : forall n, is_even n = true -> even n.
    intros.
    induction n.
    + apply zero_even.
    + simpl in H.
      destruct n.
      inversion H.
      apply ss_even.
  Admitted.
  
End Evenness.

Section Factorial.

  Inductive fac : nat -> nat -> Prop :=
    | zero_fac : fac 0 1
    | succ_fac : forall n m, fac n m -> fac (S n) ((S n) * m).

  Fixpoint facf (n : nat) : nat :=
    match n with
      | 0 => 1
      | S n' => n * (facf n')
    end.

  Eval simpl in facf 5.

  Lemma fac5_expansion : 120 = 5 * (4 * (3 * (2 * (1 * 1)))).
    trivial.
  Qed.
  
  Example fac5 : fac 5 120.
  rewrite fac5_expansion.
  repeat constructor.
  Qed.

  Lemma fac_facf : forall n m, fac n m -> facf n = m.
    intros.
    induction H.
    reflexivity.
    simpl.
    rewrite IHfac.
    trivial.
  Qed.

  Lemma facf_fac : forall n m, facf n = m -> fac n m.
    intros n.
    induction n.
    + intros. 
      rewrite <- H.
      simpl.
      constructor.
    + intros.
      rewrite <- H.
      simpl.
      apply succ_fac.
      apply IHn.
      trivial.
  Qed.

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

  Lemma tailfac_fac' : forall n k m, tailfac n k = m -> exists j, (fac n j) /\ j * k = m.
    intros n.
    induction n; intros.
    + simpl in H. subst. exists 1. split. constructor. omega.
    + simpl in H.
      apply IHn in H.
      clear IHn.
      destruct H as [j [H H0]].
      subst.
      exists (S n * j).
      split.
      - constructor. trivial.
      - rewrite <- (mult_1_l k) at 2.
        rewrite <- mult_plus_distr_r.
        assert (1 + n = S n). reflexivity.
        rewrite -> H0.
        remember (S n) as x.
        rewrite -> mult_assoc.
        rewrite -> (mult_comm j x).
        trivial.
  Qed.

  Lemma tailfac_fac'' : forall n k m, tailfac n k = m -> exists j, (fac n j) /\ j * k = m.
  Proof with auto with arith.
    Hint Constructors fac.
    intros n.
    induction n; intros.
    + exists 1. simpl in H. subst...
    + apply IHn in H.
      destruct H as [j [H H0]].
      subst.
      exists (S n * j).
      rewrite -> mult_assoc...
  Qed.

  Lemma tailfac_fac : forall m n, tailfac n 1 = m -> fac n m.
    intros.
    apply tailfac_fac' in H.
    destruct H as [j H].
    destruct H.
    simpl in H0.
    rewrite mult_1_r in H0.
    subst.
    trivial.
  Qed.

End Factorial.