Viikkotehtävän neliöhuijauksen todistus!

Vikko1.v

Theorem plus_comm : forall (n m : nat),
  n + m = m + n.
Proof.
  intros n. induction n as [| n'].
  (* case n = 0 *)
  intros m. rewrite <- plus_n_O. rewrite -> plus_O_n. trivial.
  (* case n = S n' *)
  intros m. rewrite <- plus_n_Sm. rewrite -> plus_Sn_m.
  apply eq_S. apply IHn'. Qed.

Fixpoint ble_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Theorem ble_nat_refl : forall (n : nat),
  true = ble_nat n n.
Proof.
  induction n.
    trivial.
    simpl. apply IHn. Qed.

Theorem ble_nat_Sn_0 : forall n,
  false = ble_nat (S n) 0.
Proof.
  destruct n. trivial. trivial. Qed.

Theorem ble_nat_Sn_le : forall n m,
  true = ble_nat (S n) m -> true = ble_nat n m.
Proof.
  intros n m.
  generalize dependent n.
  induction m as [| m'].
    (* case m = 0, absurd *)
    intros n H. rewrite <- ble_nat_Sn_0 in H. inversion H.
    (* case m = S m' *)
    simpl. intros n H.  destruct n as [| n'].
      (* subcase n = 0 *)
      simpl. trivial.
      (* subcase n = S n' *)
      simpl. apply IHm'. apply H. Qed.

Theorem ble_nat_S_refl : forall n m,
  true = ble_nat n m -> false = ble_nat (S m) n.
Proof.
  intros n.
  induction n as [| n'].
    (* case n = 0 *)
    intros m H. apply ble_nat_Sn_0.
    (* case n = S n' *)
    intros m H. simpl. destruct m as [| m'].
      (* case m = 0 *)
      rewrite <- ble_nat_Sn_0 in H. inversion H.
      (* case m = S m' *)
      apply IHn'. apply H. Qed.

Definition square (n : nat) : nat := n * n.

Theorem square_Sn : forall (n : nat),
  square (S n) = S (square n + n + n).
Proof.
  intros n.
  unfold square. simpl. apply eq_S.
  rewrite <- mult_n_Sm. rewrite <- plus_comm. trivial. Qed.

(* 0-indekssoitu viikkotehtava, n -> (sarake, rivi) *)
Fixpoint viikko1 (n : nat) : (nat * nat) :=
  match n with
  | O   => (O, O)
  | S n' => match viikko1 n' with
            | (O, y) => (S y, O)
            | (x, y) => if ble_nat x y then (pred x, y) else (x, S y)
            end

   end.

Example viikko1_example1 : viikko1 0 = (0, 0). reflexivity. Qed.
Example viikko1_example2 : viikko1 1 = (1, 0). reflexivity. Qed.
Example viikko1_example3 : viikko1 9 = (3, 0). reflexivity. Qed.
Example viikko1_example4 : viikko1 12 = (3, 3). reflexivity. Qed.
Example viikko1_example5 : viikko1 15 = (0, 3). reflexivity. Qed.
Example viikko1_example6 : viikko1 16 = (4, 0). reflexivity. Qed.

Lemma viikko1_lemma1' : forall (m n x y: nat),
  true = ble_nat (y + m) x -> viikko1 n = (x, y) -> viikko1 (n + m) = (x, y + m).
Proof.
  intros m.
  induction m as [| m'].
  (* Case m = 0 *)
    intros n x y t H.
    rewrite <- plus_n_O. rewrite <- plus_n_O.
    apply H.
  (* Case m = S m' *)
    intros n x y t H.
    (* Helpers *)
    assert (nH: n + S m' = S (n + m')). rewrite <- plus_n_Sm. trivial.
    assert (YH: y + S m' = S (y + m')). rewrite <- plus_n_Sm. trivial.
    (* continue ... *)
    rewrite -> YH. rewrite -> nH.
    simpl.
    replace (viikko1 (n + m')) with (x, y + m').
    destruct x as [| x'].
      (* x = 0 *)
      rewrite -> YH in t. inversion t.
      (* x = S x' *)
      replace ( ble_nat (S x') (y + m')) with (false).
      trivial.
      (* Proof of replace *)
      apply ble_nat_S_refl. rewrite -> YH in t. inversion t. trivial.
      (* End of proof *)
      symmetry. apply IHm'. rewrite -> YH in t. apply ble_nat_Sn_le. apply t.
      apply H. Qed.

Lemma viikko1_lemma1 : forall (n x : nat),
  viikko1 n = (x, 0) -> viikko1 (n + x) = (x, x).
Proof.
  intros n x H.
  replace ((x, x)) with ((x, 0 + x)).
  apply viikko1_lemma1'.
    (* Proof of prereq *)
    simpl. apply ble_nat_refl.
  apply H.
  (* Proof of replace *)
  simpl. trivial. Qed.

Lemma viikko1_lemma3 : forall (n x : nat),
  viikko1 n = (0, x) -> viikko1 (S n) = (S x, 0).
Proof.
  intros n x.
  destruct n as [| n'].
    simpl. intros H. inversion H. trivial.
    simpl. intros H. rewrite -> H. trivial. Qed.

Lemma viikko1_lemma2' : forall (m n y: nat),
  true = ble_nat m y -> viikko1 n = (m, y) -> viikko1 (n + m) = (0, y).
Proof.
  intros m.
  induction m as [| m'].
  (* case m = 0 *)
    intros n y t H.
    rewrite <- plus_n_O. apply H.
  (* case m = S m' *)
    intros n y t H.
    assert (nH: n + S m' = S (n + m')). rewrite <- plus_n_Sm. trivial.
    rewrite -> nH.
    destruct y as [| y'].
    (* case y = 0 *)
      inversion t.
    (* case y = S y' *)
      rewrite <- plus_Sn_m.
      apply IHm'.
      inversion t.
      apply ble_nat_Sn_le. apply t.
      simpl. rewrite -> H. rewrite <- t. trivial. Qed.

Lemma viikko1_lemma2 : forall (n x : nat),
  viikko1 n = (x, x) -> viikko1 (n + x) = (0, x).
Proof.
  intros n x H.
  apply viikko1_lemma2'.
  simpl. apply ble_nat_refl.
  simpl. apply H. Qed.


(* This is the thing !!! 
  Jos viikkotehtavassa olisi 0-indeksointi

  eli
  0 1 4 9
  3 2 5
  8 7 6

  ja laskettaisiin 0 -> (0, 0) niin:
*)
Theorem viikko1_square_huijaus : forall n : nat,
  viikko1 (square n) = (n, 0).
Proof.
  intros n.
  induction n as [| n'].
    reflexivity.
    rewrite -> square_Sn.
    apply viikko1_lemma3.
    apply viikko1_lemma2.
    apply viikko1_lemma1.
    apply IHn'. Qed.