Skip to content

Instantly share code, notes, and snippets.

@moratori
Created Aug 7, 2014
Embed
What would you like to do?
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
Inductive bool : Type :=
| true : bool
| false: bool.
Fixpoint lessthan (n : nat) (m : nat) : bool :=
match n with
| O =>
match m with
| O => false
| S m' => true
end
| S n' =>
match m with
| O => false
| S m' => (lessthan n' m')
end
end.
Fixpoint plus (n m : nat) : nat :=
match m with
| O => n
| S m' => S (plus n m')
end.
Theorem lessthan_th1 :
forall (n : nat) , (lessthan n (S n)) = true.
Proof.
intros.
induction n.
simpl.
reflexivity.
simpl.
rewrite -> IHn.
reflexivity.
Qed.
Theorem plus_th1 :
forall (n : nat) , (plus O n) = n.
Proof.
intros.
induction n.
simpl.
reflexivity.
simpl.
rewrite -> IHn.
reflexivity.
Qed.
Theorem plus_th2 :
forall (n m : nat) , (S (plus n m)) = (plus (S n) m).
Proof.
intros.
induction m.
simpl.
reflexivity.
simpl.
rewrite <- IHm.
reflexivity.
Qed.
Theorem plus_th3 :
forall (n m : nat) , (plus n m) = (plus m n).
Proof.
intros.
induction m.
rewrite -> plus_th1.
simpl.
reflexivity.
simpl.
rewrite -> IHm.
rewrite <- plus_th2.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment