Skip to content

Instantly share code, notes, and snippets.

@ayu-mushi

ayu-mushi/coq6.v

Last active June 4, 2019 10:51
Show Gist options
  • Save ayu-mushi/ba3768350fd31f7c1388079be53d0b2e to your computer and use it in GitHub Desktop.
Save ayu-mushi/ba3768350fd31f7c1388079be53d0b2e to your computer and use it in GitHub Desktop.
Download ZIP
Coq exercise (6)
Raw
coq6.v
Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.
Section Sort.
Variables (A:Set) (le:A->A->bool).
(* 既に整列されたリストlの中にaを挿入する *)
Fixpoint insert a (l: list A) := match l with
| nil => (a :: nil)
| b :: l' => if le a b then a :: l else b :: insert a l'
end.
(* 繰り返しの挿入でリストlを整列する *)
Fixpoint isort (l : list A) : list A :=
match l with
| nil => nil
| a :: l' => insert a (isort l')
end.
(* le は推移律と完全性をみたす *)
Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
Hypothesis le_total: forall x y, ~~ le x y -> le y x.
(* le_list x l : x はあるリスト l の全ての要素以下である *)
Inductive le_list x : list A -> Prop :=
| le_nil : le_list x nil
| le_cons : forall y l, le x y -> le_list x l -> le_list x (y::l).
(* sorted l : リスト l は整列されている *)
Inductive sorted : list A -> Prop :=
| sorted_nil : sorted nil
| sorted_cons : forall a l, le_list a l -> sorted l -> sorted (a::l).
Hint Constructors le_list sorted. (* auto の候補にする *)
Lemma le_list_insert a b l : le a b -> le_list a l -> le_list a (insert b l).
Proof.
move=> leab; elim => {l} [|c l] /=. info_auto.
case: ifPn. info_auto. info_auto.
Qed.
Lemma le_list_trans a b l : le a b -> le_list b l -> le_list a l.
Proof.
move=> leab; elim. info_auto.
info_eauto using le_trans. (* 推移律は eauto が必要 *)
Qed.
Hint Resolve le_list_insert le_list_trans. (* 補題も候補に加える *)
Theorem insert_ok a l : sorted l -> sorted (insert a l).
Proof.
elim.
+ apply sorted_cons.
apply le_nil.
apply sorted_nil.
+ move => a0 l0 leA0l0 sortedl0 sortedal0.
simpl.
case: ifPn.
- move => a_le_a0.
apply sorted_cons.
apply le_cons.
assumption.
apply: le_list_trans.
apply a_le_a0.
assumption.
apply sorted_cons.
assumption.
assumption.
- info_auto.
Qed.
Theorem isort_ok l : sorted (isort l).
Proof.
elim: l.
+ simpl.
apply sorted_nil.
+ move => a l0 sorted_sortedl0.
simpl.
apply insert_ok.
assumption.
Qed.
(* Permutation l1 l2 : リスト l2 は l1 の置換である *)
Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation nil nil
| perm_skip: forall x l l', Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap: forall x y l, Permutation (y::x::l) (x::y::l)
| perm_trans: forall l l' l'', Permutation l l' -> Permutation l' l'' -> Permutation l l''.
Hint Constructors Permutation.
Theorem Permutation_refl l : Permutation l l.
Proof.
elim l.
+ apply perm_nil.
+ move => a l0 perml0l0.
apply perm_skip.
assumption.
Qed.
(* なぜか + が働かない*)
(* [:: a, a0 & l0] の意味は? *)
Theorem insert_perm l a : Permutation (a :: l) (insert a l).
Proof.
elim: l.
+ simpl. apply Permutation_refl.
+ move => a0 l IH.
simpl.
case: ifPn.
- move => le_a_a0.
apply Permutation_refl.
- move => lt_a0_a.
apply: perm_trans.
apply: perm_swap.
apply perm_skip.
apply IH.
Qed.
Theorem isort_perm l : Permutation l (isort l).
Proof.
elim: l.
+ simpl.
apply perm_nil.
+ move => a l IH.
simpl.
apply: perm_trans.
apply perm_skip.
apply IH.
apply insert_perm.
Qed.
(* 証明付き整列関数 *)
Definition safe_isort l : {l'|sorted l' /\ Permutation l l'}.
exists (isort l).
auto using isort_ok, isort_perm.
Defined.
Print safe_isort.
End Sort.
Check safe_isort. (* le と必要な補題を与えなければならない *)
Extraction leq. (* mathcomp の eqType の抽出が汚ない *)
Definition leq' m n := if m - n is 0 then true else false.
Extraction leq'. (* こちらはすっきりする *)
Lemma leq'E m n : leq' m n = (m <= n).
Proof. rewrite /leq' /leq. by case: (m-n).
Qed.
Lemma leq'_trans m n p : leq' m n -> leq' n p -> leq' m p.
Proof. rewrite !leq'E; apply leq_trans. Qed.
Lemma leq'_total m n : ~~ leq' m n -> leq' n m.
Proof.
rewrite !leq'E.
rewrite <- ltnNge.
move => not_n_leq_n.
rewrite ltnW.
+ done.
+ assumption.
Qed.
Definition isort_leq := safe_isort nat leq' leq'_trans leq'_total.
Eval compute in proj1_sig (isort_leq (3 :: 1 :: 2 :: 0 :: nil)).
(* = [:: 0; 1; 2; 3] : seq nat *)
Extraction "program/coq66/isort.ml" isort_leq.
Raw
coq6_all.v
Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.
Section Sort.
Variables (A:Set) (le:A->A->bool).
Inductive All (P : A -> Prop) : list A -> Prop :=
| All_nil : All P nil
| All_cons : forall y l, P y -> All P l -> All P (y::l).
(* 既に整列されたリストlの中にaを挿入する *)
Fixpoint insert a (l: list A) := match l with
| nil => (a :: nil)
| b :: l' => if le a b then a :: l else b :: insert a l'
end.
(* 繰り返しの挿入でリストlを整列する *)
Fixpoint isort (l : list A) : list A :=
match l with
| nil => nil
| a :: l' => insert a (isort l')
end.
(* le は推移律と完全性をみたす *)
Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
Hypothesis le_total: forall x y, ~~ le x y -> le y x.
(* le_list x l : x はあるリスト l の全ての要素以下である *)
(* sorted l : リスト l は整列されている *)
Inductive sorted : list A -> Prop :=
| sorted_nil : sorted nil
| sorted_cons : forall a l, All (le a) l -> sorted l -> sorted (a::l).
Hint Constructors All sorted. (* auto の候補にする *)
Lemma le_list_insert a b l : le a b -> All (le a) l -> All (le a) (insert b l).
Proof.
move=> leab; elim => {l} [|c l] /=. info_auto.
case: ifPn. info_auto. info_auto.
Qed.
Lemma le_list_trans a b l : le a b -> All (le b) l -> All (le a) l.
Proof.
move=> leab; elim. info_auto.
info_eauto using le_trans. (* 推移律は eauto が必要 *)
Qed.
Hint Resolve le_list_insert le_list_trans. (* 補題も候補に加える *)
Theorem insert_ok a l : sorted l -> sorted (insert a l).
Proof.
elim.
+ apply sorted_cons.
apply All_nil.
apply sorted_nil.
+ move => a0 l0 leA0l0 sortedl0 sortedal0.
simpl.
case: ifPn.
- move => a_le_a0.
apply sorted_cons.
apply All_cons.
assumption.
apply: le_list_trans.
apply a_le_a0.
assumption.
apply sorted_cons.
assumption.
assumption.
- info_auto.
Qed.
Theorem isort_ok l : sorted (isort l).
Proof.
elim: l.
+ simpl.
apply sorted_nil.
+ move => a l0 sorted_sortedl0.
simpl.
apply insert_ok.
assumption.
Qed.
(* Permutation l1 l2 : リスト l2 は l1 の置換である *)
Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation nil nil
| perm_skip: forall x l l', Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap: forall x y l, Permutation (y::x::l) (x::y::l)
| perm_trans: forall l l' l'', Permutation l l' -> Permutation l' l'' -> Permutation l l''.
Hint Constructors Permutation.
Theorem Permutation_refl l : Permutation l l.
Proof.
elim l.
+ apply perm_nil.
+ move => a l0 perml0l0.
apply perm_skip.
assumption.
Qed.
(* なぜか + が働かない*)
(* [:: a, a0 & l0] の意味は? *)
Theorem insert_perm l a : Permutation (a :: l) (insert a l).
Proof.
elim: l.
+ simpl. apply Permutation_refl.
+ move => a0 l IH.
simpl.
case: ifPn.
- move => le_a_a0.
apply Permutation_refl.
- move => lt_a0_a.
apply: perm_trans.
apply: perm_swap.
apply perm_skip.
apply IH.
Qed.
Theorem isort_perm l : Permutation l (isort l).
Proof.
elim: l.
+ simpl.
apply perm_nil.
+ move => a l IH.
simpl.
apply: perm_trans.
apply perm_skip.
apply IH.
apply insert_perm.
Qed.
(* 証明付き整列関数 *)
Definition safe_isort l : {l'|sorted l' /\ Permutation l l'}.
exists (isort l).
auto using isort_ok, isort_perm.
Defined.
Print safe_isort.
End Sort.
Check safe_isort. (* le と必要な補題を与えなければならない *)
Extraction leq. (* mathcomp の eqType の抽出が汚ない *)
Definition leq' m n := if m - n is 0 then true else false.
Extraction leq'. (* こちらはすっきりする *)
Lemma leq'E m n : leq' m n = (m <= n).
Proof. rewrite /leq' /leq. by case: (m-n).
Qed.
Lemma leq'_trans m n p : leq' m n -> leq' n p -> leq' m p.
Proof. rewrite !leq'E; apply leq_trans. Qed.
Lemma leq'_total m n : ~~ leq' m n -> leq' n m.
Proof.
rewrite !leq'E.
rewrite <- ltnNge.
move => not_n_leq_n.
rewrite ltnW.
+ done.
+ assumption.
Qed.
Definition isort_leq := safe_isort nat leq' leq'_trans leq'_total.
Eval compute in proj1_sig (isort_leq (3 :: 1 :: 2 :: 0 :: nil)).
(* = [:: 0; 1; 2; 3] : seq nat *)
Extraction "isort_all.ml" isort_leq.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment