[coq] make an attempt to refine mathcomp set

coq/mathcomp/set-refine-attempt.v

@@ -0,0 +1,51 @@
+From mathcomp Require Import all_ssreflect.
+
+Example p1: {set bool*bool} := [set (false, false); (true, false)].
+Example s1: {set bool} := [set false].
+
+Definition s2p (s: {set bool}): bool*bool :=
+  if s == set0 then (false, false)
+  else if s == [set false] then (true, false)
+  else if s == [set true] then (false, true)
+  else (true, true).
+
+Example eg1 := Eval compute in s2p s1.
+Print eg1.
+
+(* Lesson learnt: This is not refining. *)
+
+(*
+eg1 =
+if
+ (fix eqseq (s1 s2 : seq {_ : bool & bool}) {struct s2} : bool :=
+    match s1 with
+    | [::] => match s2 with
+
+   ....
+   ....
+   ....
+   ....
+
+                      |};
+                    Finite.eqtype_hasDecEq_mixin :=
+                      {|
+                        hasDecEq.eq_op :=
+                          fun b : bool =>
+                          if if b then false else true
+                          then fun b0 : bool => if b0 then false else true
+                          else id;
+                        hasDecEq.eqP := eqbP
+                      |};
+                    Finite.fintype_isFinite_mixin :=
+                      {|
+                        isFinite.enum_subdef := [:: true; false];
+                        isFinite.enumP_subdef := bool_enumP
+                      |}
+                  |}
+              |})))
+  then (false, true)
+  else (true, true)
+     : bool * bool
+*)
+
+