logical-foundations/Basics.v

Inductive day : Type :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.

Definition next_weekday (d : day) : day :=
  match d with
  | monday => tuesday
  | tuesday => wednesday
  | wednesday => thursday
  | thursday => friday
  | friday => saturday
  | saturday => sunday
  | sunday => monday
  end.

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = monday.
Proof.
  simpl.
  reflexivity.
Qed.

Inductive bool : Type :=
| true
| false.

Definition negb (b : bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

Definition andb (b1 : bool) (b2 : bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

Definition orb (b1 : bool) (b2 : bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

Example test_orb1: (orb true false) = true.
Proof.
  simpl.
  reflexivity.
Qed.

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

Example test_orb2: false || false || true = true.
Proof.
  simpl.
  reflexivity.
Qed.

Definition nandb (b1: bool) (b2: bool) : bool :=
  negb (b1 && b2).

Definition andb3 (b1 : bool) (b2 : bool) (b3 : bool) : bool :=
  b1 && b2 && b3.

Inductive rgb : Type :=
| red
| green
| blue.

Inductive color : Type :=
| black
| white
| primary (p : rgb).

Definition monochrome (c : color) : bool :=
  match c with
  | black => true
  | white => true
  | primary p => false
  end.

Definition isred (c : color) : bool :=
  match c with
  | primary red => true
  | _ => false
  end.

Module Playground.
  Definition foo : rgb := blue.
End Playground.

Module NatPlayground.
  Inductive nat : Type :=
  | O
  | S (n : nat).

  Definition pred (n : nat) : nat :=
    match n with
    | O => O
    | S n' => n'
    end.

End NatPlayground.

Fixpoint even (n : nat) : bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n') => even n'
  end.

Definition odd (n: nat) : bool :=
  negb (even n).

Example test_odd1 : odd 1 = true.
Proof.
  simpl.
  reflexivity.
Qed.

Module NatPlayground2.
  Fixpoint plus (n : nat) (m : nat) : nat :=
    match n with
    | 0 => m
    | S n' => S (plus n' m)
    end.

  Compute (plus 3 2).

  Fixpoint mult (n m : nat) : nat :=
    match n with
    | 0 => 0
    | S n' => plus m (mult n' m)
    end.

  Compute (mult 2 4).

End NatPlayground2.

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

Fixpoint eqb (n m : nat) : bool :=
  match n, m with
  | 0, 0 => true
  | 0, S m' => false
  | S n', 0 => false
  | S n', S m' => eqb n' m'
  end.

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.

Fixpoint leb (n m : nat) : bool :=
  match n, m with
  | 0, _ => true
  | S n', 0 => false
  | S n', S m' => leb n' m'
  end.

Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

Definition ltb (n m : nat) : bool :=
  negb (m <=? n).

Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.

Theorem plus_0_n : forall n : nat, 0 + n = n.
Proof.
  intros n.
  simpl.
  reflexivity.
Qed.

Theorem plus_1_l: forall n : nat, 1 + n = S n.
Proof.
  intros n.
  simpl.
  reflexivity.
Qed.

Theorem mult_0_l : forall n : nat, 0 * n = 0.
Proof.
  intros n.
  reflexivity.
Qed.

Theorem plus_id_example: forall n m : nat,
    n = m ->
    n + n = m + m.
Proof.
  intros n m.
  intros H.
  rewrite H.
  reflexivity.
Qed.

Theorem plus_id_exercise : forall n m o : nat,
    n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o.
  intros H1 H2.
  rewrite H1.
  rewrite H2.
  reflexivity.
Qed.
  
Theorem plus_1_neq_0 : forall n : nat,
    (n + 1) =? 0 = false.
Proof.
  intros n.
  destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

Theorem negb_involutive: forall b : bool,
    negb (negb b) = b.
Proof.
  intros b.
  destruct b eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

Theorem andb_commutative : forall b c, b && c = c && b.
Proof.
  intros b c.
  destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

Theorem andb_true_elim2 : forall b c : bool,
    b && c = true -> c = true.
Proof.
  intros b c.
  destruct b eqn:Eqb.
  - simpl.
    intros H.
    apply H.
  - destruct c eqn:Eqc.
    + intros H.
      reflexivity.
    + intros H.
      apply H.
Qed.

Theorem zero_nbeq_plus_q : forall n : nat,
    0 =? (n + 1) = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
    (forall (x : bool), f x = x) ->
    forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite H.
  rewrite H.
  reflexivity.
Qed.

Theorem negation_fn_applied_twice :
  forall (f : bool -> bool),
    (forall (x : bool), f x = negb x) ->
    forall (b : bool), f (f b) = b.
Proof.
  intros f H.
  intros [].
  - rewrite H.
    rewrite H.
    reflexivity.
  - rewrite H.
    rewrite H.
    reflexivity.
Qed.

Lemma true_and_b : forall b: bool, true && b = b.
Proof.
  intros b.
  reflexivity.
Qed.

Lemma false_or_b : forall b: bool, false || b = b.
Proof.
  intros b.
  reflexivity.
Qed.

Theorem andb_eq_orb :
  forall (b c : bool),
    (b && c = b || c) ->
    b = c.
Proof.
  intros [] c H.
  - simpl in H.
    rewrite H.
    reflexivity.
  - simpl in H.
    rewrite H.
    reflexivity.
Qed.



Module LateDays.
  Inductive letter : Type :=
  | A | B | C | D | F.

  Inductive modifier : Type :=
  | Plus | Natural | Minus.

  Inductive grade : Type :=
    Grade (l : letter) (m : modifier).

  Inductive comparison : Type :=
  | Eq
  | Lt
  | Gt.

  Definition letter_comparison (l1 l2 : letter) : comparison :=
    match l1, l2 with
    | A, A => Eq
    | A, _ => Gt
    | B, A => Lt
    | B, B => Eq
    | B, _ => Gt
    | C, (A | B) => Lt
    | C, C => Eq
    | C, _ => Gt
    | D, (A | B | C) => Lt
    | D, D => Eq
    | D, _ => Gt
    | F, F => Eq
    | F, _ => Lt
    end.

  Theorem letter_comparison_Eq :
    forall l, letter_comparison l l = Eq.
  Proof.
    intros [].
    - reflexivity.
    - reflexivity.
    - reflexivity.
    - reflexivity.
    - reflexivity.
  Qed.

  Definition modifier_comparison (m1 m2 : modifier) : comparison :=
    match m1, m2 with
    | Plus, Plus => Eq
    | Plus, _ => Gt
    | Natural, Plus => Lt
    | Natural, Natural => Eq
    | Natural, _ => Gt
    | Minus, Minus => Eq
    | Minus, _ => Lt
    end.

  Definition grade_comparison (g1 g2: grade) : comparison :=
    match g1, g2 with
    | Grade l1 m1, Grade l2 m2 =>
        match letter_comparison l1 l2, modifier_comparison m1 m2 with
        | Lt, _ => Lt
        | Gt, _ => Gt
        | Eq, comp => comp
        end
    end.

  Definition lower_letter (l : letter) : letter :=
    match l with
    | A => B
    | B => C
    | C => D
    | D => F
    | F => F
    end.

  Theorem lower_letter_lowers:
    forall (l : letter),
      letter_comparison F l = Lt ->
      letter_comparison (lower_letter l) l = Lt.
  Proof.
    intros [] H.
    - reflexivity.
    - reflexivity.
    - reflexivity.
    - reflexivity.
    - apply H.
  Qed.

  Definition lower_grade (g : grade) : grade :=
    match g with
    | Grade l Plus => Grade l Natural
    | Grade l Natural => Grade l Minus
    | Grade l Minus => match l with
                       | F => Grade F Minus
                       | l' => Grade (lower_letter l') Plus
                       end
    end.

  Theorem lower_grade_F_Minus : lower_grade (Grade F Minus) = Grade F Minus.
  Proof.
    reflexivity.
  Qed.

  Lemma eq_letter_comp_modifier :
    forall (g1 g2 : grade),
      match g1, g2 with
        Grade l1 m1, Grade l2 m2 =>
          letter_comparison l1 l2 = Eq ->
          grade_comparison g1 g2 = modifier_comparison m1 m2
      end.
  Proof.
    intros [l1 m1] [l2 m2] H.
    simpl.
    rewrite H.
    reflexivity.
  Qed.

  Theorem lower_grade_lowers :
    forall (g : grade),
      grade_comparison (Grade F Minus) g = Lt ->
      grade_comparison (lower_grade g) g = Lt.
  Proof.
    intros [l m] H.
    destruct m eqn:Eqm.
    - simpl.
      rewrite letter_comparison_Eq.
      reflexivity.
    - simpl.
      rewrite letter_comparison_Eq.
      reflexivity.
    - simpl.
      destruct l eqn:Eql.
      + reflexivity.
      + reflexivity.
      + reflexivity.
      + reflexivity.
      + rewrite H.
        reflexivity.
  Qed.

  Definition apply_late_policy (late_days : nat) (g : grade) : grade :=
    if late_days <? 9 then g
    else if late_days <? 17 then lower_grade g
         else if late_days <? 21 then lower_grade (lower_grade g)
              else lower_grade (lower_grade (lower_grade g)).

  Theorem apply_late_policy_unfold :
    forall (late_days : nat) (g : grade),
      (apply_late_policy late_days g)
      =
        (if late_days <? 9 then g
         else if late_days <? 17 then lower_grade g
              else if late_days <? 21 then lower_grade (lower_grade g)
                   else lower_grade (lower_grade (lower_grade g))).
  Proof.
    intros.
    reflexivity.
  Qed.

  Theorem no_penalty_for_mostly_on_time :
    forall (late_days : nat) (g : grade),
      (late_days <? 9 = true) ->
      apply_late_policy late_days g = g.
  Proof.
    intros.
    rewrite apply_late_policy_unfold.
    rewrite H.
    reflexivity.
  Qed.
End LateDays.

Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (n : bin).

Fixpoint incr (m : bin) : bin :=
  match m with
  | Z => B0 Z
  | B0 b => B1 b
  | B1 b => B0 (incr b)
  end.

Fixpoint bin_to_nat (m : bin) : nat :=
  match m with
  | Z => O
  | B0 b => 2 * bin_to_nat b
  | B1 b => 1 + 2 * bin_to_nat b
  end.