Skip to content

Instantly share code, notes, and snippets.

@caotic123

caotic123/basic_sorting.v

Last active April 21, 2020 06:09
Show Gist options
  • Save caotic123/7aba9a1cc9b9112a9e6f84dfae14dbe9 to your computer and use it in GitHub Desktop.
Save caotic123/7aba9a1cc9b9112a9e6f84dfae14dbe9 to your computer and use it in GitHub Desktop.
Download ZIP
Sorting index proof in Coq
Raw
basic_sorting.v
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Lists.List.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Arith.Div2.
Export ListNotations.
Require Import Coq.Arith.PeanoNat.
Definition maxvalue (ls : list nat) : [] <> ls -> nat.
intros.
destruct ls.
destruct (H (@erefl (list nat) [])).
apply : (fold_left (fun x y => if x <=? y then y else x) ls n).
Defined.
Theorem substituion_ordering : forall ls n0 n1,
n1 <= n0 -> fold_left (fun x y : nat => if x <=? y then y else x) ls n1 <= fold_left (fun x y : nat => if x <=? y then y else x) ls n0.
elim.
auto.
move => /= a l H H1 H2 H3.
destruct (le_lt_dec H1 a).
rewrite (leb_correct _ _ l0).
rewrite <- H3 in l0.
by rewrite (leb_correct _ _ l0).
rewrite (leb_correct_conv _ _ l0).
destruct (H2 <=? a).
apply : (H _ _).
auto with arith.
apply : (H _ _ H3).
Qed.
Theorem conservation_ordering : forall ls n0,
n0 <= fold_left (fun x y : nat => if x <=? y then y else x) ls n0.
elim.
auto.
move => /= a l H H1.
destruct (le_lt_dec H1 a).
rewrite (leb_correct _ _ l0).
set (H a).
by rewrite -> l0.
rewrite (leb_correct_conv _ _ l0).
apply : H.
Qed.
Theorem maxValue : forall ls (H : [] <> ls) n, In n ls -> n <= maxvalue H.
intros.
unfold maxvalue.
induction ls.
destruct (H (@erefl (list nat) [])).
destruct ls.
destruct H0.
by subst.
inversion H0.
destruct H0.
simpl; subst.
destruct (le_lt_dec n n0).
by rewrite (leb_correct _ _ l); rewrite -> l; apply : conservation_ordering.
by rewrite (leb_correct_conv _ _ l); apply : conservation_ordering.
destruct (le_lt_dec a n0).
by simpl; rewrite (leb_correct _ _ l); apply : (IHls (@nil_cons _ n0 ls) H0).
simpl; rewrite -> (IHls (@nil_cons _ n0 ls) H0); rewrite (leb_correct_conv _ _ l); apply : substituion_ordering.
auto with arith.
Qed.
Fixpoint taill {A} (x : nat) (ls : list A) : list A :=
match x with
|S n => match ls with
|k :: u => taill n u
|[] => []
end
|0 => ls
end.
Require Import FunInd.
Functional Scheme taill_scheme := Induction for taill Sort Type.
Theorem taill' : forall A n (ls : list A), tail (taill n ls) = (taill (S n) ls).
intros.
pattern n, ls, (taill n ls).
apply : taill_scheme.
clear ls n.
intros.
subst.
destruct ls.
trivial.
trivial.
intros.
trivial.
intros.
subst.
simpl.
destruct u.
by rewrite H.
simpl in *.
by rewrite H.
Qed.
Definition tail_of {A} (x : list A) (t : list A) := {y | t ++ y = x}.
Theorem maxValue_tail : forall ls y (H : [] <> ls) n, In n (taill y ls) -> n <= maxvalue H.
intros.
apply : maxValue.
clear H; move : H0.
pattern y, ls, (taill y ls).
apply : taill_scheme.
intros; assumption.
intros; destruct H0.
intros; simpl in *.
set (H H0).
by right.
Qed.
Fixpoint prop_list {A}
(P : A -> A -> Prop) (v : list A) {struct v} : Prop.
intros.
destruct v.
exact True.
refine (_ (prop_list _ P v)).
destruct v.
exact (fun H => P a a).
refine (fun H => P a a0 /\ H).
Defined.
Functional Scheme prop_list_rect := Induction for prop_list Sort Type.
Fixpoint index_value (i: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h t =>
match (Nat.eqb i 0) with
| true => h
| false => index_value (i - 1) t
end
end.
Definition EqDec (A:Type) := forall x y:A, {x=y}+{x<>y}.
Fixpoint get_index {A} (l: list A) x : EqDec A-> nat:=
fun Eq => match l with
| cons h t => if (Eq h x) then 0 else get_index t x Eq + 1
| nil => 0
end.
Require Import Coq.Classes.EquivDec.
Definition descending := fun v => prop_list (fun x y => y <= x) v.
Definition hd A (ls : list A) : [] <> ls -> A :=
match ls return [] <> ls -> A with
|x :: xs => fun H => x
|[] => fun H => match (H eq_refl) with end
end.
Theorem less_conserv : forall x ls a, x <> a -> fold_left (fun x y : nat => if x <=? y then y else x) (x :: ls) a = a ->
fold_left (fun x y : nat => if x <=? y then y else x) (x :: ls) a =
fold_left (fun x y : nat => if x <=? y then y else x) ls a.
intros; simpl in *.
destruct (lt_eq_lt_dec x a).
destruct s.
rewrite (leb_correct_conv).
auto with arith.
trivial.
tauto.
rewrite (leb_correct); auto with arith.
rewrite (leb_correct) in H0.
auto with arith.
have : forall a x ls, a < x -> ~ fold_left (fun x y : nat => if x <=? y then y else x) ls x = a.
intros.
move : a0 x0 H1.
induction ls0.
intros; move => H'.
simpl in H'.
rewrite H' in H1.
destruct (Nat.nle_succ_diag_l _ H1).
intros; move => H'.
pose (IHls0 a1 x0 H1).
apply : n.
pose (conservation_ordering (a0 :: ls0) x0).
unfold "<" in H1; rewrite -> l0 in H1; simpl in *.
move : H' H l0.
destruct (x0 <=? a0).
intros; rewrite H' in H1; destruct (Nat.nle_succ_diag_l _ H1).
auto.
move => H2.
by destruct (H2 _ _ ls l).
Qed.
Theorem less_ord :
forall a0 a _x, fold_left (fun x y : nat => if x <=? y then y else x) (a0 :: _x) a = a ->
a0 <= a.
have : forall a x ls, a < x -> ~ fold_left (fun x y : nat => if x <=? y then y else x) ls x = a.
intros; move => H'; move : a x H H'.
induction ls.
intros; simpl in H'.
rewrite H' in H.
destruct (Nat.nle_succ_diag_l _ H).
intros.
pose (IHls _ _ H).
apply : f.
pose (conservation_ordering (a :: ls) x).
unfold "<" in H; rewrite -> l in H; simpl in *.
move : H' H l.
destruct (x <=? a).
intros; rewrite H' in H; destruct (Nat.nle_succ_diag_l _ H).
auto.
intros.
destruct (lt_eq_lt_dec a0 a).
destruct s.
auto with arith.
rewrite e; auto.
simpl in H.
rewrite (leb_correct) in H.
auto with arith.
destruct (x _ _ _x l H).
Qed.
Theorem ordering_const :
forall a b _x,
fold_left (fun x y : nat => if x <=? y then y else x) _x a = a ->
a <= b -> fold_left (fun x y : nat => if x <=? y then y else x) _x b = b.
have : forall a b, a <= b -> S b <=? a = false.
intros.
elim/@nat_double_ind : a/b H.
case.
auto with arith.
auto.
intros; inversion H.
intros; apply : (H (le_S_n _ _ H0)).
intros.
induction _x.
trivial.
pose (substituion_ordering (a0 :: _x) H0).
destruct (Nat.eq_dec a0 a).
inversion H0; subst.
by simpl; simpl in H; destruct (b <=? b).
subst;simpl.
destruct a.
apply : IH_x.
exact H.
rewrite (leb_correct_conv).
auto.
apply : IH_x.
by simpl in H; destruct (a <=? a).
inversion H0.
by subst.
subst;
pose(less_ord H).
simpl.
destruct a0.
destruct a.
destruct (n (erefl _)).
by simpl in H; apply : IH_x.
rewrite -> H0 in l0.
inversion l0.
subst; simpl in H.
rewrite (leb_correct) in H.
auto with arith.
rewrite <- H in H1.
pose(conservation_ordering _x (S m)).
rewrite <- l1 in H1.
destruct (Nat.nle_succ_diag_l _ H1).
subst.
rewrite leb_correct_conv.
auto with arith.
apply : IH_x.
pose(less_conserv n H).
rewrite <- e.
exact H.
Qed.
Theorem maxl_prop : forall (l : list nat) (H : [] <> l),
descending l -> maxvalue H = hd H.
intros.
unfold maxvalue; unfold hd; unfold descending.
move : H H0.
elim/@prop_list_rect : (prop_list (fun x : nat => le^~ x) l).
by intros.
by intros.
intros.
have : forall a b, a <= b -> S b <=? a = false.
intros.
elim/@nat_double_ind : a1/b H2.
case.
auto with arith.
auto.
intros.
inversion H2.
intros.
apply : (H2 (le_S_n _ _ H3)).
move => H3'; simpl.
destruct H1.
inversion H1.
subst.
pose (H (@nil_cons _ _ _) H2).
by simpl; elim (a <=? a).
subst; pose (H (@nil_cons _ _ _) H2).
rewrite H3'.
auto.
simpl in *.
pose (ordering_const e H3).
apply : (fun n (H : m <= S m) => ordering_const n H).
exact e0.
auto with arith.
Qed.
Theorem index_taill : forall (ls : list nat) k (H : [] <> (taill k ls)),
index_value k ls = hd H.
intros.
move : H.
elim/@taill_scheme : (taill k ls).
intros; subst.
destruct ls0.
destruct (H (erefl _)).
trivial.
intros.
destruct (H (erefl _)).
intros.
simpl; rewrite (Nat.sub_0_r); apply : H.
Qed.
Functional Scheme index_value_scheme := Induction for index_value Sort Prop.
Theorem inToIndex : forall (ls : list nat) k, k < length ls -> In (index_value k ls) ls.
intros.
move : H.
elim/@index_value_scheme : (index_value k ls).
intros; inversion H.
intros; subst; by left.
intros; simpl in *.
right; apply : H.
destruct i.
destruct t.
inversion e0.
simpl.
auto with arith.
by apply le_S_n in H0; simpl; rewrite (Nat.sub_0_r).
Qed.
Theorem index_InBound : forall k k' l, k' < length l -> k <= k' -> In (index_value k' l) (taill k l).
intros.
generalize dependent l.
elim/@nat_double_ind : k/k' H0.
intros.
by apply : inToIndex.
intros; inversion H0.
intros; simpl.
destruct l.
inversion H1.
simpl in *; rewrite (Nat.sub_0_r);apply : H.
auto with arith.
auto with arith.
Qed.
Theorem sorting_leb_order : forall (l : list nat) k k',
descending l -> k' < length l -> k < length l -> k <= k' -> index_value k' l <= index_value k l.
intros.
destruct (destruct_list (taill k l)).
do 2! destruct s.
have : ~ [] = taill k l. rewrite e; done.
move => H'.
pose (inToIndex H0).
rewrite (index_taill H'); rewrite <- maxl_prop.
by apply : maxValue; apply : index_InBound.
clear i e x0 H0 H1.
move : H.
unfold descending.
elim/@taill_scheme : (taill k l).
intros; assumption.
intros; assumption.
intros; apply : H; simpl in H0.
destruct u.
exact I.
by case : H0.
have : False.
elim/@taill_scheme : (taill k l) H1 e.
intros; subst.
inversion H1.
intros; inversion H1.
intros; apply : H1.
auto with arith.
trivial.
move => //=.
Qed.
(*
Theorem npos : forall ls n, In n ls -> {x | n = index_value x ls}.
intros.
exists (get_index ls n Nat.eq_dec).
induction ls.
destruct H.
simpl in *.
destruct H.
subst.
pose (@left).
have : forall n, is_left (Nat.eq_dec n n) = true.
intros.
destruct (Nat.eq_dec n0 n0).
trivial.
by contradiction n1.
move => H'.
by rewrite (H' _).
destruct (Nat.eq_dec a n).
by subst.
destruct (right n0).
by simpl.
simpl.
rewrite (Nat.add_succ_r _).
simpl.
rewrite (Nat.add_0_r _).
rewrite <- (Minus.minus_n_O).
by rewrite <- (IHls H).
Qed.
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment