Skip to content

Instantly share code, notes, and snippets.

@konn

konn/nat_aux.v

Last active August 29, 2015 14:20
Show Gist options
  • Save konn/caf5f6c0adb526f0d3b7 to your computer and use it in GitHub Desktop.
Save konn/caf5f6c0adb526f0d3b7 to your computer and use it in GitHub Desktop.
Download ZIP
Encoding sequence of natural numbers as natural numbers, preserving order.
Raw
nat_aux.v
Require Import ssreflect ssrbool eqtype ssrnat div prime.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Theorem wf_ltn : well_founded (fun (x y : nat) => x < y).
Proof.
move => x.
move : {2}x (leqnn x) => n.
elim: n x => [ | n IHn ] x H; constructor => y H0.
- apply False_ind, notF.
rewrite -(ltn0 y).
apply (leq_trans H0 H).
- apply IHn.
rewrite -ltnS.
apply (leq_trans H0 H).
Defined.
Theorem nat_course_of_value_ind:
forall (P : nat -> Prop),
P 0 ->
(forall x: nat, (forall y : nat, y <= x -> P y) -> P (x.+1)) ->
forall x : nat, P x.
Proof.
move => P base succ.
elim/(well_founded_ind wf_ltn) => n IH.
case H : n => [| k].
- assumption.
- apply succ.
rewrite H in IH.
assumption.
Qed.
Ltac cvinduction := elim/nat_course_of_value_ind.
Lemma muln2_S_mod_2 : forall n, (n * 2).+1 %% 2 = 1.
Proof.
elim; done.
Qed.
Lemma mul2n_S_mod_2 : forall n, (2 * n).+1 %% 2 = 1.
Proof.
move => n. rewrite mulnC. by apply: muln2_S_mod_2.
Qed.
Lemma double_S_mod_2 : forall n, (double n).+1 %% 2 = 1.
Proof.
move => n. rewrite -muln2. exact: muln2_S_mod_2.
Qed.
Lemma mul_mod_r : forall m n l, m > 0 -> (n * m + l) %% m = l %% m.
Proof.
move => m n l m_pos.
move : n l.
elim => [| k IH] l.
- done.
- rewrite mulSn -addnA.
rewrite modnDl.
exact: IH.
Qed.
Lemma mul_mod_l : forall m n l, m > 0 -> (l + m * n) %% m = l %% m.
Proof.
move => m n l.
rewrite addnC mulnC.
exact: mul_mod_r.
Qed.
Lemma odd_Sn : forall n, odd n = ~~odd n.+1.
Proof.
cvinduction => [| n IH].
- done.
- rewrite {2}/odd.
rewrite Bool.negb_involutive.
case Hn : n => [| k].
+ done.
+ rewrite -/odd.
rewrite Bool.negb_involutive.
rewrite [odd k]IH.
+ done.
+ rewrite Hn.
done.
Qed.
Lemma ltn_half : forall n, n > 0 -> n./2 < n.
Proof.
move => n n_pos.
rewrite -divn2.
apply: ltn_Pdiv; done.
Qed.
Lemma leq_half: forall n, n./2 <= n.
Proof.
move => n.
rewrite -divn2.
apply: leq_div.
Qed.
Lemma half_odd : forall n, n.*2.+1./2 = n.
Proof.
move => n.
rewrite -add1n.
rewrite -[1]/(nat_of_bool true).
exact: half_bit_double.
Qed.
Hint Resolve wf_ltn.
Lemma ltn_add : forall m1 m2 n1 n2, m1 < n1 -> m2 < n2 -> m1 + m2 < n1 + n2.
Proof.
move => m1 m2 n1 n2 ltn1 ltn2.
apply: ltn_trans.
- exact: (m1 + n2).
- rewrite ltn_add2l.
assumption.
- rewrite ltn_add2r.
assumption.
Qed.
Definition trunc_log' p :=
fix loop n k :=
if k is k'.+1
then if p <= n then (loop (n %/ p) k').+1 else 0
else 0.
Lemma trunc_log_equation : forall p n, trunc_log p n = trunc_log' p n n.
Proof.
move => p.
elim => [| k IH ].
- done.
- rewrite /trunc_log.
rewrite /trunc_log'.
done.
Qed.
Require Import Recdef.
Function bit_size (n : nat) {wf (fun x y => is_true (x < y)) n} :=
if (n > 0) && (2 <= n) then (bit_size n./2).+1 else 0.
Proof.
- move => n.
case/andP => n_pos n_gt1.
exact: (ltn_half n_pos).
- exact: wf_ltn.
Defined.
Definition even n : bool := ~~odd n.
Lemma evenSn : forall n, even n.+1 = odd n.
Proof.
elim => [| n IH].
- done.
- rewrite /even.
rewrite -[odd n.+1]Bool.negb_involutive.
congr negb.
Qed.
Lemma oddSn: forall n, odd n.+1 = even n.
Proof.
done.
Qed.
Lemma odd_Sdouble: forall n, odd n -> n./2.*2.+1 = n.
move => n oddn.
rewrite -add1n -[1]/(nat_of_bool true) -oddn.
exact: odd_double_half.
Qed.
Implicit Arguments odd_Sdouble [n].
Lemma even_double : forall n, even n -> n = n./2.*2.
Proof.
move => n n_even.
rewrite -{1}[n]odd_double_half.
rewrite -[odd n]Bool.negb_involutive.
rewrite -[~~ odd n]/(even n).
rewrite n_even add0n.
done.
Qed.
Implicit Arguments even_double [n].
Lemma half_SS : forall n, n.+2./2 = n./2.+1.
Proof.
elim => [| n IH].
- done.
- rewrite -[(n.+3)]add3n halfD andTb -[3./2]/1 add1n.
case H: (odd n); rewrite (add1n , add0n).
+ rewrite -{2}(odd_Sdouble H).
rewrite -doubleS doubleK.
done.
+ congr _.+1.
rewrite {2}[n]even_double.
* rewrite -add1n -[1]/(nat_of_bool true).
rewrite half_bit_double.
done.
* rewrite /even.
rewrite H.
done.
Qed.
Raw
sequences.v
Require Import ssreflect eqtype ssrbool ssrnat.
Require Import prime seq div ssralg nat_aux.
Check wf_ltn.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition Seq := seq nat.
Fixpoint rep_1 (n : nat) : nat :=
match n with
| 0 => 0
| S n => (double (rep_1 n)).+1
end.
Lemma rep_succ_pos : forall n, rep_1 n.+1 > 0.
Proof.
done.
Qed.
Lemma rep_succ_odd: forall n, odd (rep_1 n.+1).
Proof.
case => [| n].
- done.
- rewrite /rep_1 - /(rep_1 n.+1).
rewrite -[odd _]Bool.negb_involutive.
rewrite -odd_Sn.
rewrite odd_double.
done.
Qed.
Definition digits (n : nat) : nat :=
match n with
| 0 => 0
| n => (bit_size n).+1
end.
Eval compute in digits 8.
Fixpoint encode (s : Seq) : nat :=
match s with
| [::] => 0
| [:: n] => (double (rep_1 n)).+1
| (n :: ns) =>
let bits := rep_1 n
in bits + 2 ^ (digits bits + 1) * encode ns
end.
Eval compute in encode [::1;2;3].
Require Import Recdef.
Function split (count : nat) (n : nat) {wf (fun x y => is_true (x < y)) n} : nat * nat :=
match n with
| 0 => (count, 0)
| S n =>
let q := n.+1./2
in if odd n.+1
then split (count.+1) q
else (count, q)
end.
Proof.
- move => count n k HS Hr.
apply ltn_half; done.
- exact: wf_ltn.
Defined.
Lemma split_le: forall n d, snd (split d n) <= n.
Proof.
elim/(well_founded_ind wf_ltn) => n IH d.
rewrite !split_equation.
case H: n => [| k].
- done.
- case: ifP => [neven | nodd].
+ apply: leq_trans.
* exact: (k.+1./2).
* apply: IH.
rewrite -H.
apply: ltn_half; try rewrite H; done.
* exact: leq_half.
+ rewrite /snd.
rewrite -{1}addn1.
rewrite halfD -[odd 1]/true odd_Sn nodd /= addn0 add1n.
apply: leq_trans.
* exact: k.
* apply: ltn_half.
- apply: odd_gt0.
rewrite odd_Sn nodd.
done.
* done.
Qed.
Lemma split_lt: forall n d, snd (split d n.+1) < n.+1.
Proof.
move => n d.
case Hnk1 : n => [| k]; rewrite split_equation //= Bool.negb_involutive.
case: ifP => [odd| even].
- apply: leq_ltn_trans.
+ exact: k.+2./2.
+ exact: split_le.
+ apply: ltn_half; done.
- rewrite /=.
case Hk: k => [| k'].
+ done.
+ rewrite -{1}[k'.+1]add1n.
rewrite -{1}[k']odd_double_half.
rewrite odd_Sn.
rewrite -[k' in odd k']Hk.
rewrite even /=.
rewrite doubleK.
rewrite -[k'.+3]/(2 + k').+1.
rewrite ltnS -[2 + k']/(1 + k').+1 !ltnS.
exact: leq_half.
Qed.
Function decode' (n : nat) {wf (fun x y => is_true (ltn x y)) n} :=
let (d, rest) := split 0 n
in if rest == 0
then [:: d - 1]
else d :: decode' rest.
Proof.
move => n d rest Hnrest rest_pos.
have H: rest = snd (split 0 n).
- rewrite Hnrest //=.
rewrite H.
rewrite H in rest_pos.
clear H Hnrest rest.
move: rest_pos.
case: n => [contr | H k].
- done.
- by apply split_lt.
exact wf_ltn.
Defined.
Definition decode (n : nat) : list nat :=
match n with
| 0 => [::]
| S n => decode' (S n)
end.
Eval compute in encode [:: 1; 2; 3].
Eval compute in decode (encode [:: 1; 2; 3]).
Eval compute in decode 12.
Eval compute in encode (decode 12).
Eval compute in encode [::].
Eval compute in decode 0.
Lemma split_0 : forall d, split d 0 = (d, 0).
Proof.
move => d; by rewrite !split_equation //=.
Qed.
Lemma half_rep : forall n, (rep_1 n.+1)./2 = rep_1 n.
Proof.
elim => [|n IH].
- done.
- rewrite {1}/rep_1.
rewrite half_odd.
rewrite -/rep_1.
done.
Qed.
Lemma split_rep : forall n d, split d (rep_1 n) = (n + d, 0).
Proof.
elim => [| k IH] d.
- done.
- rewrite split_equation.
move: (rep_succ_pos k) => repSk_pos.
rewrite -(prednK repSk_pos).
rewrite (prednK repSk_pos).
move: (rep_succ_odd k) => repSk_odd.
rewrite repSk_odd.
rewrite half_rep.
rewrite addSn -addnS.
apply IH.
Qed.
Lemma encode_cons : forall tl hd, encode tl < encode (hd :: tl).
Proof.
elim => [| hd' tl' IH n].
- done.
- rewrite /(encode (_ :: _ :: _)).
rewrite -/encode.
rewrite -/(encode (hd' :: tl')).
move kDef: (encode (hd' :: tl')) => k.
suff enc_pos: k > 0.
+ move: (digits (rep_1 n)) => l.
rewrite expnD.
rewrite expn1.
apply: ltn_addl.
apply: (ltn_Pmull _ enc_pos).
elim: l => [| u lIH].
* rewrite expn0 mul1n. done.
* rewrite expnS.
apply: ltn_trans.
exact: (2^ u * 2).
assumption.
rewrite -mulnA.
apply: ltn_Pmull.
done.
apply: (leq_trans _ lIH).
done.
+ rewrite -{}kDef.
apply: leq_ltn_trans.
* exact: encode tl'.
done.
apply IH.
Qed.
Fixpoint initseg (s1 s2 : seq nat) : bool :=
match (s1, s2) with
| ([::], _) => true
| (x :: xs, y :: ys) => (x == y) && (initseg xs ys)
| (_, _) => false
end.
Function proper_initseg (s1 s2 : seq nat) := (s1 != s2) && initseg s1 s2.
Lemma encode_cons_pos : forall tl hd, encode (hd :: tl) > 0.
Proof.
elim => hd.
- rewrite -/(encode [::]).
exact: encode_cons.
- move => tl IH hd'.
apply: (ltn_trans (IH hd)).
+ apply encode_cons.
Qed.
Lemma encode_0 : forall s, (encode s = 0) <-> (s = [::]).
Proof.
elim => [| hd tl IH].
- done.
- constructor => [enc_0| empty].
+ apply: False_ind.
apply: notF.
have enc_pos : encode (hd :: tl) > 0.
* exact: encode_cons_pos.
rewrite enc_0 in enc_pos.
done.
+ done.
Qed.
Lemma bit_size_rep: forall n, bit_size (rep_1 n.+1) = n.
Proof.
elim => [| n IH ].
- done.
- rewrite bit_size_equation.
move: (rep_succ_pos n.+1) => n2_pos.
rewrite n2_pos andTb.
have H : 1 < rep_1 n.+2.
by rewrite -(prednK n2_pos).
rewrite {}H.
rewrite half_rep.
rewrite IH.
done.
Qed.
Lemma digits_rep : forall n, digits (rep_1 n) = n.
Proof.
elim => [| n IH ].
- done.
- rewrite /digits.
move: (rep_succ_pos n) => pos.
rewrite -(prednK pos) (prednK pos).
by rewrite bit_size_rep.
Qed.
Theorem split_encode:
forall ns n d,
split d (rep_1 n + 2 ^ (digits (rep_1 n) + 1) * encode ns)
= (n + d, encode ns).
Proof.
elim => [| hd tl IH] n.
- move => d.
rewrite /encode muln0 addn0.
elim n => [| n' IH].
+ done.
+ exact: split_rep.
- elim n => [| n' IHn]; move => d.
+ rewrite /rep_1 /digits !add0n expn1.
rewrite split_equation.
rewrite mul2n.
move k_def: (encode (hd :: tl)).*2 => k.
have dbl_pos: k > 0.
* rewrite -k_def.
rewrite -[0]/0.*2.
rewrite ltn_double.
exact : encode_cons_pos.
rewrite -{1}(prednK dbl_pos).
rewrite (prednK dbl_pos).
rewrite -k_def odd_double.
rewrite doubleK.
done.
+ rewrite split_equation.
move k_def: (rep_1 n'.+1) (rep_succ_pos n') => k k_pos.
rewrite -{1}(prednK k_pos) addSn -addSn (prednK k_pos).
rewrite [digits k + 1]addn1 expnS mulnC [2 * _]mulnC mulnA muln2.
rewrite odd_add odd_double addbF.
rewrite -k_def.
rewrite rep_succ_odd.
rewrite addSn -addnS.
rewrite -IHn.
congr (split d.+1).
rewrite !digits_rep.
rewrite expnS.
rewrite halfD.
rewrite (rep_succ_odd n').
rewrite mulnA [_ * 2]mulnC -mulnA mul2n.
rewrite odd_double andbF add0n.
rewrite half_rep doubleK -muln2 -mulnA -expnSr mulnC.
by rewrite addn1.
Qed.
Lemma rep_double_succ: forall n, (rep_1 n).*2.+1 = rep_1 n.+1.
Proof.
elim => [| n IH].
- done.
- rewrite -half_rep.
move: (rep_succ_odd n.+1) => rep_odd.
rewrite -add1n -[1]/(nat_of_bool true).
rewrite -rep_odd.
by rewrite odd_double_half.
Qed.
Lemma decode_decode' : forall n, n > 0 -> decode' n = decode n.
Proof.
move => n n_pos.
rewrite /decode.
rewrite -(prednK n_pos) (prednK n_pos).
done.
Qed.
Theorem decode_encode: forall s : seq nat, decode (encode s) = s.
Proof.
elim => [| hd tl]; rewrite //=.
case Htl: tl => [| hd' tl'] IH.
- rewrite /decode.
rewrite decode'_equation rep_double_succ.
rewrite split_rep addn0 //=.
rewrite subn1 succnK.
done.
- rewrite /decode.
move ldef: (rep_1 hd + 2 ^ (digits (rep_1 hd) + 1) * (encode (hd' :: tl'))) => l.
have l_pos: l > 0.
+ rewrite -ldef.
move: ldef.
move: (encode_cons_pos tl' hd').
move kdef: (encode _) => k k_pos ldef.
rewrite addn_gt0.
have enough: (2 ^ (digits (rep_1 hd) + 1) * k > 0).
* rewrite muln_gt0.
rewrite k_pos andbT.
rewrite expn_gt0.
done.
rewrite enough orbT.
done.
rewrite -(prednK l_pos) (prednK l_pos).
rewrite -ldef -/decode decode'_equation.
rewrite split_encode.
move: (encode_cons_pos tl' hd') => e_pos.
case: ifP => [encode_zero|_].
- rewrite (eqP encode_zero) in e_pos.
done.
- rewrite addn0.
rewrite (decode_decode' e_pos).
rewrite IH.
done.
Qed.
Theorem encode_decode: forall n : nat, encode (decode n) = n.
Proof.
Admitted.
Theorem decode_monotone: forall (n m : nat),
n < m -> initseg (decode n) (decode m).
Proof.
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment