Ultra simplify filter

shell.nix

@@ -1,9 +1,9 @@
 {withEmacs ? false,
- nixpkgs ? (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/c4196cca9acd1c51f62baf10fcbe34373e330bb3.tar.gz";
-  sha256 = "0jsisiw8yckq96r5rgdmkrl3a7y9vg9ivpw12h11m8w6rxsfn5m5";
+ nixpkgs ?  (fetchTarball {
+  url = "https://github.com/NixOS/nixpkgs/archive/82b54d490663b6d87b7b34b9cfc0985df8b49c7d.tar.gz";
+  sha256 = "12gpsif48g5b4ys45x36g4vdf0srgal4c96351m7gd2jsgvdllyf";
 }),
-coq-version ? "default",
+coq-version ? "8.10",
 print-env ? false
 }:
 with import nixpkgs {};
@@ -16,15 +16,16 @@ let
     "8.8" = coqPackages_8_8;
     "8.9" = coqPackages_8_9;
     "8.10" = coqPackages_8_10;
+    "8.11" = coqPackages_8_11;
     }."${coq-version}";
   coq = myCoqPackages.coq;
 in
 stdenv.mkDerivation rec {
   name = "env";
   env = buildEnv { name = name; paths = buildInputs; };
   buildInputs = [ coq ] ++ (with myCoqPackages;
-    [mathcomp mathcomp-finmap mathcomp-bigenough
-     mathcomp-multinomials mathcomp-real-closed coqeal])
+    [ mathcomp mathcomp-finmap mathcomp-bigenough
+      mathcomp-multinomials mathcomp-real-closed ])
                 ++ lib.optional withEmacs pgEmacs;
   shellHook = ''
     nixEnv (){

theories/boolp.v

@@ -55,7 +55,6 @@ Proof. by case: extentionality=> _; apply. Qed.
 Lemma propeqE (P Q : Prop) : (P = Q) = (P <-> Q).
 Proof. by apply: propext; split=> [->|/propext]. Qed.
 
-
 Lemma funeqE {T U : Type} (f g : T -> U) : (f = g) = (f =1 g).
 Proof. by rewrite propeqE; split=> [->//|/funext]. Qed.
 
@@ -87,6 +86,9 @@ Proof.
 by rewrite propeqE; split=> [->//|?]; rewrite funeq3E=> ???; rewrite propeqE.
 Qed.
 
+Lemma predext {T} (P Q : T -> Prop) : (forall x, P x <-> Q x) -> P = Q.
+Proof. by rewrite predeqE. Qed.
+
 Lemma propT (P : Prop) : P -> P = True.
 Proof. by move=> p; rewrite propeqE; tauto. Qed.
 
@@ -276,7 +278,7 @@ move=> cb /asboolPn nb; apply/asboolPn.
 by apply: contra nb => /asboolP /cb /asboolP.
 Qed.
 
-Definition contrapNN := contra.
+Definition contrapNN := contrap.
 
 Lemma contrapL (Q P : Prop) : (Q -> ~ P) -> P -> ~ Q.
 Proof.

theories/classical_sets.v

@@ -96,6 +96,10 @@ Reserved Notation "[ 'set' x : T | P ]"
   (at level 0, x at level 99, only parsing).
 Reserved Notation "[ 'set' x | P ]"
   (at level 0, x, P at level 99, format "[ 'set'  x  |  P ]").
+Reserved Notation "[ 'get' x : T | P ]"
+  (at level 0, x at level 99, only parsing).
+Reserved Notation "[ 'get' x | P ]"
+  (at level 0, x, P at level 99, format "[ 'get'  x  |  P ]").
 Reserved Notation "[ 'set' E | x 'in' A ]" (at level 0, E, x at level 99,
   format "[ '[hv' 'set'  E '/ '  |  x  'in'  A ] ']'").
 Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]"
@@ -315,11 +319,16 @@ Qed.
 
 Lemma subsetI A (X Y Z : set A) : (X `<=` Y `&` Z) = ((X `<=` Y) /\ (X `<=` Z)).
 Proof.
-rewrite propeqE; split=> [H|[y z ??]]; split; by [move=> ?/H[]|apply y|apply z].
+rewrite propeqE; split=> [XYZ|[XY XZ] x Xx]; first by split=> x /XYZ[].
+by split; [apply: XY|apply: XZ].
 Qed.
 
 Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z.
-Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed.
+Proof. by move=> [XZ x [/XZ]|YZ x [_ /YZ]]. Qed.
+
+Lemma subsetI2 (A : Type) (X Y X' Y' : set A) :
+  X `<=` X'  -> Y `<=` Y' -> X `&` Y `<=` X' `&` Y'.
+Proof. by move=> sX sY x [/sX ? /sY]. Qed.
 
 Lemma setD_eq0 A (X Y : set A) : (X `\` Y = set0) = (X `<=` Y).
 Proof.
@@ -447,18 +456,18 @@ Record class_of (T : Type) := Class {
 
 Section ClassDef.
 
-Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
+Structure type := Pack { sort; _ : class_of sort }.
 Local Coercion sort : type >-> Sortclass.
 Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c _ := cT return class_of cT in c.
+Definition class := let: Pack _ c := cT return class_of cT in c.
 
-Definition clone c of phant_id class c := @Pack T c T.
-Let xT := let: Pack T _ _ := cT in T.
+Definition clone c of phant_id class c := @Pack T c.
+Let xT := let: Pack T _ := cT in T.
 Notation xclass := (class : class_of xT).
 Local Coercion base : class_of >-> Choice.class_of.
 
 Definition pack m :=
-  fun bT b of phant_id (Choice.class bT) b => @Pack T (Class b m) T.
+  fun bT b of phant_id (Choice.class bT) b => @Pack T (Class b m).
 
 Definition eqType := @Equality.Pack cT xclass.
 Definition choiceType := @Choice.Pack cT xclass.
@@ -500,6 +509,8 @@ Canonical matrix_pointedType m n (T : pointedType) :=
   PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
 
 Notation get := (xget point).
+Notation "[ 'get' x : T | P ]" := (get [set x : T | P]) : classical_set_scope.
+Notation "[ 'get' x | P ]" := [get x : _ | P] : classical_est_scope.
 
 Section PointedTheory.
 
@@ -539,7 +550,7 @@ Hypothesis (Rsucc : forall s, exists t, R s t /\ s <> t /\
 
 Let Teq := @gen_eqMixin T.
 Let Tch := @gen_choiceMixin T.
-Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0) T.
+Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
 Let lub := fun A : {A : set T | total_on A R} =>
   get (fun t : Tp => (forall s, sval A s -> R s t) /\
     forall r, (forall s, sval A s -> R s r) -> R t r).
@@ -656,7 +667,7 @@ Lemma ZL_preorder T (t0 : T) (R : T -> T -> Prop) :
   exists t, premaximal R t.
 Proof.
 set Teq := @gen_eqMixin T; set Tch := @gen_choiceMixin T.
-set Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0) T.
+set Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
 move=> Rrefl Rtrans tot_max.
 set eqR := fun s t => R s t /\ R t s; set ceqR := fun s => [set t | eqR s t].
 have eqR_trans r s t : eqR r s -> eqR s t -> eqR r t.