Library UniMath.Combinatorics.Tests
Require Import UniMath.Foundations.Preamble.
Require UniMath.Combinatorics.Lists.
Require UniMath.Combinatorics.StandardFiniteSets.
Require UniMath.Combinatorics.FiniteSets.
Require UniMath.Combinatorics.FiniteSequences.
Require UniMath.Combinatorics.FiniteSets.
Require UniMath.Combinatorics.OrderedSets.
Require UniMath.Combinatorics.StandardFiniteSets.
Require UniMath.Combinatorics.BoundedSearch.
Require UniMath.MoreFoundations.DecidablePropositions.
Require UniMath.MoreFoundations.NegativePropositions.
Module Test_list.
Import UniMath.Combinatorics.Lists.
Local Notation "[]" := nil (at level 0, format "[]").
Local Infix "::" := cons.
Goal concatenate (1::2::[]) (3::4::5::[]) = (1::2::3::4::5::[]).
reflexivity.
Defined.
Goal flatten ((1::2::[])::(3::4::5::[])::(6::[])::[]) = (1::2::3::4::5::6::[]).
reflexivity.
Defined.
End Test_list.
Module Test_stn.
Import UniMath.Combinatorics.StandardFiniteSets.
Import UniMath.MoreFoundations.NegativePropositions.
Local Open Scope stn.
Goal stn 6. exact (stnel(6,3)). Qed.
Goal stn 6. exact (stnpr 3). Qed.
Goal (stnel(6,3) ≠ stnel(6,4)). exact tt. Defined.
Goal ¬(stnel(6,3) ≠ stnel(6,3)). intro n. apply n. Defined.
Goal ∏ m n (i:m≤n) (j:stn m), pr1 (stnmtostnn m n i j) = pr1 j.
intros. induction j as [j J]. reflexivity.
Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●2)) = ●2. reflexivity. Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●3)) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●4)) = ●4. reflexivity. Defined.
Goal @sni 6 (●3) (●2) = ●2. reflexivity. Defined.
Goal @sni 6 (●3) (●3) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (●4) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (●5) = ●4. reflexivity. Defined.
Module Test_weqdnicompl.
Let n := 5.
Let X := stn n.
Let i := ●3 : stn (S n).
Let Y := @stn_compl (S n) i.
Let v := weqdnicompl i : X ≃ Y.
Let j := ●4 : X.
Let jni := ●5,,tt : Y.
Goal v j = jni. reflexivity. Defined.
Goal invmap v jni = j. reflexivity. Defined.
Goal homotweqinvweq v jni = idpath _. reflexivity. Defined.
Goal homotinvweqweq v j = idpath _.
reflexivity. Defined. Goal homotweqinvweqweq v j = idpath _. reflexivity. Defined.
End Test_weqdnicompl.
Module Test2.
Goal weqdnicoprod 4 firstelement (ii1 (●0)) = ●1. reflexivity. Defined.
Goal weqdnicoprod 4 firstelement (ii1 (●3)) = ●4. reflexivity. Defined.
Goal invmap (weqdnicoprod 4 firstelement) (●1) = (ii1 (●0)). reflexivity. Defined.
Goal invmap (weqdnicoprod 4 firstelement) (●4) = (ii1 (●3)). reflexivity. Defined.
Goal weqdnicoprod 4 lastelement (ii1 (●3)) = ●3. reflexivity. Defined.
Goal weqdnicoprod 4 lastelement (ii2 tt) = ●4. reflexivity. Defined.
Goal invmap (weqdnicoprod 4 lastelement) (●1) = (ii1 (●1)). reflexivity. Defined.
Goal invmap (weqdnicoprod 4 lastelement) (●4) = (ii2 tt). reflexivity. Defined.
Goal homotweqinvweq (weqdnicoprod 4 lastelement) (● 0) = idpath _. reflexivity. Defined. Goal homotinvweqweq (weqdnicoprod 4 (●4)) (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq (weqdnicoprod 4 (●4)) (ii1 (●1)) = idpath _.
reflexivity. Defined.
Local Definition w : unit ≃ stn 1.
simple refine (weq_iso _ _ _ _).
{ intro. exact firstelement. }
{ intro. exact tt. }
{ intro u. simpl. induction u. reflexivity. }
{ intro i. simpl. apply subtypeEquality_prop.
simpl. induction i as [i I]. simpl. apply pathsinv0. apply natlth1tois0. exact I. }
Defined.
Goal w tt = firstelement. reflexivity. Defined.
Goal invmap w firstelement = tt. reflexivity. Defined.
Goal homotweqinvweq w firstelement = idpath _. reflexivity. Defined.
Goal homotinvweqweq w tt = idpath _. reflexivity. Defined.
Local Definition w' := invweq w.
Goal w' firstelement = tt. reflexivity. Defined.
Goal invmap w' tt= firstelement. reflexivity. Defined.
Goal homotweqinvweq w' tt = idpath _. reflexivity. Defined.
Goal homotinvweqweq w' firstelement = idpath _. reflexivity. Defined.
Definition ww' := weqcomp w w'.
Goal ww' tt = tt. reflexivity. Defined.
Goal invmap ww' tt = tt. reflexivity. Defined.
Goal homotweqinvweq ww' tt = idpath _. reflexivity. Defined.
Goal homotinvweqweq ww' tt = idpath _. reflexivity. Defined.
Definition w_w := weqcoprodf w w.
Goal w_w (ii1 tt) = ii1 firstelement. reflexivity. Defined.
Goal invmap w_w (ii2 firstelement) = ii2 tt. reflexivity. Defined.
Goal homotweqinvweq w_w (ii2 firstelement) = idpath _. reflexivity. Defined.
Goal homotinvweqweq w_w (ii1 tt) = idpath _. reflexivity. Defined.
Definition i := ●1 : stn 4.
Definition j := ●0 : stn 4.
Lemma ne : ¬ (i = j).
Show proof.
Definition re' := weqrecompl_ne (stn 4) i (isisolatedinstn i) (stnneq i).
Definition c := complpair (stn 4) i j ne : compl _ i.
Definition c' := compl_ne_pair (stn 4) i (stnneq i) j tt : stn_compl i.
Goal re (ii2 tt) = i. reflexivity. Defined.
Goal re (ii1 c) = j. reflexivity. Defined.
Goal invmap re i = (ii2 tt). reflexivity. Defined.
Goal invmap re j = (ii1 c). reflexivity. Defined.
Goal homotweqinvweq re i = idpath _. reflexivity. Defined.
Goal homotweqinvweq re j = idpath _. reflexivity. Defined.
Goal homotinvweqweq re (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq re (ii1 c) = idpath _.
try reflexivity.
Abort.
Goal re' (ii2 tt) = i. reflexivity. Defined.
Goal re' (ii1 c') = j. reflexivity. Defined.
Goal invmap re' i = (ii2 tt). reflexivity. Defined.
Goal invmap re' j = (ii1 c'). reflexivity. Defined.
Goal homotweqinvweq re' i = idpath _. reflexivity. Defined.
Goal homotweqinvweq re' j = idpath _. reflexivity. Defined.
Goal homotinvweqweq re' (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq re' (ii1 c') = idpath _. reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii2 tt) = (●2). reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii1 (●2)) = (●3). reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii1 (●1)) = (●1). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●2) = (ii2 tt). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●3) = (ii1 (●2)). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●1) = (ii1 (●1)). reflexivity. Defined.
End Test2.
Goal ∏ (f : stn 3 -> nat), stnsum f = f(●0) + f(●1) + f(●2). reflexivity. Defined.
Goal ∏ (f : stn 3 -> nat), stnsum f = (f(●0) + f(●1)) + f(●2). reflexivity. Defined.
Module Test_weqstnsum.
Let X := stnset 7.
Let Y (x:X) := stnset (pr1 x).
Let W := ∑ x, Y x.
Let f : W ≃ stn _ := weqstnsum1 _.
Let f' : stn _ ≃ W := invweq f.
Goal f(●1,,●0) = ●0. reflexivity. Defined. Goal f(●2,,●0) = ●1. reflexivity. Defined.
Goal f(●2,,●1) = ●2. reflexivity. Defined.
Goal f(●3,,●0) = ●3. reflexivity. Defined.
Goal f(●3,,●1) = ●4. reflexivity. Defined.
Goal f(●3,,●2) = ●5. reflexivity. Defined.
Goal f(●4,,●0) = ●6. reflexivity. Defined.
Goal f(●5,,●0) = ●10. reflexivity. Defined.
Goal f(●6,,●0) = ●15. reflexivity. Defined.
Goal (pr2 (pr2 (f'(●0)))) = idpath true. reflexivity. Defined. Goal f'(●0) = (●1,,●0). reflexivity. Defined. Goal f'(●0) = (●1,,●0). reflexivity. Defined.
Goal f'(●1) = (●2,,●0). reflexivity. Defined.
Goal f'(●2) = (●2,,●1). reflexivity. Defined.
Goal f'(●3) = (●3,,●0). reflexivity. Defined.
Goal f'(●4) = (●3,,●1). reflexivity. Defined.
Goal f'(●5) = (●3,,●2). reflexivity. Defined.
Goal f'(●6) = (●4,,●0). reflexivity. Defined.
Goal f'(●10) = (●5,,●0). reflexivity. Defined.
Goal f'(●15) = (●6,,●0). reflexivity. Defined.
End Test_weqstnsum.
Module Test_weqfromprodofstn.
Let f : stn 5 × stn 4 ≃ stn 20 := weqfromprodofstn 5 4.
Goal f(●0,,●0) = ●0. reflexivity. Defined.
Goal f(●0,,●1) = ●1. reflexivity. Defined.
Goal f(●2,,●0) = ●8. reflexivity. Defined.
Goal f(●4,,●3) = ●19. reflexivity. Defined.
Let f' := invweq f.
Goal f'(●19) = (●4,,●3). reflexivity. Defined.
Goal f'(●18) = (●4,,●2). reflexivity. Defined.
Goal f'(●14) = (●3,,●2). reflexivity. Defined.
End Test_weqfromprodofstn.
Goal ∏ (f : stn 3 -> nat), stnprod f = f(●0) * f(●1) * f(●2).
Show proof.
Local Definition testfun : stn 3 -> stn 10.
Show proof.
Goal ∏ n, testfun n < 5.
Show proof.
End Test_stn.
Module Test_fin.
Import UniMath.Combinatorics.FiniteSets.
Require UniMath.Combinatorics.Lists.
Require UniMath.Combinatorics.StandardFiniteSets.
Require UniMath.Combinatorics.FiniteSets.
Require UniMath.Combinatorics.FiniteSequences.
Require UniMath.Combinatorics.FiniteSets.
Require UniMath.Combinatorics.OrderedSets.
Require UniMath.Combinatorics.StandardFiniteSets.
Require UniMath.Combinatorics.BoundedSearch.
Require UniMath.MoreFoundations.DecidablePropositions.
Require UniMath.MoreFoundations.NegativePropositions.
Module Test_list.
Import UniMath.Combinatorics.Lists.
Local Notation "[]" := nil (at level 0, format "[]").
Local Infix "::" := cons.
Goal concatenate (1::2::[]) (3::4::5::[]) = (1::2::3::4::5::[]).
reflexivity.
Defined.
Goal flatten ((1::2::[])::(3::4::5::[])::(6::[])::[]) = (1::2::3::4::5::6::[]).
reflexivity.
Defined.
End Test_list.
Module Test_stn.
Import UniMath.Combinatorics.StandardFiniteSets.
Import UniMath.MoreFoundations.NegativePropositions.
Local Open Scope stn.
Goal stn 6. exact (stnel(6,3)). Qed.
Goal stn 6. exact (stnpr 3). Qed.
Goal (stnel(6,3) ≠ stnel(6,4)). exact tt. Defined.
Goal ¬(stnel(6,3) ≠ stnel(6,3)). intro n. apply n. Defined.
Goal ∏ m n (i:m≤n) (j:stn m), pr1 (stnmtostnn m n i j) = pr1 j.
intros. induction j as [j J]. reflexivity.
Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●2)) = ●2. reflexivity. Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●3)) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (@dni 6 (●3) (●4)) = ●4. reflexivity. Defined.
Goal @sni 6 (●3) (●2) = ●2. reflexivity. Defined.
Goal @sni 6 (●3) (●3) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (●4) = ●3. reflexivity. Defined.
Goal @sni 6 (●3) (●5) = ●4. reflexivity. Defined.
Module Test_weqdnicompl.
Let n := 5.
Let X := stn n.
Let i := ●3 : stn (S n).
Let Y := @stn_compl (S n) i.
Let v := weqdnicompl i : X ≃ Y.
Let j := ●4 : X.
Let jni := ●5,,tt : Y.
Goal v j = jni. reflexivity. Defined.
Goal invmap v jni = j. reflexivity. Defined.
Goal homotweqinvweq v jni = idpath _. reflexivity. Defined.
Goal homotinvweqweq v j = idpath _.
reflexivity. Defined. Goal homotweqinvweqweq v j = idpath _. reflexivity. Defined.
End Test_weqdnicompl.
Module Test2.
Goal weqdnicoprod 4 firstelement (ii1 (●0)) = ●1. reflexivity. Defined.
Goal weqdnicoprod 4 firstelement (ii1 (●3)) = ●4. reflexivity. Defined.
Goal invmap (weqdnicoprod 4 firstelement) (●1) = (ii1 (●0)). reflexivity. Defined.
Goal invmap (weqdnicoprod 4 firstelement) (●4) = (ii1 (●3)). reflexivity. Defined.
Goal weqdnicoprod 4 lastelement (ii1 (●3)) = ●3. reflexivity. Defined.
Goal weqdnicoprod 4 lastelement (ii2 tt) = ●4. reflexivity. Defined.
Goal invmap (weqdnicoprod 4 lastelement) (●1) = (ii1 (●1)). reflexivity. Defined.
Goal invmap (weqdnicoprod 4 lastelement) (●4) = (ii2 tt). reflexivity. Defined.
Goal homotweqinvweq (weqdnicoprod 4 lastelement) (● 0) = idpath _. reflexivity. Defined. Goal homotinvweqweq (weqdnicoprod 4 (●4)) (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq (weqdnicoprod 4 (●4)) (ii1 (●1)) = idpath _.
reflexivity. Defined.
Local Definition w : unit ≃ stn 1.
simple refine (weq_iso _ _ _ _).
{ intro. exact firstelement. }
{ intro. exact tt. }
{ intro u. simpl. induction u. reflexivity. }
{ intro i. simpl. apply subtypeEquality_prop.
simpl. induction i as [i I]. simpl. apply pathsinv0. apply natlth1tois0. exact I. }
Defined.
Goal w tt = firstelement. reflexivity. Defined.
Goal invmap w firstelement = tt. reflexivity. Defined.
Goal homotweqinvweq w firstelement = idpath _. reflexivity. Defined.
Goal homotinvweqweq w tt = idpath _. reflexivity. Defined.
Local Definition w' := invweq w.
Goal w' firstelement = tt. reflexivity. Defined.
Goal invmap w' tt= firstelement. reflexivity. Defined.
Goal homotweqinvweq w' tt = idpath _. reflexivity. Defined.
Goal homotinvweqweq w' firstelement = idpath _. reflexivity. Defined.
Definition ww' := weqcomp w w'.
Goal ww' tt = tt. reflexivity. Defined.
Goal invmap ww' tt = tt. reflexivity. Defined.
Goal homotweqinvweq ww' tt = idpath _. reflexivity. Defined.
Goal homotinvweqweq ww' tt = idpath _. reflexivity. Defined.
Definition w_w := weqcoprodf w w.
Goal w_w (ii1 tt) = ii1 firstelement. reflexivity. Defined.
Goal invmap w_w (ii2 firstelement) = ii2 tt. reflexivity. Defined.
Goal homotweqinvweq w_w (ii2 firstelement) = idpath _. reflexivity. Defined.
Goal homotinvweqweq w_w (ii1 tt) = idpath _. reflexivity. Defined.
Definition i := ●1 : stn 4.
Definition j := ●0 : stn 4.
Lemma ne : ¬ (i = j).
Show proof.
apply stnneq_to_nopath. exact tt.
Definition re := weqrecompl (stn 4) i (isisolatedinstn _).Definition re' := weqrecompl_ne (stn 4) i (isisolatedinstn i) (stnneq i).
Definition c := complpair (stn 4) i j ne : compl _ i.
Definition c' := compl_ne_pair (stn 4) i (stnneq i) j tt : stn_compl i.
Goal re (ii2 tt) = i. reflexivity. Defined.
Goal re (ii1 c) = j. reflexivity. Defined.
Goal invmap re i = (ii2 tt). reflexivity. Defined.
Goal invmap re j = (ii1 c). reflexivity. Defined.
Goal homotweqinvweq re i = idpath _. reflexivity. Defined.
Goal homotweqinvweq re j = idpath _. reflexivity. Defined.
Goal homotinvweqweq re (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq re (ii1 c) = idpath _.
try reflexivity.
Abort.
Goal re' (ii2 tt) = i. reflexivity. Defined.
Goal re' (ii1 c') = j. reflexivity. Defined.
Goal invmap re' i = (ii2 tt). reflexivity. Defined.
Goal invmap re' j = (ii1 c'). reflexivity. Defined.
Goal homotweqinvweq re' i = idpath _. reflexivity. Defined.
Goal homotweqinvweq re' j = idpath _. reflexivity. Defined.
Goal homotinvweqweq re' (ii2 tt) = idpath _. reflexivity. Defined.
Goal homotinvweqweq re' (ii1 c') = idpath _. reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii2 tt) = (●2). reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii1 (●2)) = (●3). reflexivity. Defined.
Goal @weqdnicoprod_map 4 (●2) (ii1 (●1)) = (●1). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●2) = (ii2 tt). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●3) = (ii1 (●2)). reflexivity. Defined.
Goal @weqdnicoprod_invmap 4 (●2) (●1) = (ii1 (●1)). reflexivity. Defined.
End Test2.
Goal ∏ (f : stn 3 -> nat), stnsum f = f(●0) + f(●1) + f(●2). reflexivity. Defined.
Goal ∏ (f : stn 3 -> nat), stnsum f = (f(●0) + f(●1)) + f(●2). reflexivity. Defined.
Module Test_weqstnsum.
Let X := stnset 7.
Let Y (x:X) := stnset (pr1 x).
Let W := ∑ x, Y x.
Let f : W ≃ stn _ := weqstnsum1 _.
Let f' : stn _ ≃ W := invweq f.
Goal f(●1,,●0) = ●0. reflexivity. Defined. Goal f(●2,,●0) = ●1. reflexivity. Defined.
Goal f(●2,,●1) = ●2. reflexivity. Defined.
Goal f(●3,,●0) = ●3. reflexivity. Defined.
Goal f(●3,,●1) = ●4. reflexivity. Defined.
Goal f(●3,,●2) = ●5. reflexivity. Defined.
Goal f(●4,,●0) = ●6. reflexivity. Defined.
Goal f(●5,,●0) = ●10. reflexivity. Defined.
Goal f(●6,,●0) = ●15. reflexivity. Defined.
Goal (pr2 (pr2 (f'(●0)))) = idpath true. reflexivity. Defined. Goal f'(●0) = (●1,,●0). reflexivity. Defined. Goal f'(●0) = (●1,,●0). reflexivity. Defined.
Goal f'(●1) = (●2,,●0). reflexivity. Defined.
Goal f'(●2) = (●2,,●1). reflexivity. Defined.
Goal f'(●3) = (●3,,●0). reflexivity. Defined.
Goal f'(●4) = (●3,,●1). reflexivity. Defined.
Goal f'(●5) = (●3,,●2). reflexivity. Defined.
Goal f'(●6) = (●4,,●0). reflexivity. Defined.
Goal f'(●10) = (●5,,●0). reflexivity. Defined.
Goal f'(●15) = (●6,,●0). reflexivity. Defined.
End Test_weqstnsum.
Module Test_weqfromprodofstn.
Let f : stn 5 × stn 4 ≃ stn 20 := weqfromprodofstn 5 4.
Goal f(●0,,●0) = ●0. reflexivity. Defined.
Goal f(●0,,●1) = ●1. reflexivity. Defined.
Goal f(●2,,●0) = ●8. reflexivity. Defined.
Goal f(●4,,●3) = ●19. reflexivity. Defined.
Let f' := invweq f.
Goal f'(●19) = (●4,,●3). reflexivity. Defined.
Goal f'(●18) = (●4,,●2). reflexivity. Defined.
Goal f'(●14) = (●3,,●2). reflexivity. Defined.
End Test_weqfromprodofstn.
Goal ∏ (f : stn 3 -> nat), stnprod f = f(●0) * f(●1) * f(●2).
Show proof.
reflexivity.
Local Definition testfun : stn 3 -> stn 10.
Show proof.
intros n.
induction n as [n b].
induction n as [|n].
- exact (2,,idpath _).
- induction n as [|n].
+ exact (3,,idpath _).
+ induction n as [|n].
* exact (4,,idpath _).
* contradicts (negnatlthn0 n) b.
induction n as [n b].
induction n as [|n].
- exact (2,,idpath _).
- induction n as [|n].
+ exact (3,,idpath _).
+ induction n as [|n].
* exact (4,,idpath _).
* contradicts (negnatlthn0 n) b.
Goal ∏ n, testfun n < 5.
Show proof.
intros.
induction n as [i c].
inductive_reflexivity i c.
induction n as [i c].
inductive_reflexivity i c.
End Test_stn.
Module Test_fin.
Import UniMath.Combinatorics.FiniteSets.
Goal fincard (isfiniteempty) = 0. reflexivity. Qed.
Goal fincard (isfiniteunit) = 1. reflexivity. Qed.
Goal fincard (isfinitebool) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl true isfinitebool) = 1. reflexivity. Qed.
Goal fincard (isfinitedirprod isfinitebool isfinitebool) = 4. reflexivity. Qed.
Goal fincard (isfinitedirprod isfinitebool (isfinitedirprod isfinitebool isfinitebool)) = 8. reflexivity. Qed.
Goal cardinalityFiniteSet (isfinite_to_FiniteSet (isfinitedirprod isfinitebool (isfinitedirprod isfinitebool isfinitebool))) = 8. reflexivity. Qed.
Goal fincard (isfinitecompl (ii1 tt) (isfinitecoprod (isfiniteunit) (isfinitebool))) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl (ii1 tt) (isfinitecoprod (isfiniteunit) (isfinitebool))) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl (dirprodpair tt tt) (isfinitedirprod isfiniteunit isfiniteunit)) = 0. reflexivity. Qed.
Goal fincard (isfinitecompl (dirprodpair true (dirprodpair true false)) (isfinitedirprod (isfinitebool) (isfinitedirprod (isfinitebool) (isfinitebool)))) = 7. reflexivity. Qed.
Goal fincard (
isfiniteweq (isfinitedirprod isfinitebool isfinitebool)
) = 24. reflexivity. Qed.
Module Test_isfinite_isdeceq.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Let X := stnset 5.
Let finX : isfinite X := isfinitestn _.
Let eqX := isfinite_to_DecidableEquality finX.
Let x := ●3 : X.
Let x' := ●4 : X.
Let decide P := choice P true false.
Goal decide (eqX x x') = false. reflexivity. Defined.
Goal decide (eqX x x) = true. reflexivity. Defined.
Let eqbool := isfinite_to_DecidableEquality isfinitebool : DecidableRelation bool.
Goal decide (eqbool true true) = true. reflexivity. Defined.
Goal decide (eqbool false true) = false. reflexivity. Defined.
Let C := X ⨿ X.
Let eqQ : DecidableRelation C :=
isfinite_to_DecidableEquality (isfinitecoprod finX finX).
Let c := ii1 x : C.
Let c' := ii1 x' : C.
Let c'' := ii2 x : C.
Goal decide (eqQ c c') = false. reflexivity. Defined.
Goal decide (eqQ c c) = true. reflexivity. Defined.
Goal decide (eqQ c c'') = false. reflexivity. Defined.
Let Y := stnset 4.
Let y := ●1 : Y.
Let y' := ●2 : Y.
Let finY : isfinite Y := isfinitestn _.
Let V := X × Y.
Let eqV := isfinite_to_DecidableEquality (isfinitedirprod finX finY).
Goal decide (eqV (x,,y) (x',,y')) = false. reflexivity. Defined.
Let Y' (x:X) : hSet := Y.
Let W := ∑ x, Y' x.
Let eqW : DecidableRelation W :=
isfinite_to_DecidableEquality (isfinitetotal2 Y' finX (λ _, finY)).
Goal decide (eqW (x,,y) (x',,y')) = false.
reflexivity. Defined.
Let T := ∏ x, Y' x.
Let eqT : DecidableRelation T :=
isfinite_to_DecidableEquality (isfiniteforall Y' finX (λ _, finY)).
Goal decide (eqT (λ _, y) (λ _, y)) = true.
reflexivity. Defined.
End Test_isfinite_isdeceq.
End Test_fin.
Module Test_seq.
Import UniMath.Combinatorics.FiniteSequences.
Local Open Scope stn.
End Test_seq.
Module Test_finite_sets.
Import UniMath.Combinatorics.FiniteSets.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Goal 3 = fincard_standardSubset (λ i:stn 10, 2*i < 6)%dnat. Show proof.
Goal 6 = tallyStandardSubset (λ i:stn 10, 3 ≤ i ∧ i ≤ 8)%dnat%declog. Show proof.
Goal 6 = tallyStandardSubsetSegment (λ i:stn 14, 2*i ≠ 4)%dnat (●7). Show proof.
End Test_finite_sets.
Module Test_ord.
Import UniMath.Combinatorics.OrderedSets.
Import UniMath.Combinatorics.StandardFiniteSets.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Goal 3 = height ( ●3 : ⟦ 8 ⟧ %foset ). reflexivity. Defined.
Module TestLex.
Let X := stnset 5.
Let R := λ (x x':X), (pr1 x ≤ pr1 x')%dnat.
Let Y := λ x:X, stnset (pr1 x).
Let S := λ (x:X) (y y':Y x), (pr1 y ≤ pr1 y')%dnat.
Let Z := ∑ x, Y x.
Let T := lexicographicOrder X Y R S.
Let x2 := ●2 : X.
Let x3 := ●3 : X.
Goal (choice (R x2 x3) true false = true). reflexivity. Defined.
Goal (choice (R x2 x2) true false = true). reflexivity. Defined.
Goal (choice (R x3 x2) true false = false). reflexivity. Defined.
Let y1 := ●1 : Y x2.
Let y2 := ●2 : Y x3.
Let t := (x2,,y1) : Z.
Let t' := (x3,,y2) : Z.
End TestLex.
Module TestLex2.
Import UniMath.MoreFoundations.DecidablePropositions.
Open Scope foset.
Let i := ●2 : ⟦ 4 ⟧.
Let j := ●3 : ⟦ 4 ⟧.
Goal choice (i < j)%foset true false = true. reflexivity. Defined.
Goal choice (i ≤ j)%foset true false = true. reflexivity. Defined.
Goal choice (i ≐ j)%foset true false = false. reflexivity. Defined.
Let X := (∑ i:⟦ 4 ⟧, ⟦ pr1 i ⟧)%foset.
Let x := ( ●2 ,, ●1 ):X.
Let y := ( ●3 ,, ●1 ):X.
Lemma d : isdeceq X.
Show proof.
Definition which {X} : X ⨿ ¬X -> bool.
Show proof.
Goal choice (x < y) true false = true.
reflexivity. Defined.
Goal choice (x ≤ y)%foset true false = true.
reflexivity.
Defined.
Goal choice (y < x)%foset true false = false.
reflexivity.
Defined.
Goal choice (y ≤ x)%foset true false = false.
reflexivity.
Defined.
Goal choice (x ≐ y)%foset true false = false.
reflexivity.
Defined.
Goal choice (x ≐ x)%foset true false = true.
reflexivity.
Defined.
Goal which (d x y) = false.
reflexivity.
Defined.
Goal which (d x x) = true.
reflexivity.
Defined.
Goal choice (x ≠ y)%foset true false = true.
reflexivity.
Defined.
Goal which (isdeceqnat 2 (height x)) = true.
try reflexivity. Abort.
Goal 2 = height x.
try reflexivity. Abort.
End TestLex2.
Goal ∏ X (lt:hrel X), iscotrans lt <-> iswklin lt.
Show proof.
Goal (idweq nat ∘ idweq _ ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal (idweq nat ∘ invweq (idweq _) ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal invmap (idweq nat ∘ idweq _ ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal invmap (idweq nat ∘ invweq (idweq _) ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
End Test_ord.
Module Test_search.
Import UniMath.Combinatorics.BoundedSearch.
Import UniMath.Foundations.Propositions.
Local Definition someseq (n : nat) : bool.
Show proof.
Definition P : nat → hProp.
Show proof.
Local Definition P_dec (n : nat) : P n ⨿ ¬ P n.
Show proof.
Local Definition P_inhab : ∃ n, P n.
Show proof.
Goal 1 = pr1 (minimal_n P P_dec P_inhab). reflexivity. Defined.
Variable P_inhab' : ∃ n, P n.
Definition new_n' : ∑ n : nat, P n := minimal_n P P_dec P_inhab'.
End Test_search.
Goal fincard (isfiniteunit) = 1. reflexivity. Qed.
Goal fincard (isfinitebool) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl true isfinitebool) = 1. reflexivity. Qed.
Goal fincard (isfinitedirprod isfinitebool isfinitebool) = 4. reflexivity. Qed.
Goal fincard (isfinitedirprod isfinitebool (isfinitedirprod isfinitebool isfinitebool)) = 8. reflexivity. Qed.
Goal cardinalityFiniteSet (isfinite_to_FiniteSet (isfinitedirprod isfinitebool (isfinitedirprod isfinitebool isfinitebool))) = 8. reflexivity. Qed.
Goal fincard (isfinitecompl (ii1 tt) (isfinitecoprod (isfiniteunit) (isfinitebool))) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl (ii1 tt) (isfinitecoprod (isfiniteunit) (isfinitebool))) = 2. reflexivity. Qed.
Goal fincard (isfinitecompl (dirprodpair tt tt) (isfinitedirprod isfiniteunit isfiniteunit)) = 0. reflexivity. Qed.
Goal fincard (isfinitecompl (dirprodpair true (dirprodpair true false)) (isfinitedirprod (isfinitebool) (isfinitedirprod (isfinitebool) (isfinitebool)))) = 7. reflexivity. Qed.
Goal fincard (
isfiniteweq (isfinitedirprod isfinitebool isfinitebool)
) = 24. reflexivity. Qed.
Module Test_isfinite_isdeceq.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Let X := stnset 5.
Let finX : isfinite X := isfinitestn _.
Let eqX := isfinite_to_DecidableEquality finX.
Let x := ●3 : X.
Let x' := ●4 : X.
Let decide P := choice P true false.
Goal decide (eqX x x') = false. reflexivity. Defined.
Goal decide (eqX x x) = true. reflexivity. Defined.
Let eqbool := isfinite_to_DecidableEquality isfinitebool : DecidableRelation bool.
Goal decide (eqbool true true) = true. reflexivity. Defined.
Goal decide (eqbool false true) = false. reflexivity. Defined.
Let C := X ⨿ X.
Let eqQ : DecidableRelation C :=
isfinite_to_DecidableEquality (isfinitecoprod finX finX).
Let c := ii1 x : C.
Let c' := ii1 x' : C.
Let c'' := ii2 x : C.
Goal decide (eqQ c c') = false. reflexivity. Defined.
Goal decide (eqQ c c) = true. reflexivity. Defined.
Goal decide (eqQ c c'') = false. reflexivity. Defined.
Let Y := stnset 4.
Let y := ●1 : Y.
Let y' := ●2 : Y.
Let finY : isfinite Y := isfinitestn _.
Let V := X × Y.
Let eqV := isfinite_to_DecidableEquality (isfinitedirprod finX finY).
Goal decide (eqV (x,,y) (x',,y')) = false. reflexivity. Defined.
Let Y' (x:X) : hSet := Y.
Let W := ∑ x, Y' x.
Let eqW : DecidableRelation W :=
isfinite_to_DecidableEquality (isfinitetotal2 Y' finX (λ _, finY)).
Goal decide (eqW (x,,y) (x',,y')) = false.
reflexivity. Defined.
Let T := ∏ x, Y' x.
Let eqT : DecidableRelation T :=
isfinite_to_DecidableEquality (isfiniteforall Y' finX (λ _, finY)).
Goal decide (eqT (λ _, y) (λ _, y)) = true.
reflexivity. Defined.
End Test_isfinite_isdeceq.
End Test_fin.
Module Test_seq.
Import UniMath.Combinatorics.FiniteSequences.
Local Open Scope stn.
End Test_seq.
Module Test_finite_sets.
Import UniMath.Combinatorics.FiniteSets.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Goal 3 = fincard_standardSubset (λ i:stn 10, 2*i < 6)%dnat. Show proof.
reflexivity.
Goal 6 = tallyStandardSubset (λ i:stn 10, 3 ≤ i ∧ i ≤ 8)%dnat%declog. Show proof.
reflexivity.
Goal 6 = tallyStandardSubsetSegment (λ i:stn 14, 2*i ≠ 4)%dnat (●7). Show proof.
reflexivity.
End Test_finite_sets.
Module Test_ord.
Import UniMath.Combinatorics.OrderedSets.
Import UniMath.Combinatorics.StandardFiniteSets.
Import UniMath.MoreFoundations.DecidablePropositions.
Local Open Scope stn.
Goal 3 = height ( ●3 : ⟦ 8 ⟧ %foset ). reflexivity. Defined.
Module TestLex.
Let X := stnset 5.
Let R := λ (x x':X), (pr1 x ≤ pr1 x')%dnat.
Let Y := λ x:X, stnset (pr1 x).
Let S := λ (x:X) (y y':Y x), (pr1 y ≤ pr1 y')%dnat.
Let Z := ∑ x, Y x.
Let T := lexicographicOrder X Y R S.
Let x2 := ●2 : X.
Let x3 := ●3 : X.
Goal (choice (R x2 x3) true false = true). reflexivity. Defined.
Goal (choice (R x2 x2) true false = true). reflexivity. Defined.
Goal (choice (R x3 x2) true false = false). reflexivity. Defined.
Let y1 := ●1 : Y x2.
Let y2 := ●2 : Y x3.
Let t := (x2,,y1) : Z.
Let t' := (x3,,y2) : Z.
End TestLex.
Module TestLex2.
Import UniMath.MoreFoundations.DecidablePropositions.
Open Scope foset.
Let i := ●2 : ⟦ 4 ⟧.
Let j := ●3 : ⟦ 4 ⟧.
Goal choice (i < j)%foset true false = true. reflexivity. Defined.
Goal choice (i ≤ j)%foset true false = true. reflexivity. Defined.
Goal choice (i ≐ j)%foset true false = false. reflexivity. Defined.
Let X := (∑ i:⟦ 4 ⟧, ⟦ pr1 i ⟧)%foset.
Let x := ( ●2 ,, ●1 ):X.
Let y := ( ●3 ,, ●1 ):X.
Lemma d : isdeceq X.
Show proof.
apply isdeceq_total2.
- apply isdeceqstn.
- intro i. apply isdeceqstn.
- apply isdeceqstn.
- intro i. apply isdeceqstn.
Definition which {X} : X ⨿ ¬X -> bool.
Show proof.
intros c.
induction c.
- exact true.
- exact false.
induction c.
- exact true.
- exact false.
Goal choice (x < y) true false = true.
reflexivity. Defined.
Goal choice (x ≤ y)%foset true false = true.
reflexivity.
Defined.
Goal choice (y < x)%foset true false = false.
reflexivity.
Defined.
Goal choice (y ≤ x)%foset true false = false.
reflexivity.
Defined.
Goal choice (x ≐ y)%foset true false = false.
reflexivity.
Defined.
Goal choice (x ≐ x)%foset true false = true.
reflexivity.
Defined.
Goal which (d x y) = false.
reflexivity.
Defined.
Goal which (d x x) = true.
reflexivity.
Defined.
Goal choice (x ≠ y)%foset true false = true.
reflexivity.
Defined.
Goal which (isdeceqnat 2 (height x)) = true.
try reflexivity. Abort.
Goal 2 = height x.
try reflexivity. Abort.
End TestLex2.
Goal ∏ X (lt:hrel X), iscotrans lt <-> iswklin lt.
Show proof.
intros. unfold iscotrans, iswklin. split.
{ intros i x1 x3 x2. apply i. }
{ intros i x z y. apply i. }
{ intros i x1 x3 x2. apply i. }
{ intros i x z y. apply i. }
Goal (idweq nat ∘ idweq _ ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal (idweq nat ∘ invweq (idweq _) ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal invmap (idweq nat ∘ idweq _ ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
Goal invmap (idweq nat ∘ invweq (idweq _) ∘ idweq _)%weq 3 = 3. reflexivity. Defined.
End Test_ord.
Module Test_search.
Import UniMath.Combinatorics.BoundedSearch.
Import UniMath.Foundations.Propositions.
Local Definition someseq (n : nat) : bool.
Show proof.
destruct n.
- exact false.
- destruct n.
+ exact true.
+ destruct n.
* exact true.
* exact false.
- exact false.
- destruct n.
+ exact true.
+ destruct n.
* exact true.
* exact false.
Definition P : nat → hProp.
Show proof.
intros n.
refine (hProppair (someseq n = true) _).
refine (isasetbool _ _).
refine (hProppair (someseq n = true) _).
refine (isasetbool _ _).
Local Definition P_dec (n : nat) : P n ⨿ ¬ P n.
Show proof.
unfold P, someseq.
destruct n.
- apply ii2. exact nopathsfalsetotrue.
- destruct n.
+ apply ii1. apply idpath.
+ destruct n.
* apply ii1, idpath.
* apply ii2. exact nopathsfalsetotrue.
destruct n.
- apply ii2. exact nopathsfalsetotrue.
- destruct n.
+ apply ii1. apply idpath.
+ destruct n.
* apply ii1, idpath.
* apply ii2. exact nopathsfalsetotrue.
Local Definition P_inhab : ∃ n, P n.
Show proof.
apply hinhpr. refine (2%nat,,_). apply idpath.
Goal 1 = pr1 (minimal_n P P_dec P_inhab). reflexivity. Defined.
Variable P_inhab' : ∃ n, P n.
Definition new_n' : ∑ n : nat, P n := minimal_n P P_dec P_inhab'.
End Test_search.