Formal Methods

PDF version

[Rough notes]

Treating software, or specifications of software, as mathematical objects, so we can prove theorems about them.

Inductive nat : Type :=
  | Z : nat
  | S : nat -> nat.

Inductive even : nat -> Prop :=
  | evZ : even Z
  | evS : forall n:nat,
           even n -> even (S(S n)).

Theorem six_even:
   even(S(S(S(S(S(S Z)))))).
  apply evS.
  apply evS.
  apply evS.
  apply evZ.

Fixpoint plus (n:nat) (m:nat): nat :=
  match n with
  | Z => m
  | S k => S (plus k m)

Eval compute in plus (S(S Z)) (S(S(S Z))).

Theorem ev_plus_ev_is_ev:
  forall n m : nat,
    even n ->
    even m ->
    even (plus n m).
  intros n m EN EM.
  induction EN as [|n2 EN2].
  simpl. exact EM.
  simpl. apply evS. exact IHEN2.

Inductive odd : nat -> Prop :=
  | odd1: odd (S Z)
  | oddS: forall n:nat, odd n -> odd(S(S n)).

Lemma succ_odd_is_even:
  forall n:nat, odd n -> even (S n).
  intros n OddN.
  induction OddN.
  apply evS. apply evZ.
  apply evS. exact IHOddN.