proposition: Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d.
proof: Proof. case d as [i f|i f e]; case i as [i|i]. - now simpl; rewrite unorm_involutive. - simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. set (m := match nzhead _ with Nil =>_ | _ => _ end). replace m with (Neg (unorm i)). 2:{ now unfold m; revert Ha; case nzhead. } case (uint_eq_dec (nzhead i) Nil); intro Hi. + unfold unorm; rewrite Hi; simpl. case (uint_eq_dec (nzhead f) Nil). * intro Hf; exfalso; apply Ha. now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. * now case nzhead. + rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. now revert Ha; case nzhead. - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He. + now rewrite He; simpl; rewrite unorm_involutive. + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). replace m with (HexadecimalExp (Pos (unorm i)) f (Decimal.norm e)). 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. now case e; clear e; [|intro e; case e|..]. } simpl; rewrite DecimalFacts.norm_involutive, unorm_involutive. revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. now case e; clear e; [|intro e; case e|..]. - simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He. + rewrite He; simpl. case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. set (m := match nzhead _ with Nil =>_ | _ => _ end). replace m with (Neg (unorm i)). 2:{ now unfold m; revert Ha; case nzhead. } case (uint_eq_dec (nzhead i) Nil); intro Hi. * unfold unorm; rewrite Hi; simpl. case (uint_eq_dec (nzhead f) Nil). -- intro Hf; exfalso; apply Ha. now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. -- now case nzhead. * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. now revert Ha; case nzhead. + set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end). replace m with (HexadecimalExp i' f (Decimal.norm e)). 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. now case e; clear e; [|intro e; case e|..]. } simpl; rewrite DecimalFacts.norm_involutive. set (i'' := match i' with Pos _ => _ | _ => _ end). clear m; set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end). replace m with (HexadecimalExp i'' f (Decimal.norm e)). 2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl]. now case e; clear e; [|intro e; case e|..]. } unfold i'', i'. case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha]. fold i'; replace i' with (Neg (unorm i)). 2:{ now unfold i'; revert Ha; case nzhead. } case (uint_eq_dec (nzhead i) Nil); intro Hi. * unfold unorm; rewrite Hi; simpl. case (uint_eq_dec (nzhead f) Nil). -- intro Hf; exfalso; apply Ha. now rewrite <-nzhead_app_nzhead, Hi, app_nil_l. -- now case nzhead. * rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead. now revert Ha; case nzhead. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith