Inductive day :=
| Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday.
About day.
About Friday.
Definition next_day (d : day) : day :=
match d with
| Monday => Tuesday
| Tuesday => Wednesday
| Wednesday => Thursday
| Thursday => Friday
| Friday => Saturday
| Saturday => Sunday
| Sunday => Monday
end.
Eval compute in next_day Tuesday.
Eval compute in next_day (next_day Tuesday).
Theorem next_day_monday : next_day Monday = Tuesday.
Proof.
reflexivity.
Qed.
Definition previous_day (d : day) : day :=
match d with
| Monday => Sunday
| Tuesday => Monday
| Wednesday => Tuesday
| Thursday => Wednesday
| Friday => Thursday
| Saturday => Friday
| Sunday => Saturday
end.
Theorem previous_next_day : forall d, previous_day (next_day d) = d.
Proof.
intros d; destruct d; reflexivity.
Qed.
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S x => S (plus x m)
end.
Theorem S_plus_one n : S n = plus n 1.
Proof.
induction n as [|x IHx].
- simpl. reflexivity.
- simpl. rewrite IHx. reflexivity.
Qed.
Print "+".
Theorem add_com n m : n + m = m + n.
Proof.
revert m.
induction n as [|n IHn].
- intros m.
simpl.
induction m as [|m IHm].
+ simpl. trivial.
+ simpl. rewrite <- IHm. reflexivity.
- intros m.
induction m as [|m IHm].
+ simpl.
rewrite IHn. simpl. reflexivity.
+ simpl.
rewrite IHn.
simpl.
rewrite <- IHm.
simpl.
rewrite IHn.
reflexivity.
Qed.
Theorem add_com' n m : n + m = m + n.
Proof.
revert m.
induction n; induction m; auto.
simpl; rewrite IHn; simpl; rewrite <- IHm; simpl; auto.
Qed.
Require Import Coq.micromega.Lia.
Theorem add_com'' n m : n + m = m + n.
Proof. lia. Qed.
Theorem thm : forall x y, x < y -> (x + y) - 2 * x < 2 * y.
Proof. lia. Qed.
| Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday.
About day.
About Friday.
Definition next_day (d : day) : day :=
match d with
| Monday => Tuesday
| Tuesday => Wednesday
| Wednesday => Thursday
| Thursday => Friday
| Friday => Saturday
| Saturday => Sunday
| Sunday => Monday
end.
Eval compute in next_day Tuesday.
Eval compute in next_day (next_day Tuesday).
Theorem next_day_monday : next_day Monday = Tuesday.
Proof.
reflexivity.
Qed.
Definition previous_day (d : day) : day :=
match d with
| Monday => Sunday
| Tuesday => Monday
| Wednesday => Tuesday
| Thursday => Wednesday
| Friday => Thursday
| Saturday => Friday
| Sunday => Saturday
end.
Theorem previous_next_day : forall d, previous_day (next_day d) = d.
Proof.
intros d; destruct d; reflexivity.
Qed.
Fixpoint plus (n m : nat) : nat :=
match n with
| O => m
| S x => S (plus x m)
end.
Theorem S_plus_one n : S n = plus n 1.
Proof.
induction n as [|x IHx].
- simpl. reflexivity.
- simpl. rewrite IHx. reflexivity.
Qed.
Print "+".
Theorem add_com n m : n + m = m + n.
Proof.
revert m.
induction n as [|n IHn].
- intros m.
simpl.
induction m as [|m IHm].
+ simpl. trivial.
+ simpl. rewrite <- IHm. reflexivity.
- intros m.
induction m as [|m IHm].
+ simpl.
rewrite IHn. simpl. reflexivity.
+ simpl.
rewrite IHn.
simpl.
rewrite <- IHm.
simpl.
rewrite IHn.
reflexivity.
Qed.
Theorem add_com' n m : n + m = m + n.
Proof.
revert m.
induction n; induction m; auto.
simpl; rewrite IHn; simpl; rewrite <- IHm; simpl; auto.
Qed.
Require Import Coq.micromega.Lia.
Theorem add_com'' n m : n + m = m + n.
Proof. lia. Qed.
Theorem thm : forall x y, x < y -> (x + y) - 2 * x < 2 * y.
Proof. lia. Qed.