Library UniMath.NumberSystems.Tests

Require UniMath.Foundations.NaturalNumbers.
Require UniMath.MoreFoundations.DecidablePropositions.
Require UniMath.MoreFoundations.NegativePropositions.

Module Test_nat.

  Import UniMath.Foundations.NaturalNumbers.
  Import UniMath.MoreFoundations.DecidablePropositions.
  Import UniMath.MoreFoundations.NegativePropositions.

  Local Open Scope nat_scope.

  Goal 3 5. exact tt. Defined.
  Goal ¬ (3 3). intro n. apply n. Defined.

  Module Test_A.
    Let C := compl nat 0.
    Let C' := compl_ne nat 0 (λ m, 0 m).
    Let w := compl_ne_weq_compl nat 0 (λ m, 0 m) : C C'.
    Let cn : C := (3,,negpaths0sx _).
    Let cn' : C' := (3,,tt).
    Goal w cn = cn'. reflexivity. Defined.
    Goal invmap w cn' = cn. reflexivity. Defined.
    Goal homotinvweqweq w cn = idpath _. try reflexivity. Abort.     Goal homotweqinvweq w cn' = idpath _. reflexivity. Defined.     Let f := weqrecompl nat 0 (isdeceqnat 0).
    Let f' := weqrecompl_ne nat 0 (isdeceqnat 0) (λ m, 0 m).
    Goal f (ii1 cn) = 3. reflexivity. Defined.
    Goal f' (ii1 cn') = 3. reflexivity. Defined.
    Goal invmap f 3 = (ii1 cn). reflexivity. Defined.
    Goal invmap f' 3 = (ii1 cn'). reflexivity. Defined.
    Goal homotweqinvweq f 3 = idpath _. reflexivity. Defined.
    Goal homotweqinvweq f' 3 = idpath _. reflexivity. Defined.
    Goal homotinvweqweq f (ii1 cn) = idpath _. try reflexivity. Abort.     Goal homotinvweqweq f' (ii1 cn') = idpath _. reflexivity. Defined.   End Test_A.

  Goal choice (3 < 4)%dnat true false = true. reflexivity. Defined.
  Goal choice (3 < 4 4 < 5)%dnat%declog true false = true. reflexivity. Defined.
  Goal choice (¬ (3 < 4))%dnat%declog true false = false. reflexivity. Defined.
  Goal choice (3 < 4 4 < 3)%dnat%declog true false = true. reflexivity. Defined.
  Goal choice (4 < 3 2 < 1)%dnat%declog true false = false. reflexivity. Defined.

  Goal si 3 (di 3 2) = 2. reflexivity. Defined.
  Goal si 3 (di 3 3) = 3. reflexivity. Defined.
  Goal si 3 (di 3 4) = 4. reflexivity. Defined.

  Goal si 3 2 = 2. reflexivity. Defined.
  Goal si 3 3 = 3. reflexivity. Defined.
  Goal si 3 4 = 3. reflexivity. Defined.
  Goal si 3 5 = 4. reflexivity. Defined.

  Module Test_weqdicompl.

    Let w := weqdicompl 3 : nat nat_compl 3.
    Goal w 2 = (2,,tt). reflexivity. Defined.
    Goal w 3 = (4,,tt). reflexivity. Defined.
    Goal invmap w (2,,tt) = 2. reflexivity. Defined.
    Goal invmap w (4,,tt) = 3. reflexivity. Defined.
    Goal homotweqinvweq w (2,,tt) = idpath _. reflexivity. Defined.
    Goal homotweqinvweq w (4,,tt) = idpath _. reflexivity. Defined.
    Goal homotinvweqweq w 2 = idpath _. reflexivity. Defined.
    Goal homotinvweqweq w 4 = idpath _. reflexivity. Defined.
    Goal homotweqinvweqweq w 2 = idpath _. reflexivity. Defined.
    Goal homotweqinvweqweq w 4 = idpath _. reflexivity. Defined.

  End Test_weqdicompl.

End Test_nat.

Require UniMath.Algebra.IteratedBinaryOperations.
Require UniMath.Combinatorics.FiniteSets.
Require UniMath.NumberSystems.NaturalNumbersAlgebra.

Module Test_finsum.

  Import UniMath.Algebra.IteratedBinaryOperations.
  Import UniMath.Combinatorics.FiniteSets.
  Import UniMath.NumberSystems.NaturalNumbersAlgebra.

  Goal X (fin : finstruct X) (f : X nat),
    finsum (hinhpr fin) f = stnsum (f pr1weq (pr2 fin)).
  Proof.
    intros.
    intermediate_path (iterop_fun_mon (M := nataddabmonoid) (f pr1weq (pr2 fin))).
    - reflexivity.
    - apply iterop_fun_nat.
  Qed.

  Goal 15 = finsum (isfinitestn _) (λ i:stn 6, i). reflexivity. Qed.
  Goal 20 = finsum isfinitebool (λ i:bool, 10). reflexivity. Qed.
  Goal 21 = finsum (isfinitecoprod isfinitebool isfinitebool)
                   (coprod_rect (λ _, nat) (bool_rect _ 10 4) (bool_rect _ 6 1)).
    reflexivity.   Qed.

  Goal 10 = finsum' (isfinitestn _) (λ i:stn 5, i). reflexivity. Defined.   Goal 20 = finsum' isfinitebool (λ i:bool, 10). reflexivity. Qed.
  Goal 21 = finsum' (isfinitecoprod isfinitebool isfinitebool)
                   (coprod_rect (λ _, nat) (bool_rect _ 10 4) (bool_rect _ 6 1)).
    try reflexivity.   Abort.

  Section Iteration.
    Local Notation "s □ x" := (append s x) (at level 64, left associativity).
    Context (G:abgr) (R:ring) (S:commring) (g g' g'':G) (r r' r'':R) (s s' s'':S).
    Local Open Scope multmonoid.
    Goal iterop_unoseq_abgr (nil : Sequence G) = 1. reflexivity. Qed.
    Goal iterop_unoseq_abgr (nil g g') = g×g'. reflexivity. Qed.
    Goal iterop_unoseq_abgr (nil g g' g'') = g×g'×g''. reflexivity. Qed.
    Goal iterop_unoseq_unoseq_mon (M:=G) (sequenceToUnorderedSequence(nil sequenceToUnorderedSequence(nil g g') sequenceToUnorderedSequence(nil g g' g''))) = (g×g') × (g×g'×g''). reflexivity. Qed.
    Goal iterop_unoseq_unoseq_mon (M:=G) (sequenceToUnorderedSequence(nil sequenceToUnorderedSequence(nil g) sequenceToUnorderedSequence(nil))) = g × 1. reflexivity. Qed.
    Goal iterop_unoseq_unoseq_mon (M:=G) (sequenceToUnorderedSequence(nil sequenceToUnorderedSequence(nil) sequenceToUnorderedSequence(nil g))) = 1 × g. reflexivity. Qed.
    Close Scope multmonoid.

    Local Open Scope ring.
    Goal sum_unoseq_ring (nil : Sequence R) = 0. reflexivity. Qed.
    Goal sum_unoseq_ring (nil r r') = r+r'. reflexivity. Qed.
    Goal sum_unoseq_ring (nil r r' r'') = r+r'+r''. reflexivity. Qed.
    Goal product_unoseq_ring (nil : Sequence S) = 1. reflexivity. Qed.
    Goal product_unoseq_ring (nil s s') = s×s'. reflexivity. Qed.
    Goal product_unoseq_ring (nil s s' s'') = s×s'×s''. reflexivity. Qed.
  End Iteration.

End Test_finsum.

Require UniMath.NumberSystems.Integers.

Module Test_int.

  Import UniMath.NumberSystems.Integers.

  Goal true = (hzbooleq (natnattohz 3 4) (natnattohz 17 18)) . reflexivity. Qed.
  Goal false = (hzbooleq (natnattohz 3 4) (natnattohz 17 19)) . reflexivity. Qed.
  Goal 2 × 100 + 7 × 10 + 4 = (hzabsval (natnattohz (5 × 10 + 8) (3 × 100 + 3 × 10 + 2))) . reflexivity. Qed.
  Goal O = (hzabsval (hzplus (natnattohz 2 3) (natnattohz 3 2))) . reflexivity. Qed.
  Goal 2 = (hzabsval (hzminus (natnattohz 2 3) (natnattohz 3 2))) . reflexivity. Qed.
  Goal 3 × 100 = (hzabsval (hzmult (natnattohz (2 × 10) (5 × 10)) (natnattohz (3 × 10) (2 × 10)))) . reflexivity. Qed.

End Test_int.

Require UniMath.NumberSystems.RationalNumbers.

Module Test_rat.

  Import UniMath.NumberSystems.RationalNumbers.

  Open Scope hz_scope .

  Open Scope hq_scope .

  Transparent hz .

  Goal true = ( hqbooleq ( hzhztohq ( natnattohz 4 0 ) ( tpair _ ( natnattohz 3 0 ) ( ct ( hzneq , isdecrelhzneq, ( natnattohz 3 0 ) , 0 %hz ) ) ) ) ( hzhztohq ( natnattohz 13 1 ) ( tpair _ ( natnattohz 11 2 ) ( ct ( hzneq , isdecrelhzneq , ( natnattohz 11 2 ) , 0 %hz ) ) ) ) ) . reflexivity. Qed.

  Goal true = ( decreltobrel hqgthdec ( hzhztohq ( natnattohz 5 0 ) ( tpair _ ( natnattohz 3 0 ) ( ct ( hzneq , isdecrelhzneq , ( natnattohz 3 0 ) , hzzero ) ) ) ) ( hzhztohq ( natnattohz 13 1 ) ( tpair _ ( natnattohz 11 2 ) ( ct ( hzneq , isdecrelhzneq , ( natnattohz 11 2 ) , hzzero ) ) ) ) ) . reflexivity. Qed.

  Goal 4 = ( hzabsval ( intpart ( hqdiv ( hztohq ( nattohz ( 10 ) ) ) ( - ( 1 + 1 + 1 ) ) ) ) ) . reflexivity. Qed.

End Test_rat.