Coq 練習問題(7)

coq7.v

Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.


(* 練習問題5.1 *)

Section sort.
Variable A : eqType.
Variable le : A -> A -> bool.
Variable le_trans: forall x y z, le x y -> le y z -> le x z.
Variable le_total: forall x y, ~~ le x y -> le y x.
Fixpoint insert a l := match l with
  | nil => (a :: nil)
  | b :: l' => if le a b
      then a :: l
      else b :: insert a l'
  end.
Fixpoint isort l := if l is a :: l' then insert a (isort l') else nil.

Fixpoint sorted l := (* allを使ってbool上の述語を定義する *) if l is a :: l'
  then all (le a) l' && sorted l'
  else true.

Lemma le_seq_insert a b l : le a b -> all (le a) l -> all (le a) (insert b l).
Proof. elim: l => /= [-> // | c l IH].
move=> leab. move => /andP [leac leal].
case: ifPn => lebc /=.
- rewrite leab leac. done.
- by rewrite leac IH.
Qed.
Lemma le_seq_trans a b l : le a b -> all (le b) l -> all (le a) l.
Proof.
move=> leab /allP lebl. apply/allP => x Hx. by apply/le_trans/lebl.
Qed.
Theorem insert_ok a l : sorted l -> sorted (insert a l).
Proof.
  elim: l.
  + done.
  + move => b l'.
    move => IH.
    simpl.
    case: ifPn.
    move => leab.
    simpl.
    rewrite leab andTb.
    move => /andP  [allbl' sortedl'].
    rewrite allbl' sortedl' !andbT.
    apply (le_seq_trans a b l').
    - assumption.
    - assumption.
  + move => leba /andP [lebl' sortedl'].
    rewrite /=.
    rewrite le_seq_insert.
    rewrite andTb.
    by apply IH.
    by apply le_total.
    assumption.
Qed.
Theorem isort_ok l : sorted (isort l).
Proof.
  elim: l.
  + done.
  + move => a l' IH.
    simpl.
    apply insert_ok.
    assumption.
Qed.


(* perm_eq が seq で定義されているが補題だけを使う *)
Theorem insert_perm l a : perm_eq (a :: l) (insert a l).
Proof.
elim: l => //= b l pal.
case: ifPn => //= leab. by rewrite (perm_catCA [:: a] [:: b]) perm_cons.
Qed.
Check perm_catCA.

(*  
perm_catCA
     : forall (T : eqType) (s1 s2 s3 : seq T), perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3)
   *)
(* perm_eq_trans : forall (T : eqType), transitive (seq T) perm_eq *)
Search "perm_eq".
Check perm_eq_sym.
Check perm_cons.
Theorem isort_perm l : perm_eq l (isort l).
Proof.
  elim: l.
  + done.
  + move => a l' IH.
    simpl.
    rewrite perm_eq_sym.
    apply: perm_eq_trans.
    rewrite perm_eq_sym.
    apply insert_perm.
    rewrite perm_cons.
    by rewrite perm_eq_sym.
    
Qed.

End sort.

Check isort.

Definition isortn : seq nat -> seq nat := isort _ leq.
Definition sortedn := sorted _ leq.
Lemma leq_total a b : ~~ (a <= b) -> b <= a.
  rewrite leqNgt.
  Search (reflect _ (~~ _)).
  move => /negPn a_nleq_b .
  rewrite <- ltnS.
  apply: leq_trans.
  apply a_nleq_b.
  rewrite <- addn1.
  apply leq_addr.
Qed.
Theorem isortn_ok l : sortedn (isortn l) && perm_eq l (isortn l).
Proof.
  rewrite isort_perm andbT.
  rewrite /sortedn.
  rewrite isort_ok.
  reflexivity.
  move => x y z.
  apply: leq_trans.
  move => x y.
  apply leq_total.
Qed.
Require Import Extraction. Extraction "isort.ml" isortn.
Extraction leq.

coq7_2.v

(* 練習問題6.1 *)
Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.

Section even_odd.
Notation even n := (~~ odd n).
(* 単なる表記なので，展開が要らない *)
Theorem even_double n : even (n + n).
Proof. elim: n => // n. 
rewrite addnS. rewrite /=. rewrite negbK.
done.
Qed.
(* 等式を使ってnに対する通常の帰納法を可能にする *)
Theorem even_plus m n : even m -> even n = even (m + n).
Proof. elim: n => /= [|n IH] Hm.
- rewrite addn0.
apply Logic.eq_sym.
assumption.
- rewrite addnS.
  rewrite IH.
  simpl.
  reflexivity.
  assumption.
Qed.
Theorem one_not_even : ~~ even 1. Proof. reflexivity. Qed.
Theorem even_not_odd n : even n -> ~~ odd n. Proof. intro. assumption. Qed.
Theorem even_odd n : even n -> odd n.+1.
Proof.
  elim: n.
  move => _.
  apply one_not_even.
  move => /= n IH.
  move => nevenn.
  assumption.
Qed.
Theorem odd_even n : odd n -> even n.+1.
Proof.
  move => oddn.
  simpl.
  rewrite oddn.
  Search _ (~~ ~~ _).
  rewrite Bool.negb_involutive.
  reflexivity.
Qed.
Lemma odd_eq_even n : odd n = even n.+1.
Proof.
  case oddn: (odd n).
  apply Logic.eq_sym.
  apply even_odd.
  apply odd_even.
  assumption.

  Search "negP".
  apply Logic.eq_sym.
  apply negbTE.
  apply negbT in oddn.
  move: oddn.
  apply contra.
  simpl.
  rewrite Bool.negb_involutive.
  intro. assumption.
(*   elim n.
  move => even1.
  assumption.
  move => n' IH evenN2.
  apply even_odd.
  rewrite (even_plus 2 n').
  rewrite addnC addn2.
  assumption.
  apply odd_even.
  reflexivity. *)
Qed.
Lemma even_eq_odd n : odd n.+1 = even n.
Proof.
  rewrite odd_eq_even.
  apply Logic.eq_sym.
  rewrite <- addn2.
  rewrite addnC.
  apply (even_plus 2 n).
  simpl.
  reflexivity.
Qed.

Theorem even_or_odd n : even n || odd n.
Proof.
  case: (odd n).
  simpl.
  reflexivity.
  simpl.
  reflexivity.
Qed.
Theorem odd_odd_even m n : odd m -> odd n = even (m+n).
Proof.
  elim: m.
  move => /= odd0.
  elimtype False.
  by [].
  move =>  m' IH.
  move => oddn1.
  rewrite addnC addnS.
  rewrite <- odd_eq_even.
  have evenm : even m'.
  rewrite odd_eq_even.
  rewrite Bool.negb_involutive.
  assumption.
  rewrite odd_eq_even.
  rewrite [odd (n+m')]odd_eq_even.
  apply Logic.eq_sym.
  rewrite <- addn1.
  rewrite <- addnA.
  rewrite [(m' + 1)]addnC.
  rewrite addnA.
  rewrite addn1.
  apply Logic.eq_sym.
  rewrite addnC.
  apply even_plus.
  assumption. 
(* IH : odd m' -> odd n = even (m' + n) *)
(* have newIH : ~(odd n = even (m' + n)).   *)
  (* move: IH.
  elim: n.
  rewrite add0n.
  move => asum.
  simpl.
  apply Logic.eq_sym. apply negbTE.
  assumption.
  move => n' IH2 IH'.
  rewrite even_eq_odd.
  rewrite <- addn1.
  rewrite <- addnA. rewrite  [1+m']addnC.
  rewrite addnA addn1.
  rewrite even_eq_odd.
  rewrite addnC.
  apply even_plus.
  assumption.*)
Qed.
End even_odd.