Require Import List Arith Omega.

(* Here we show that the sum of powers of x up to n is a simple (rational)
  formula in x at the power (n+1). *)

Fixpoint nat_power (n m:nat) {struct m} : nat :=
 match m with 0 => 1 | S p => n*n^p end
where "n ^ m" := (nat_power n m).

(* We define a higher-order function. *)
Fixpoint sum_f (f:nat->nat)(n:nat) : nat :=
  match n with 0 => f 0 | S p => f (S p)+sum_f f p end.

(* The theorems used in the following proof, mult_1_r, mult_plus_distr_l,
  plus_assoc, and plus_comm, were all found using SearchRewrite. *)

Lemma sum_of_powers1 : forall x n, 
     x*sum_f (nat_power x) n + 1 = x^(n+1)+sum_f (nat_power x) n.
intros x; induction n.
 simpl. rewrite mult_1_r. reflexivity.
simpl. rewrite mult_plus_distr_l; rewrite <- plus_assoc.
rewrite IHn. rewrite plus_comm with (n := n). simpl. reflexivity.
Qed.

(* The theorem le_refl was found using SearchPattern. *)
SearchPattern (?x <= ?x).

(*The theorem mult_le_compat was found using SearchPattern. *)
SearchPattern (_ * _ <= _ * _).

Lemma power_pos : forall x n, 1 <= x -> 1 <= x ^ n.
intros x; induction n.
 simpl; intros h; apply le_refl.
intros x1; simpl; replace 1 with (1 * 1) by ring.
(* The tactic 'tauto' is actually apply twice, because 'apply mult_le_compat'
  generates two goals. *)
apply mult_le_compat; tauto.
Qed.

(* To find plus_reg_l, there is currently no other solution than looking at all
  theorems involving '_ <= _'.  There are about 50 such theorems. *)
SearchPattern (_ <= _).

(* Please note that the proof of the following lemma uses the previous
  lemma. *)
Lemma sum_of_powers :  forall x n, 1 <= x ->
  (x-1)*sum_f (nat_power x) n = x^(n+1)-1.
intros x n Hx; apply plus_reg_l with (p := 1*sum_f(nat_power x) n).
rewrite <- mult_plus_distr_r; rewrite <- le_plus_minus.
 apply plus_reg_l with 1.
 assert (H' : 1 +(1*sum_f (nat_power x) n+ (x^(n+1)-1))=
              1*sum_f(nat_power x) n + (1+(x^(n+1)-1))).
 ring.
 rewrite H'; clear H'; rewrite <- le_plus_minus.
  rewrite plus_comm with (n:=1); rewrite sum_of_powers1; ring.
 apply power_pos; assumption.
assumption.
Qed.

(* We now switch to another exercise, where we describe a sorting
 algorithm, by insertion, and we prove a few properties about this
 algorithm. The order between natural numbers is here expressed using
 the boolean function leb. This function was found using Search, and
 by guessing the behavior from the name.  The behavior is confirmed by
 the theorems about the function, found using the command
 SearchAbout. *)
Search bool.
SearchAbout leb.

Fixpoint insert a l {struct l} :=
  match l with
    nil => a::nil
  | b::tl => if leb a b then a::b::tl else b::insert a tl
  end.

Fixpoint sort l :=
  match l with nil => nil | a::tl => insert a (sort tl) end.

(* We now wish to express what it means for a function to be sorted.
  A first important property is to express that the first two elements,
  if they exist, must respect the order. *)

Definition head_sorted (l : list nat) : bool :=
 match l with
   a::b::_ => leb a b
 | _ => true
 end.

(* Then a list is sorted if any two consecutive elements respect the
  order. *)
Fixpoint sorted (l : list nat) : bool :=
match l with
  a::tl => if head_sorted (a::tl) then sorted tl else false
| nil => true
end.

(* The need for this lemma arises in the following proofs, because
  we reason by cases on the value of (leb x y). *)

Lemma leb_false_asym :
  forall x y, leb x y = false -> leb y x = true.
intros x y xyf; apply leb_correct.
apply lt_le_weak.
apply leb_complete_conv.
assumption.
Qed.

Lemma sorted_to_head :
  forall l, sorted l = true -> head_sorted l = true.
intros l.
case l.  
 intros; reflexivity.
intros a l'; case l'.
 intros; reflexivity.
intros b l''.
unfold sorted.
case (head_sorted (a::b::l'')).
 reflexivity.
intros h; exact h.
Qed.

Lemma sorted_to_tail :
  forall a l, sorted (a::l) = true -> sorted l = true.
intros a l'; case l'.
 intros; reflexivity.
intros b l; unfold sorted.
case (head_sorted (a :: b :: l)).
 case (head_sorted (b::l)).
  intros h; exact h.
 intros h; exact h.
intros h; discriminate.
Qed.

Lemma insert_sorted :
 forall x l, sorted l = true -> sorted (insert x l) = true.
intros x l.
(* We prove a more general statement. *)
assert (main:(sorted l = true -> sorted (insert x l) = true) /\
        forall a, sorted (a::l) = true -> sorted (insert x (a::l)) = true).
 induction l.
  split.
   intros; reflexivity.
(* In the following tactic, we give the name _ for the first hypothesis
 second element to be introduced, because we simply want to discard it. *)
  intros a _; simpl.
(* We want to reason by cases on the value of 'leb x a' but we want to
  remember in which case we are. *)
  assert (alt : leb x a = true \/ leb x a = false).
   case (leb x a). left; reflexivity. right; reflexivity.
  case alt.
   intros alt1; rewrite alt1.
   simpl.
   rewrite alt1.
   reflexivity.
  intros alt2; rewrite alt2.
  simpl.
  assert (t1: leb a x = true).
   apply leb_false_asym; assumption.
  rewrite t1.
  reflexivity.
 split.
  intuition.
 intros b.
(* We expand the definition of 'insert' by hand, avoiding the use of
  simpl, which goes too far and produces a term that is too complex. *)
 change (insert x (b::a::l)) with
        (if leb x b then x::b::a::l else b::(insert x (a::l))).
 assert (alt : leb x b = true \/ leb x b = false).
  case (leb x b).  left; reflexivity.  right; reflexivity.
 destruct alt as [alt1 | alt2].
  rewrite alt1.
(* We expand the definition of sorted and head_sorted by hand. *)
  change (sorted (x::b::a::l)) with
    (if leb x b then sorted (b::a::l) else false).
  rewrite alt1. intros h; exact h.
 rewrite alt2.
 intros sbal.
 assert (sal:sorted (a::l) = true).
  apply sorted_to_tail with (a := b).
  assumption.
 assert (sxal : sorted (insert x (a::l)) = true).
  destruct IHl as [_ IHl']; apply IHl'.
  assumption.
 change (sorted (b::insert x (a::l))) with
  (if head_sorted (b::insert x (a::l))
  then sorted (insert x (a::l)) else false).
 simpl head_sorted.
 assert (alt : leb x a = true \/ leb x a = false).
  case (leb x a). left;reflexivity. right; reflexivity.
 destruct alt as [alt1' | alt2'].
  rewrite alt1'.
  rewrite leb_false_asym.
   assumption.
  assumption.
 rewrite alt2'.
 simpl in sbal.
 destruct (leb b a).
  assumption.
 discriminate.
tauto.
Qed.

Lemma sort_sorted : forall l, sorted (sort l) = true.
induction l.
 reflexivity.
simpl.
apply insert_sorted.
assumption.
Qed.

(* We now prove that the result of sorting a list is a permutation of that
  list.  We expression permutations by counting occurrences. *) 

Fixpoint count x l :=
  match l with
    a::tl => if beq_nat x a then 1 + count x tl else count x tl
  | nil => 0
  end.

Lemma count_insert_incr :
  forall x l, count x (insert x l) = 1 + count x l.
induction l.
 simpl; rewrite <- beq_nat_refl; reflexivity.
simpl; case (leb x a); simpl.
 rewrite <- beq_nat_refl; reflexivity.
rewrite IHl; case (beq_nat x a); reflexivity.
Qed.

Lemma count_insert_diff :
  forall x y l, x <> y -> count x (insert y l) = count x l.
intros x y l xny; assert (t1 : beq_nat x y = false).
 assert (tmp : beq_nat x y = true -> x = y).
  intros h; apply beq_nat_eq; rewrite h; reflexivity.
 destruct (beq_nat x y).
  case xny; tauto.
 reflexivity.
induction l.
 simpl.
 rewrite t1. 
 reflexivity.
simpl.
case (leb y a).
 simpl.
 rewrite t1.
 reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.

Lemma sort_count :
 forall x l, count x (sort l) = count x l.
intros x l; induction l.
 reflexivity.
simpl.
assert (t1 : beq_nat x a = true -> x = a).
 apply beq_nat_true.
assert (t2 : beq_nat x a = false -> x <> a).
 apply beq_nat_false.
destruct (beq_nat x a).
 rewrite <- t1.
  rewrite count_insert_incr.
  rewrite IHl.
  reflexivity.
 reflexivity.
rewrite count_insert_diff.
 apply IHl.
apply t2.
reflexivity.
Qed.

(* A mathematical example: proving that the square root of two is not
  rational.  More precisely, there is no pair (n, m) of non zero
  natural numbers such that n*n = 2 * (m * m).  We prove this by induction
  over a p larger than n. *)

Lemma sqrt2_not_rational :
  forall n m, n <> 0 -> n * n <> 2 * (m * m).
assert (main: forall p, forall n m, n <= p -> n <> 0 -> n * n <> 2 * (m * m)).
 induction p.
(* if n <= 0 and n <> 0, there is a contradiction, these two hypotheses
 are linear formulas, and omega can treat this case. *)
  intros; omega.
 intros n m np n0 q.
 assert (nsp : n * n <> 0).
  destruct n.
   case n0; reflexivity.
  discriminate.
 assert (t1 : forall x y, x = 2 * y -> x <> 0 -> y < x).
  intros; omega.
 assert (mslns: m * m < n * n).
  apply t1; assumption.
 assert (nsl2ms : n * n < (2 * m) * (2 * m)).
  replace ((2*m)*(2*m)) with (2 * (2 * (m * m))).
   omega.
  ring.
 assert (q' : (2 * m - n) * (2 * m - n) = 2 * ((n - m) * (n - m))).
SearchRewrite ((_ - _) * _).
  rewrite mult_minus_distr_r. rewrite mult_minus_distr_r.
  rewrite mult_minus_distr_l. rewrite mult_minus_distr_l.
  rewrite mult_minus_distr_l. rewrite mult_minus_distr_l.
  rewrite mult_minus_distr_l. rewrite mult_minus_distr_l.
  rewrite mult_minus_distr_l. rewrite <- q.
  replace (2 * m * (2 * m)) with (2 * (2 * (m * m))).
   rewrite <- q.
   replace (2 * m * n) with (2 * (n * m)).
    replace (2 * (m * n)) with (n * (2 * m)).
     reflexivity.
    ring.
   ring.
  ring.
 assert (sqd : forall x y, x * x < y * y -> x < y).
  intros x y xs; case (le_or_lt y x); intros h.
   assert (y * y <= x * x).
    apply mult_le_compat.
     assumption. assumption.
   omega.
  assumption.
 assert (mn : m < n).
  apply sqd; assumption.
 assert (nm : n < 2 * m).
  apply sqd; assumption.
 assert (decr: 2 * m - n < n).
  omega.
 assert (nz : 2 * m - n <> 0).
  omega.
 apply IHp with (n := 2 * m - n) (m := n - m).
   omega.
  assumption.
exact q'.
intros n m; apply main with (p := n).
apply le_refl.
Qed.