Skip to content

Instantly share code, notes, and snippets.

@caotic123
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.
Sorting index proof in Coq
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