Skip to content

Instantly share code, notes, and snippets.

@mathink

mathink/show_with_proof.v

Last active December 21, 2016 14:06
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mathink/ca496c0fc2ee60c62eceec252b81be70 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mathink/ca496c0fc2ee60c62eceec252b81be70 to your computer and use it in GitHub Desktop.
Download ZIP
nat を string で十進表記する(ハードモード)
Raw
show_with_proof.v
(* safe translator from nat to string *)
Require Import Arith List Omega Ascii String Recdef Wf_nat Program.Wf Program.Tactics.
Generalizable All Variables.
Fixpoint div10 (n: nat): nat * nat :=
match n with
| S (S (S (S (S (S (S (S (S (S n'))))))))) =>
let (q, r) := div10 n' in (S q, r)
| digit => (0, digit)
end.
Eval compute in div10 8.
(* = (0, 8) *)
(* : nat * nat *)
Eval compute in div10 12.
(* = (1, 2) *)
(* : nat * nat *)
Functional Scheme div10_ind := Induction for div10 Sort Prop.
Lemma div10_lt:
forall (n: nat),
(fst (div10 n) < n \/ n = 0).
Proof.
intros n.
functional induction div10 n; auto with arith.
left.
rewrite e9 in IHp; simpl in *.
destruct IHp.
- apply lt_n_S.
now repeat apply lt_S.
- subst; simpl in *.
injection e9; intros; subst; auto with arith.
Qed.
Lemma div10_rem_lt_10:
forall (n: nat),
(snd (div10 n) < 10).
Proof.
intros n.
functional induction div10 n; simpl; auto with arith.
now rewrite e9 in IHp.
Qed.
Fixpoint contain (c: ascii)(s: string) :=
match s with
| ""%string => False
| String c' s' => c = c' \/ contain c s'
end.
Definition numeral (c: ascii) := contain c "0123456789".
Inductive numerals: string -> Prop :=
| numerals_numeral
: forall (c: ascii), numeral c -> numerals (String c ""%string)
| numerals_String
: forall (c: ascii)(s: string),
numeral c -> numerals s -> numerals (String c s).
Hint Constructors numerals.
Open Scope char_scope.
Obligation Tactic := try now unfold numeral, contain; tauto.
Program Definition digit_to_ascii (n: { m | m < 10}): {c | numeral c} :=
let (n, H) := n in
match n as n return n < 10 -> { c | numeral c } with
| 0 => fun _ => "0"
| 1 => fun _ => "1"
| 2 => fun _ => "2"
| 3 => fun _ => "3"
| 4 => fun _ => "4"
| 5 => fun _ => "5"
| 6 => fun _ => "6"
| 7 => fun _ => "7"
| 8 => fun _ => "8"
| 9 => fun _ => "9"
| _ => fun (H: _ < 10) => match (_: False) with end
end H.
Next Obligation.
intros.
repeat apply lt_S_n in H.
now elim (Nat.nlt_0_r _ H).
Qed.
Open Scope string_scope.
Obligation Tactic := program_simpl.
Fixpoint srev_aux (acc: string)(s: string): string :=
match s with
| "" => acc
| String c s' => srev_aux (String c acc) s'
end.
Definition srev := srev_aux "".
Lemma srev_aux_numerals:
forall (acc s: string),
numerals acc ->
numerals s ->
numerals (srev_aux acc s).
Proof.
now intros acc s Ha Hs; revert acc Ha; induction Hs; simpl; auto.
Qed.
Lemma srev_numerals:
forall s, numerals s -> numerals (srev s).
Proof.
intros s Hs; induction Hs; unfold srev; simpl; auto.
now apply srev_aux_numerals; auto.
Qed.
Lemma nat_10_ind:
forall (P: nat -> Prop),
P 0 ->
P 1 ->
P 2 ->
P 3 ->
P 4 ->
P 5 ->
P 6 ->
P 7 ->
P 8 ->
P 9 ->
(forall n: nat, P n -> P (10 + n)) ->
forall n: nat, P n.
Proof.
intros P H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 Hn n.
revert P H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 Hn.
induction n as [|[|[|[|[|[|[|[|[|[|n]]]]]]]]] IHn]; auto.
intros.
pattern (S n); apply (IHn (fun n => P (S n))); auto.
- now apply Hn.
- intros.
now rewrite plus_n_Sm; apply Hn.
Qed.
Lemma div10_decomp_aux:
forall (q r n: nat),
n = r + 10 * q ->
r < 10 ->
(q,r) = div10 n.
Proof.
intros q r n; revert n q r.
apply (nat_10_ind (fun n => forall q r: nat, _ -> _ -> (q,r) = div10 n));
try (intros q r Heq Hlt; assert (q = 0); [omega | subst];
simpl in *; rewrite plus_comm in Heq;
simpl in Heq; subst; auto).
intros n IH q r Heq Hlt.
destruct q; [omega |].
rewrite <- mult_n_Sm, (plus_comm _ 10), Nat.add_shuffle3 in Heq.
apply plus_reg_l in Heq.
simpl.
now rewrite <- (IH _ _ Heq).
Qed.
Lemma div10_decomp:
forall (q r: nat),
r < 10 ->
(q,r) = div10 (r + 10 * q).
Proof.
now intros; apply div10_decomp_aux.
Qed.
Lemma n_decomp_10:
forall (n: nat),
exists q r, (10 * q + r = n /\ r < 10).
Proof.
intros; exists (fst (div10 n)), (snd (div10 n)).
functional induction div10 n;
try (now split; simpl; auto with arith).
rewrite e9 in IHp.
simpl (fst _) in *; simpl (snd _) in *.
destruct IHp as [Heq Hlt].
now rewrite <- mult_n_Sm, <- plus_assoc, Nat.add_shuffle3, Heq.
Qed.
Function div10_l_aux (acc: list nat)(n: nat){wf lt n}: list nat :=
let (q,r) := div10 n in
match q with
| O => r :: acc
| S q' => (div10_l_aux (r :: acc) q)
end.
Proof.
- intros.
generalize (div10_lt n); rewrite teq.
now intros [Hlt | Heq]; [assumption | subst; simpl in teq; discriminate].
- apply lt_wf.
Defined.
Definition div10_l := div10_l_aux nil.
Check fold_left.
Lemma div10_decomp_inv:
forall n q r,
div10 n = (q, r) -> n = 10 * q + r.
Proof.
intros n; functional induction div10 n;
intros q' r' Heq; try (now injection Heq; intros; subst; auto with arith).
injection Heq; intros; subst.
now rewrite <- mult_n_Sm, <- plus_assoc, Nat.add_shuffle3, IHp with q r'; auto with arith.
Qed.
Lemma div10_l_aux_valid:
forall (n: nat)(acc: list nat),
(10 ^ (List.length acc)) * n + fold_left `(q * 10 + r) acc 0
= fold_left `(q * 10 + r) (div10_l_aux acc n) 0.
Proof.
intros n acc.
functional induction div10_l_aux acc n.
- assert (n = r /\ n < 10).
{
destruct n as [|[|[|[|[|[|[|[|[|[| n]]]]]]]]]];
try now (simpl in e; injection e; intros; subst;
split; auto with arith).
simpl in e.
now destruct (div10 n); discriminate.
}
simpl.
destruct H as [Heq Hlt]; subst n; clear e Hlt.
revert r.
induction acc as [| x acc IH].
+ simpl; intros; omega.
+ simpl (List.length _).
simpl (fold_left _ _ _).
intros.
rewrite <- (IH (r * 10 + x)).
assert (10 ^ Datatypes.length acc * (r * 10 + x) =
10 ^ S (List.length acc) * r + 10 ^ List.length acc * x).
{
rewrite mult_plus_distr_l.
rewrite Nat.pow_succ_r'.
now rewrite (mult_comm 10 _), (mult_comm r 10), mult_assoc.
}
rewrite H, <- plus_assoc.
apply f_equal2_plus; auto.
- simpl (fold_left _ _ _) in *.
rewrite <- IHl.
simpl (List.length _).
rewrite Nat.pow_succ_r', (mult_comm 10 _), <- mult_assoc.
apply div10_decomp_inv in e; subst n.
rewrite mult_plus_distr_l, <- plus_assoc.
apply f_equal2_plus; auto.
clear IHl.
revert r.
induction acc as [| x acc IH].
+ simpl; intros; omega.
+ simpl (List.length _).
simpl (fold_left _ _ _).
intros.
rewrite <- (IH (r * 10 + x)).
assert (10 ^ Datatypes.length acc * (r * 10 + x) =
10 ^ S (List.length acc) * r + 10 ^ List.length acc * x).
{
rewrite mult_plus_distr_l.
rewrite Nat.pow_succ_r'.
now rewrite (mult_comm 10 _), (mult_comm r 10), mult_assoc.
}
rewrite H, <- plus_assoc.
apply f_equal2_plus; auto.
Qed.
Lemma div10_l_valid:
forall (n: nat),
n = fold_left `(q * 10 + r) (div10_l n) 0.
Proof.
intros n; unfold div10_l.
generalize (div10_l_aux_valid n nil).
now simpl; rewrite !plus_0_r.
Qed.
Lemma div10_l_aux_lt_10:
forall (acc: list nat)(n: nat),
Forall `(m < 10) acc ->
Forall `(m < 10) (div10_l_aux acc n).
Proof.
intros acc n.
functional induction div10_l_aux acc n.
- assert (r < 10).
{
now generalize (div10_rem_lt_10 n); rewrite e.
}
intros Hacc.
now apply Forall_cons.
- assert (r < 10).
{
now generalize (div10_rem_lt_10 n); rewrite e.
}
intros Hacc; apply IHl.
now apply Forall_cons.
Qed.
Definition div10_l_lt_10 (n: nat):
Forall `(m < 10) (div10_l n) :=
div10_l_aux_lt_10 nil n (Forall_nil _).
Lemma Forall_inv':
forall (X: Type)(P: X -> Prop)(x: X)(l: list X),
Forall P (x :: l) -> P x /\ Forall P l.
Proof.
now intros X P x l H; inversion H.
Qed.
Program Fixpoint add_prop (X: Type)(l: list X)(P: X -> Prop)(H: Forall P l)
: list { x | P x } :=
match l as l return Forall P l -> list {x | P x }with
| nil => fun _ => nil
| x :: xs => fun (H: Forall P (x :: xs)) =>
(exist P x (proj1 (Forall_inv' _ P x xs H)))
:: add_prop _ xs P (proj2 (Forall_inv' _ P x xs H))
end H.
Definition nat_to_numerals_aux (n: nat): list {c | numeral c} :=
map (fun (n: {m | m < 10}) => digit_to_ascii n)
(add_prop _ _ _ (div10_l_lt_10 n)).
Program Fixpoint numeral_list_to_numerals (l: list {c | numeral c})(H: 0 < List.length l) {struct l}
: {s | numerals s} :=
match l as l return 0 < List.length l -> {s | numerals s} with
| nil => fun (H: 0 < 0) => match (lt_irrefl _ H) with end
| c :: xs =>
fun (H: 0 < S (List.length xs)) =>
let (c, Hc) := c in
match zerop (List.length xs) with
| left _ => exist numerals (String c "") _
| right Hlt =>
let (s, Hs) := numeral_list_to_numerals xs Hlt in
exist numerals (String c s) _
end
end H.
Lemma div10_l_aux_not_nil:
forall (acc: list nat)(n: nat),
0 < List.length (div10_l_aux acc n).
Proof.
intros acc n; functional induction div10_l_aux acc n.
- now simpl; auto with arith.
- now apply IHl.
Qed.
Lemma add_prop_length:
forall (X: Type)(P: X -> Prop)(l: list X)(H: Forall P l),
List.length (add_prop _ _ _ H) = List.length l.
Proof.
now induction l; simpl; auto.
Qed.
Lemma nat_to_numerals_aux_not_nil:
forall (n: nat),
0 < List.length (nat_to_numerals_aux n).
Proof.
intros; unfold nat_to_numerals_aux.
rewrite map_length, add_prop_length.
now apply div10_l_aux_not_nil.
Qed.
Definition nat_to_numerals (n: nat) :=
numeral_list_to_numerals _ (nat_to_numerals_aux_not_nil n).
(* Proofs *)
Open Scope list_scope.
Lemma div10_l_aux_decomp:
forall (acc: list nat)(q r: nat),
r < 10 ->
0 < q ->
div10_l_aux acc (q * 10 + r) = div10_l_aux (r :: acc) q.
Proof.
intros; simpl.
generalize (div10_decomp q _ H).
rewrite (plus_comm r), (mult_comm 10).
set (q * 10 + r) as n.
intros Heq.
functional induction div10_l_aux acc n.
- rewrite <- Heq in e; injection e; intros; subst; simpl.
now elim (lt_irrefl _ H0).
- now rewrite <- Heq in e; injection e; intros; subst; simpl.
Qed.
Require Import ProofIrrelevance.
Lemma add_prop_cons:
forall (X: Type)(P: X -> Prop)(x: X)(l: list X)
(Hx: P x)(Hl: Forall P l),
add_prop X (x :: l) P (Forall_cons _ Hx Hl) =
exist P x Hx :: add_prop X l P Hl.
Proof.
intros X P x l; revert P x.
induction l as [| y l IHl].
- simpl; intros.
now rewrite (proof_irrelevance _ _ Hx).
- intros.
generalize (IHl P y (proj1 (Forall_inv' _ P _ _ Hl)) (proj2 (Forall_inv' _ P _ _ Hl))).
rewrite (proof_irrelevance _ _ Hl).
intros H; rewrite H.
simpl.
rewrite (proof_irrelevance _ _ Hx).
rewrite (proof_irrelevance _ _ (proj1 (Forall_inv' _ _ _ _ Hl))).
rewrite (proof_irrelevance _ _ (proj2 (Forall_inv' _ _ _ _ Hl))).
reflexivity.
Qed.
Lemma Forall_app:
forall (X: Type)(P: X -> Prop)(l1 l2: list X),
Forall P l1 -> Forall P l2 ->
Forall P (l1 ++ l2).
Proof.
induction l1 as [| x l1 IH1]; auto.
simpl; intros.
apply Forall_inv' in H; destruct H.
now apply Forall_cons; auto.
Qed.
Lemma add_prop_app:
forall (X: Type)(P: X -> Prop)(l1 l2: list X)
(H1: Forall P l1)(H2: Forall P l2),
add_prop X (l1 ++ l2) P (Forall_app _ _ _ _ H1 H2) =
add_prop X l1 P H1 ++ add_prop X l2 P H2.
Proof.
induction l1 as [| x l1 IH]; simpl; intros.
- now rewrite (proof_irrelevance _ _ H2).
- generalize (IH l2 (proj2 (Forall_inv' _ _ _ _ H1)) H2).
rewrite (proof_irrelevance _ (proj2
(Forall_inv' X P x (l1 ++ l2) (Forall_app X P (x :: l1) l2 H1 H2))) (Forall_app X P l1 l2 (proj2 (Forall_inv' X P x l1 H1)) H2)).
intros H; rewrite H.
now rewrite (proof_irrelevance _ _ (proj1 (Forall_inv' X P x l1 H1))).
Qed.
Lemma div10_l_aux_app_aux:
forall (l acc acc': list nat)(n: nat),
l = acc ++ acc' ->
div10_l_aux l n = div10_l_aux acc n ++ acc'.
Proof.
intros l acc acc' n Heq; revert acc acc' Heq.
functional induction div10_l_aux l n.
- assert (n = r /\ n < 10).
{
destruct n as [|[|[|[|[|[|[|[|[|[| n]]]]]]]]]];
try now (simpl in e; injection e; intros; subst;
split; auto with arith).
simpl in e.
now destruct (div10 n); discriminate.
}
simpl.
destruct H as [Heq Hlt]; subst n; clear e.
destruct r as [|[|[|[|[|[|[|[|[|[| r]]]]]]]]]];
try (now simpl; intros acc' acc'' Heq; subst acc).
repeat apply lt_S_n in Hlt.
now elim (Nat.nlt_0_r _ Hlt).
- intros; rewrite IHl0 with (r :: acc0) acc'; try now simpl; rewrite Heq.
assert (r < 10).
{
now generalize (div10_rem_lt_10 n); rewrite e; simpl.
}
apply div10_decomp_inv in e; subst n.
rewrite mult_comm.
now rewrite div10_l_aux_decomp; auto with arith.
Qed.
Lemma div10_l_aux_app:
forall (acc acc': list nat)(n: nat),
div10_l_aux (acc ++ acc') n = div10_l_aux acc n ++ acc'.
Proof.
now intros; apply div10_l_aux_app_aux.
Qed.
Lemma nat_to_numerals_aux_decomp:
forall (q r: nat)(Hltr: r < 10),
0 < q ->
map (@proj1_sig _ _) (nat_to_numerals_aux (q * 10 + r)) =
map (@proj1_sig _ _) (nat_to_numerals_aux q) ++ (proj1_sig (digit_to_ascii (exist _ r Hltr)) :: nil).
Proof.
unfold nat_to_numerals_aux.
intros q r Hltr Hltq.
rewrite !map_map.
assert (proj1_sig (digit_to_ascii (exist (fun m : nat => m < 10) r Hltr)) :: nil
=
map (fun x : {m : nat | m < 10} => proj1_sig (digit_to_ascii x)) (exist _ r Hltr :: nil)).
{
reflexivity.
}
rewrite H.
rewrite <- (map_app (fun x => proj1_sig (digit_to_ascii x))).
assert (H': Forall (fun m : nat => m < 10) (r :: nil)).
{
now apply Forall_cons; auto.
}
assert (exist (fun m : nat => m < 10) r Hltr :: nil =
add_prop _ (r :: nil) _ H').
{
simpl.
now rewrite (proof_irrelevance _ (proj1 _) Hltr).
}
rewrite H0.
rewrite <- add_prop_app.
clear H0 H.
generalize (div10_l_lt_10 (q * 10 + r)); intros H.
unfold div10_l in *.
revert H.
pattern (div10_l_aux nil (q * 10 + r)).
rewrite (div10_l_aux_decomp nil q r Hltr) in *; auto.
generalize (Forall_app nat (fun m : nat => m < 10) (div10_l_aux nil q)
(r :: nil) (div10_l_lt_10 q) H').
rewrite <- div10_l_aux_app; simpl.
now intros; rewrite (proof_irrelevance _ f H).
Qed.
Lemma nat_to_numerals_aux_decomp':
forall (q r: nat)(Hltr: r < 10),
0 < q ->
nat_to_numerals_aux (q * 10 + r) =
(nat_to_numerals_aux q) ++ (digit_to_ascii (exist _ r Hltr) :: nil).
Proof.
unfold nat_to_numerals_aux.
intros q r Hltr Hltq.
assert ( (digit_to_ascii (exist (fun m : nat => m < 10) r Hltr)) :: nil
=
map (fun x : {m : nat | m < 10} => (digit_to_ascii x)) (exist _ r Hltr :: nil)).
{
reflexivity.
}
rewrite H.
rewrite <- (map_app (fun x => (digit_to_ascii x))).
assert (H': Forall (fun m : nat => m < 10) (r :: nil)).
{
now apply Forall_cons; auto.
}
assert (exist (fun m : nat => m < 10) r Hltr :: nil =
add_prop _ (r :: nil) _ H').
{
simpl.
now rewrite (proof_irrelevance _ (proj1 _) Hltr).
}
rewrite H0.
rewrite <- add_prop_app.
clear H0 H.
generalize (div10_l_lt_10 (q * 10 + r)); intros H.
unfold div10_l in *.
revert H.
pattern (div10_l_aux nil (q * 10 + r)).
rewrite (div10_l_aux_decomp nil q r Hltr) in *; auto.
generalize (Forall_app nat (fun m : nat => m < 10) (div10_l_aux nil q)
(r :: nil) (div10_l_lt_10 q) H').
rewrite <- div10_l_aux_app; simpl.
now intros; rewrite (proof_irrelevance _ f H).
Qed.
Lemma div10_l_decomp:
forall (q r: nat),
r < 10 ->
0 < q ->
div10_l (q * 10 + r) = div10_l q ++ r :: nil.
Proof.
intros q r Hltr Hltq.
unfold div10_l.
rewrite div10_l_aux_decomp; auto.
now rewrite <- div10_l_aux_app.
Qed.
Program Definition numerals_app (s1 s2: { s | numerals s}): {s | numerals s} :=
exist numerals (s1 ++ s2)%string _.
Next Obligation.
now induction H0; apply numerals_String.
Qed.
Lemma app_length_lt:
forall (X: Type)(l1 l2: list X),
0 < List.length l1 -> 0 < List.length l2 ->
0 < List.length (l1 ++ l2).
Proof.
intros; rewrite app_length.
rewrite <- (plus_0_r 0).
now apply plus_lt_compat.
Qed.
Program Definition numerals_cons (c: {c | numeral c})(s: {s | numerals s}): {s | numerals s} :=
exist numerals (String c s) _.
Lemma numeral_list_to_numerals_cons:
forall (c: {c | numeral c})(l: list {c | numeral c})(H: 0 < List.length l),
numeral_list_to_numerals (c :: l) (Nat.lt_lt_succ_r _ _ H)
= numerals_cons c (numeral_list_to_numerals _ H).
Proof.
intros c l; revert c.
induction l as [| c' l IH]; intros.
- now elim (lt_irrefl _ H).
- destruct c as [c Hc].
simpl in H.
generalize H as H'.
apply le_lt_or_eq in H.
destruct H as [Hlt | Heq].
+ intros.
apply lt_S_n in Hlt.
generalize (IH c' Hlt).
rewrite (proof_irrelevance _ _ H').
intros Heq; rewrite Heq; clear Heq IH.
generalize (Nat.lt_lt_succ_r 0 (Datatypes.length (c' :: l)) H') as H''.
simpl (List.length _).
unfold numerals_cons.
simpl (exist numerals _ _).
intros H''.
simpl.
assert (zerop (List.length l) = right Hlt).
{
destruct l; simpl.
- now elim (lt_irrefl _ Hlt).
- now rewrite (proof_irrelevance _ _ Hlt).
}
rewrite H.
destruct c' as [c' Hc'].
simpl.
now destruct (numeral_list_to_numerals l Hlt); simpl.
+ apply eq_add_S in Heq.
destruct l.
* simpl; intros.
destruct c' as [c' Hc'].
simpl.
now unfold numerals_cons; simpl.
* discriminate.
Qed.
Lemma numerals_app_valid:
forall (l1 l2: list {c | numeral c})
(H1: 0 < List.length l1)
(H2: 0 < List.length l2),
numeral_list_to_numerals (l1 ++ l2) (app_length_lt _ _ _ H1 H2) =
numerals_app (numeral_list_to_numerals l1 H1)
(numeral_list_to_numerals l2 H2).
Proof.
induction l1 as [| c l1 IH]; intros.
- now elim (lt_irrefl _ H1).
- simpl ((_ :: _) ++ l2).
assert (0 < List.length (l1 ++ l2)).
{
rewrite app_length.
now apply Nat.add_pos_r.
}
generalize (numeral_list_to_numerals_cons c (l1 ++ l2) H); intros Heq.
rewrite (proof_irrelevance _ (Nat.lt_lt_succ_r 0 (Datatypes.length (l1 ++ l2)) H) (app_length_lt {c0 : ascii | numeral c0} (c :: l1) l2 H1 H2)) in Heq.
rewrite Heq; clear Heq.
revert c H1.
case_eq (zerop (List.length l1)).
+ intros e Heq c Hlt; simpl.
rewrite Heq; simpl.
destruct c as [c Hc]; simpl.
unfold numerals_cons, numerals_app.
simpl.
destruct l1; [| discriminate]; simpl in *.
rewrite (proof_irrelevance _ H2 H).
now rewrite (proof_irrelevance _ (numerals_cons_obligation_1 (exist (fun c0 : ascii => numeral c0) c Hc) (numeral_list_to_numerals l2 H)) (numerals_app_obligation_1 (exist numerals (String c "") (numerals_numeral c Hc)) (numeral_list_to_numerals l2 H))).
+ intros H1 Heq c Hlt.
simpl.
rewrite Heq; clear Heq.
destruct c as [c Hc]; simpl.
generalize (IH l2 H1 H2).
rewrite (proof_irrelevance _ (app_length_lt {c0 : ascii | numeral c0} l1 l2 H1 H2) H).
intros Heq; rewrite Heq.
unfold numerals_cons, numerals_app.
destruct (numeral_list_to_numerals l1 H1); simpl.
now rewrite (proof_irrelevance _ (numerals_String c (x ++ proj1_sig (numeral_list_to_numerals l2 H2)) Hc (numerals_app_obligation_1 (exist (fun s : string => numerals s) x n) (numeral_list_to_numerals l2 H2))) (numerals_app_obligation_1 (exist numerals (String c x) (numerals_String c x Hc n)) (numeral_list_to_numerals l2 H2))).
Qed.
Program Definition numeral_numerals (c: {c | numeral c}): {s | numerals s} :=
exist numerals (String c ""%string) _.
Lemma nat_to_numerals_decomp:
forall (q r: nat)(Hltr: r < 10),
0 < q ->
(nat_to_numerals (q * 10 + r)) =
numerals_app (nat_to_numerals q) (numeral_numerals (digit_to_ascii (exist _ r Hltr))).
Proof.
unfold nat_to_numerals; intros.
generalize (nat_to_numerals_aux_not_nil (q * 10 + r)) as Hlt.
rewrite (nat_to_numerals_aux_decomp' _ _ Hltr); auto.
intros Hlt.
assert (0 < List.length (nat_to_numerals_aux q)).
{
unfold nat_to_numerals_aux.
rewrite map_length, add_prop_length.
unfold div10_l.
now apply div10_l_aux_not_nil.
}
generalize (numerals_app_valid (nat_to_numerals_aux q) (digit_to_ascii (exist (fun m : nat => m < 10) r Hltr) :: nil) H0 (Nat.lt_0_succ _)); intros Heq.
rewrite (proof_irrelevance _ (app_length_lt {c : ascii | numeral c} (nat_to_numerals_aux q)
(digit_to_ascii (exist (fun m : nat => m < 10) r Hltr) :: nil) H0
(Nat.lt_0_succ 0)) Hlt) in Heq.
rewrite Heq; clear Heq.
rewrite (proof_irrelevance _ (nat_to_numerals_aux_not_nil q) H0).
destruct r as [|[|[|[|[|[|[|[|[|[|r]]]]]]]]]];
try now simpl; auto.
clear Hlt.
generalize Hltr; intros.
repeat apply lt_S_n in Hltr.
now elim (Nat.nlt_0_r _ Hltr).
Qed.
(* *)
Open Scope char_scope.
Definition numeral_to_digit (c: { c | numeral c }): { m | m < 10 }.
refine (let (c, Hc) := c in
match c as c return numeral c -> { m | m < 10 } with
| "0" => fun Hc => exist `(m < 10) 0 _
| "1" => fun Hc => exist `(m < 10) 1 _
| "2" => fun Hc => exist `(m < 10) 2 _
| "3" => fun Hc => exist `(m < 10) 3 _
| "4" => fun Hc => exist `(m < 10) 4 _
| "5" => fun Hc => exist `(m < 10) 5 _
| "6" => fun Hc => exist `(m < 10) 6 _
| "7" => fun Hc => exist `(m < 10) 7 _
| "8" => fun Hc => exist `(m < 10) 8 _
| "9" => fun Hc => exist `(m < 10) 9 _
| Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
fun H => match (_:False) with end
end Hc); auto with arith;
unfold numeral, contain in H;
destruct H as [H0 |[H1 |[H2 |[H3 |[H4 |[H5 |[H6 |[H7 |[H8 |[H9 | F]]]]]]]]]]; try discriminate; contradiction.
Defined.
Lemma numerals_inv:
forall (c: ascii)(s: string),
numerals (String c s) -> numeral c.
Proof.
now intros c s H; inversion H.
Qed.
Lemma numerals_inv':
forall (c c': ascii)(s: string),
numerals (String c (String c' s)) ->
numerals (String c' s).
Proof.
now intros c s s' H; inversion H.
Qed.
Fixpoint string_to_ascii_list (s: string): list ascii :=
match s with
| ""%string => nil
| String c s' => c :: string_to_ascii_list s'
end.
Lemma numerals_all_numeral:
forall s, numerals s ->
Forall numeral (string_to_ascii_list s).
Proof.
now intros s Hs; induction Hs; simpl; apply Forall_cons; auto.
Qed.
Definition numerals_to_numeral_list (s: {s | numerals s}): list {c | numeral c} :=
let (s, Hs) := s in
add_prop _ (string_to_ascii_list s)
numeral (numerals_all_numeral s Hs).
Definition numerals_to_nat (s : {s | numerals s}): nat :=
fold_left (fun n m => n * 10 + proj1_sig m)
(map numeral_to_digit (numerals_to_numeral_list s)) 0.
Lemma test: numerals "2361".
Proof.
do 3 (apply numerals_String; [unfold numeral; simpl; tauto |]).
apply numerals_numeral; unfold numeral; simpl; tauto.
Qed.
Eval compute in numerals_to_nat (exist numerals _ test).
(* = 2361 *)
(* : nat *)
Lemma string_to_ascii_list_app:
forall (s1 s2: string),
string_to_ascii_list (append s1 s2) =
string_to_ascii_list s1 ++ string_to_ascii_list s2.
Proof.
induction s1 as [| c s1 IH]; simpl; auto.
now intros s2; rewrite IH.
Qed.
Lemma Forall_app_inv:
forall (X: Type)(P: X -> Prop)(l1 l2: list X),
Forall P (l1 ++ l2) -> Forall P l1 /\ Forall P l2.
Proof.
induction l1; auto.
simpl; intros l2 Hf.
inversion Hf; subst.
now split; [apply Forall_cons; auto; apply IHl1 with l2 | apply IHl1].
Qed.
Lemma fold_left_cons:
forall (A B: Type)(f: A -> B -> A)(l: list B)(e: A)(x: B),
fold_left f (x :: l) e = fold_left f l (f e x).
Proof.
reflexivity.
Qed.
Lemma numerals_to_nat_app:
forall (s1 s2: {s | numerals s}),
numerals_to_nat (numerals_app s1 s2) =
(10 ^ length (proj1_sig s2)) * numerals_to_nat s1 +
numerals_to_nat s2.
Proof.
intros [s1 Hs1] [s2 Hs2].
simpl.
unfold numerals_to_nat.
set (fun (n: nat)(m: {m : nat | m < 10}) => n * 10 + proj1_sig m) as f in *.
unfold numerals_to_numeral_list, numerals_app.
simpl (proj1_sig (exist _ _ _)).
generalize (numerals_all_numeral (s1 ++ s2)
(numerals_app_obligation_1
(exist (fun s : string => numerals s) s1 Hs1)
(exist (fun s : string => numerals s) s2 Hs2))) as Hf.
rewrite string_to_ascii_list_app; intros Hf.
generalize Hf as Hf'; intros.
apply Forall_app_inv in Hf.
destruct Hf as [Hf1 Hf2].
generalize (add_prop_app _ numeral (string_to_ascii_list s1) (string_to_ascii_list s2) Hf1 Hf2) as Heq; intros.
rewrite (proof_irrelevance _ _ Hf') in Heq.
rewrite Heq.
rewrite map_app.
clear Heq Hf'.
rewrite (proof_irrelevance _ Hf1 (numerals_all_numeral _ Hs1)).
rewrite (proof_irrelevance _ Hf2 (numerals_all_numeral _ Hs2)).
clear Hf1 Hf2.
revert s1 Hs1.
induction s2 as [| c2 s2 IH2].
- now inversion Hs2.
- inversion Hs2; subst.
+ simpl (length _).
simpl (_ ^ _).
assert (map numeral_to_digit
(add_prop ascii (string_to_ascii_list (String c2 "")) numeral
(numerals_all_numeral (String c2 "") Hs2)) = numeral_to_digit (exist _ c2 H0) :: nil).
{
unfold numeral in H0.
repeat destruct H0 as [H | H0]; subst; try reflexivity.
now elim H0.
}
rewrite H in *.
intros s1 Hs1.
rewrite fold_left_app.
rewrite fold_left_cons.
unfold numeral in H0.
repeat destruct H0 as [H' | H0]; subst;
now rewrite (mult_comm 10); subst f; simpl.
+ simpl (length _).
rewrite Nat.pow_succ_r'.
intros s1 Hs1.
rewrite <- mult_assoc, (mult_comm 10).
simpl (string_to_ascii_list _) in *.
simpl (add_prop _ (_ :: _) _ _).
rewrite map_cons.
rewrite (proof_irrelevance _ _ H1).
assert (H: numerals (append s1 (String c2 ""))).
{
clear IH2.
induction Hs1; auto.
- simpl.
now apply numerals_String; auto.
- simpl.
now apply numerals_String.
}
generalize (IH2 H2 _ H); clear IH2.
generalize (numerals_all_numeral (s1 ++ String c2 "") H) as H1'.
rewrite string_to_ascii_list_app.
intros H1'; generalize H1' as H1''.
apply Forall_app_inv in H1'.
destruct H1'; intros H1''.
generalize (add_prop_app ascii numeral _ _ H0 H3); intros H4.
rewrite (proof_irrelevance _ _ H1'') in H4.
rewrite H4; clear H4.
rewrite map_app.
rewrite (proof_irrelevance _ H0 (numerals_all_numeral s1 Hs1)); clear H0.
assert (map numeral_to_digit
(add_prop ascii (string_to_ascii_list (String c2 "")) numeral
H3) = numeral_to_digit (exist _ c2 H1) :: nil).
{
unfold numeral in H1.
repeat destruct H1 as [H' | H1]; subst; try reflexivity.
now elim H1.
}
rewrite H0.
intros.
set (map numeral_to_digit
(add_prop ascii (string_to_ascii_list s1) numeral
(numerals_all_numeral s1 Hs1))) as x in *.
rewrite (proof_irrelevance _ (proj2 _) (numerals_all_numeral s2 H2)).
set (map numeral_to_digit
(add_prop ascii (string_to_ascii_list s2) numeral
(numerals_all_numeral s2 H2))) as y in *.
rewrite <- app_assoc in H4.
set (numeral_to_digit (exist numeral c2 H1)) as n in *.
simpl (_ ++ (_ :: nil) ++ _) in H4.
rewrite H4; clear H4.
rewrite fold_left_app, fold_left_cons.
simpl.
subst f; simpl.
set (fun (n: nat)(m: {m | m < 10}) => n * 10 + proj1_sig m) as f.
rewrite mult_plus_distr_l, mult_assoc.
rewrite <- plus_assoc.
apply f_equal2_plus; auto.
clear x.
assert (length s2 = List.length y).
{
subst y.
rewrite map_length, add_prop_length.
clear c2 Hs2 H1 H2 s1 Hs1 H H3 H1'' n H0 f.
induction s2; auto.
now simpl; rewrite IHs2.
}
rewrite H4; clear H4.
assert (proj1_sig n = f 0 n).
{
now subst f; simpl.
}
rewrite H4; clear H4.
assert (forall y x n,
10 ^ Datatypes.length y * f x n + fold_left f y 0 =
fold_left f y (f x n)
).
{
induction y0 as [| m y0 IHy].
- intros; simpl; omega.
- intros.
simpl (List.length _).
rewrite Nat.pow_succ_r', !(mult_comm 10).
simpl.
rewrite <- IHy.
rewrite <- IHy.
subst f.
simpl.
set (fold_left
(fun (n1 : nat) (m0 : {m0 : nat | m0 < 10}) => n1 * 10 + proj1_sig m0)
y0 0) as p.
set (10 ^ List.length y0) as e.
rewrite !mult_plus_distr_l.
rewrite mult_plus_distr_r.
rewrite !mult_plus_distr_l.
rewrite <- !plus_assoc.
ring.
}
apply H4.
Qed.
Lemma lt_ind:
forall (P: nat -> Prop),
(forall m, (forall n, n < m -> P n) -> P m) ->
forall n, P n.
Proof.
intros P IH n.
revert P IH; induction n as [| n IHn].
- intros; apply IH.
now intros n Hlt; inversion Hlt.
- intros.
apply (IHn (fun n => P (S n))).
intros.
apply IH.
intros n' Hlt.
destruct n' as [| n'].
+ apply IH.
intros.
now inversion H0.
+ apply lt_S_n in Hlt.
now apply H.
Qed.
(* *)
Theorem nat_to_numerals_to_nat:
forall (n: nat),
numerals_to_nat (nat_to_numerals n) = n.
Proof.
apply lt_ind.
intros n IH.
destruct (n_decomp_10 n) as [q [r [Heq Hlt]]].
rewrite <- Heq, mult_comm.
destruct q as [| q].
-
destruct r as [|[|[|[|[|[|[|[|[|[| r]]]]]]]]]];
try (repeat apply lt_S_n in Hlt; elim (Nat.nlt_0_r _ Hlt));
now compute.
- rewrite (nat_to_numerals_decomp _ _ Hlt); auto with arith.
rewrite numerals_to_nat_app.
simpl (length _).
simpl (_ ^ _).
assert (numerals_to_nat
(numeral_numerals
(digit_to_ascii (exist (fun m : nat => m < 10) r Hlt))) = r).
{
destruct r as [|[|[|[|[|[|[|[|[|[| r]]]]]]]]]];
try (generalize Hlt; repeat apply lt_S_n in Hlt; elim (Nat.nlt_0_r _ Hlt)); now compute.
}
rewrite H; clear H.
rewrite (mult_comm 10).
apply f_equal2_plus; auto.
apply f_equal2_mult; auto.
apply IH.
rewrite <- Heq.
omega.
Qed.
(* *)
Fixpoint normalize_numerals_aux (s: string): string :=
match s with
| String "0" "" => s
| String "0" s' => normalize_numerals_aux s'
| _ => s
end.
Lemma normalize_numerals_aux_valid:
forall s, numerals s -> numerals (normalize_numerals_aux s).
Proof.
intros s Hs; induction Hs.
- destruct H as [H0 | H].
+ subst c; simpl; auto.
now apply numerals_numeral; unfold numeral; left.
+ repeat destruct H as [Heq | H]; subst; try (now elim H);
apply numerals_numeral; unfold numeral; simpl; tauto.
- repeat destruct H as [Heq | H]; subst; try (now elim H);
try (now simpl;inversion Hs; subst; auto); (* for 0 *)
try (now simpl; apply numerals_String; unfold numeral; simpl; tauto).
Qed.
Definition normalize_numerals (s: {s | numerals s}): {s | numerals s} :=
let (s, Hs) := s in
exist numerals _ (normalize_numerals_aux_valid _ Hs).
Theorem numerals_to_nat_numerals:
forall (s: string)(Hs: numerals s),
(nat_to_numerals (numerals_to_nat (exist numerals s Hs))) =
(normalize_numerals (exist numerals s Hs)).
Proof.
Admitted.
Lemma irrelevance_exist_eq:
forall (X: Type)(P: X -> Prop)(x y: X)(Hx: P x)(Hy: P y),
x = y -> exist P x Hx = exist P y Hy.
Proof.
intros; subst.
now rewrite (proof_irrelevance _ Hx Hy).
Qed.
Lemma normalize_nothing:
forall (c: ascii)(s: string),
numeral c -> numerals s ->
c <> "0" ->
normalize_numerals_aux (String c s) = String c s.
Proof.
intros c s Hc Hs Hneq.
repeat destruct Hc as [Heq | Hc]; subst; try (now elim Hc);
simpl; auto.
now elim (Hneq (eq_refl _)).
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment