proposition: Lemma dnorm_spec_i d : let (i, f) := match d with Decimal i f => (i, f) | DecimalExp i f _ => (i, f) end in let i' := match dnorm d with Decimal i _ => i | DecimalExp i _ _ => i end in match i with | Pos i => i' = Pos (unorm i) | Neg i => (i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil)) \/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil)) end.
proof: Proof. case d as [i f|i f e]; case i as [i|i]. - now simpl. - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + rewrite Ha; right; split; [now simpl|split]. * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + left; split; [now revert Ha; case nzhead|]. case (uint_eq_dec (nzhead i) Nil). * intro Hi; right; intro Hf; apply Ha. now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. * now intro H; left. - simpl; case (norm e); clear e; intro e; [|now simpl]. now case e; clear e; [|intro e..]; [|case e|..]. - simpl. set (m := match nzhead _ with Nil => _ | _ => _ end). set (m' := match _ with Decimal _ _ => _ | _ => _ end). replace m' with m. 2:{ unfold m'; case (norm e); clear m' e; intro e; [|now simpl]. now case e; clear e; [|intro e..]; [|case e|..]. } unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha. + rewrite Ha; right; split; [now simpl|split]. * now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha). * now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha). + left; split; [now revert Ha; case nzhead|]. case (uint_eq_dec (nzhead i) Nil). * intro Hi; right; intro Hf; apply Ha. now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. * now intro H; left. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith