From Coq.micromega Require Import Lia.
From Coq.Arith Require Import PeanoNat.
Import Compare_dec.
From Coq.Lists Require Import List.
Import ListNotations.
Fixpoint insert (n : nat) (l : list nat) : list nat :=
match l with
| [] => [n]
| a :: l' => if le_lt_dec n a then n :: l else a :: (insert n l')
end.
Fixpoint insertion_sort (l : list nat) : list nat :=
match l with
| [] => []
| a :: l' => insert a (insertion_sort l')
end.
Fixpoint sorted (l : list nat) : Prop :=
match l with
| nil => True
| cons a l' =>
match l' with
| [] => True
| b :: l'' => a <= b /\ sorted l'
end
end.
Lemma sorted_tail (a : nat) (l : list nat) : sorted (a :: l) -> sorted l.
Proof. destruct l; simpl; tauto. Qed.
Lemma sorted_first_two (a b : nat) (l : list nat) :
sorted (a :: b :: l) -> a <= b.
Proof. simpl; tauto. Qed.
Lemma sorted_less_than_all (a : nat) (l : list nat) :
sorted l /\ (forall b, In b l -> a <= b) <-> sorted (a :: l).
Proof.
revert a; induction l as [|b l IHl].
- simpl. tauto.
- intros a.
split.
+ intros Hbl.
destruct Hbl as [Hbl Hble].
simpl.
simpl in Hbl.
split.
* apply Hble.
simpl. tauto.
* trivial.
+ intros Habl.
split.
* eapply sorted_tail; eauto.
* intros c Hc.
simpl in Hc.
destruct Habl as [Hab Hbl].
destruct Hc as [Hc|Hc].
-- rewrite <- Hc. trivial.
-- apply IHl in Hbl.
destruct Hbl as [Hl Hble].
transitivity b.
++ trivial.
++ apply Hble. trivial.
Qed.
Lemma in_insert (n : nat) (l : list nat) :
forall a, In a (insert n l) <-> a = n \/ In a l.
Proof.
revert n; induction l as [|b l IHl].
- simpl. firstorder.
- intros n a.
split.
+ simpl.
destruct le_lt_dec.
* simpl. firstorder.
* simpl. intros Hl.
firstorder.
+ intros Habl.
simpl in Habl.
simpl.
destruct le_lt_dec.
* simpl. firstorder.
* simpl. firstorder.
Qed.
Lemma insert_sorted (n : nat) (l : list nat) : sorted l -> sorted (insert n l).
Proof.
revert n.
induction l as [|a l IHl].
- intros n. simpl. trivial.
- intros n Hl. simpl.
destruct le_lt_dec.
+ simpl.
split.
* trivial.
* destruct l as [|b l].
-- trivial.
-- split.
++ eapply sorted_first_two; eauto.
++ eapply sorted_tail; eauto.
+ apply sorted_less_than_all.
split.
* apply IHl. eapply sorted_tail; eauto.
* apply sorted_less_than_all in Hl.
destruct Hl as [Hl1 Hl2].
intros b Hb.
apply in_insert in Hb.
destruct Hb as [Hb1|Hb2].
-- rewrite Hb1. lia.
-- auto.
Qed.
Theorem insertion_sort_sorted (l : list nat) : sorted (insertion_sort l).
Proof.
induction l as [|a l IHl].
- simpl. trivial.
- simpl.
apply insert_sorted; trivial.
Qed.
From Coq.Sorting Require Import Permutation.
Print Permutation.
Lemma insert_perm a l : Permutation (a :: l) (insert a l).
Proof.
revert a; induction l as [|b l IHl].
- simpl.
intros a.
apply Permutation_refl.
- intros a.
simpl.
destruct le_lt_dec.
+ apply Permutation_refl.
+ eapply (@perm_trans _ _ (b :: a :: l)).
* apply perm_swap.
* apply perm_skip.
apply IHl.
Qed.
Theorem insertion_sort_perm l : Permutation l (insertion_sort l).
Proof.
induction l as [|a l IHl].
- simpl.
apply perm_nil.
- simpl.
apply (@perm_trans _ _ (a :: insertion_sort l)).
+ apply perm_skip.
trivial.
+ apply insert_perm.
Qed.
Search nat "dec".
From Coq.Arith Require Import PeanoNat.
Import Compare_dec.
From Coq.Lists Require Import List.
Import ListNotations.
Fixpoint insert (n : nat) (l : list nat) : list nat :=
match l with
| [] => [n]
| a :: l' => if le_lt_dec n a then n :: l else a :: (insert n l')
end.
Fixpoint insertion_sort (l : list nat) : list nat :=
match l with
| [] => []
| a :: l' => insert a (insertion_sort l')
end.
Fixpoint sorted (l : list nat) : Prop :=
match l with
| nil => True
| cons a l' =>
match l' with
| [] => True
| b :: l'' => a <= b /\ sorted l'
end
end.
Lemma sorted_tail (a : nat) (l : list nat) : sorted (a :: l) -> sorted l.
Proof. destruct l; simpl; tauto. Qed.
Lemma sorted_first_two (a b : nat) (l : list nat) :
sorted (a :: b :: l) -> a <= b.
Proof. simpl; tauto. Qed.
Lemma sorted_less_than_all (a : nat) (l : list nat) :
sorted l /\ (forall b, In b l -> a <= b) <-> sorted (a :: l).
Proof.
revert a; induction l as [|b l IHl].
- simpl. tauto.
- intros a.
split.
+ intros Hbl.
destruct Hbl as [Hbl Hble].
simpl.
simpl in Hbl.
split.
* apply Hble.
simpl. tauto.
* trivial.
+ intros Habl.
split.
* eapply sorted_tail; eauto.
* intros c Hc.
simpl in Hc.
destruct Habl as [Hab Hbl].
destruct Hc as [Hc|Hc].
-- rewrite <- Hc. trivial.
-- apply IHl in Hbl.
destruct Hbl as [Hl Hble].
transitivity b.
++ trivial.
++ apply Hble. trivial.
Qed.
Lemma in_insert (n : nat) (l : list nat) :
forall a, In a (insert n l) <-> a = n \/ In a l.
Proof.
revert n; induction l as [|b l IHl].
- simpl. firstorder.
- intros n a.
split.
+ simpl.
destruct le_lt_dec.
* simpl. firstorder.
* simpl. intros Hl.
firstorder.
+ intros Habl.
simpl in Habl.
simpl.
destruct le_lt_dec.
* simpl. firstorder.
* simpl. firstorder.
Qed.
Lemma insert_sorted (n : nat) (l : list nat) : sorted l -> sorted (insert n l).
Proof.
revert n.
induction l as [|a l IHl].
- intros n. simpl. trivial.
- intros n Hl. simpl.
destruct le_lt_dec.
+ simpl.
split.
* trivial.
* destruct l as [|b l].
-- trivial.
-- split.
++ eapply sorted_first_two; eauto.
++ eapply sorted_tail; eauto.
+ apply sorted_less_than_all.
split.
* apply IHl. eapply sorted_tail; eauto.
* apply sorted_less_than_all in Hl.
destruct Hl as [Hl1 Hl2].
intros b Hb.
apply in_insert in Hb.
destruct Hb as [Hb1|Hb2].
-- rewrite Hb1. lia.
-- auto.
Qed.
Theorem insertion_sort_sorted (l : list nat) : sorted (insertion_sort l).
Proof.
induction l as [|a l IHl].
- simpl. trivial.
- simpl.
apply insert_sorted; trivial.
Qed.
From Coq.Sorting Require Import Permutation.
Print Permutation.
Lemma insert_perm a l : Permutation (a :: l) (insert a l).
Proof.
revert a; induction l as [|b l IHl].
- simpl.
intros a.
apply Permutation_refl.
- intros a.
simpl.
destruct le_lt_dec.
+ apply Permutation_refl.
+ eapply (@perm_trans _ _ (b :: a :: l)).
* apply perm_swap.
* apply perm_skip.
apply IHl.
Qed.
Theorem insertion_sort_perm l : Permutation l (insertion_sort l).
Proof.
induction l as [|a l IHl].
- simpl.
apply perm_nil.
- simpl.
apply (@perm_trans _ _ (a :: insertion_sort l)).
+ apply perm_skip.
trivial.
+ apply insert_perm.
Qed.
Search nat "dec".