Zorn etc. (Co-Authored by Georges Gonthier <[email protected]>)

_CoqProject

@@ -11,6 +11,7 @@
 classical/all_classical.v
 classical/boolp.v
 classical/contra.v
+classical/wochoice.v
 classical/classical_sets.v
 classical/mathcomp_extra.v
 classical/functions.v

classical/Make

@@ -9,6 +9,7 @@
 
 boolp.v
 contra.v
+wochoice.v
 classical_sets.v
 mathcomp_extra.v
 functions.v

classical/contra.v

@@ -61,6 +61,30 @@ Variant move_view S T := MoveView of S -> T.
 Definition move_viewP {S T} mv : S -> T := let: MoveView v := mv in v.
 Hint View for move/ move_viewP|2.
 
+(******************************************************************************)
+(* Type-level equivalence                                                     *)
+(******************************************************************************)
+
+Variant equivT S T := EquivT of S -> T & T -> S.
+Notation "S <--> T" := (equivT S T) (at level 95, no associativity).
+
+Definition equivT_refl S : S <--> S := EquivT id id.
+Definition equivT_transl {S T U} : S <--> T -> S <--> U -> T <--> U :=
+  fun '(EquivT S_T T_S) '(EquivT S_U U_S) => EquivT (S_U \o T_S) (S_T \o U_S).
+Definition equivT_sym {S T} : S <--> T -> T <--> S :=
+   equivT_transl^~ (equivT_refl S).
+Definition equivT_trans {S T U} : S <--> T -> T <--> U -> S <--> U :=
+   equivT_transl \o equivT_sym.
+Definition equivT_transr {S T U} eqST : U <--> S -> U <--> T :=
+   equivT_trans^~ eqST.
+Definition equivT_Prop (P Q : Prop) : (P <--> Q) <-> (P <-> Q).
+Proof. split; destruct 1; split; assumption. Defined.
+Definition equivT_LR {S T} '(EquivT S_T _) : S -> T := S_T.
+Definition equivT_RL {S T} '(EquivT _ T_S) : T -> S := T_S.
+
+Hint View for move/ equivT_LR|2 equivT_RL|2.
+Hint View for apply/ equivT_RL|2 equivT_LR|2.
+
 (******************************************************************************)
 (*   A generic Forall "constructor" for the Gallina forall quantifier, i.e.,  *)
 (*   \Forall x, P := Forall (fun x => P) := forall x, P.                      *)
@@ -746,8 +770,81 @@ Proof. by rewrite 2!lax_notE. Qed.
 
 End Internals.
 Import Internals.
+Definition notP := @Internals.notP.
 Hint View for move/ move_viewP|2.
+Hint View for move/ Internals.equivT_LR|2 Internals.equivT_RL|2.
+Hint View for apply/ Internals.equivT_RL|2 Internals.equivT_LR|2.
 Export (canonicals) Internals.
+Canonical TypeForall.
+Canonical PropForall.
+Canonical SetForall.
+Canonical wrap1Prop.
+Canonical wrap1Type.
+Canonical proper_nProp.
+Canonical trivial_nProp.
+Canonical True_nProp.
+Canonical False_nProp.
+Canonical not_nProp.
+Canonical and_nProp.
+Canonical and3_nProp.
+Canonical and4_nProp.
+Canonical and5_nProp.
+Canonical or_nProp.
+Canonical or3_nProp.
+Canonical or4_nProp.
+Canonical unary_and_rhs.
+Canonical binary_and_rhs.
+Canonical imply_nProp.
+Canonical exists_nProp.
+Canonical exists2_nProp.
+Canonical inhabited_nProp.
+Canonical forall_nProp.
+Canonical proper_nBody.
+Canonical nonproper_nBody.
+Canonical bounded_nBody.
+Canonical unbounded_nBody.
+Canonical is_true_nProp.
+Canonical true_neg.
+Canonical true_pos.
+Canonical false_neg.
+Canonical false_pos.
+Canonical id_neg.
+Canonical id_pos.
+Canonical negb_neg.
+Canonical negb_pos.
+Canonical neg_ltn_LHS.
+Canonical neg_leq_LHS.
+Canonical leq_neg.
+Canonical eq_nProp.
+Canonical bool_neq.
+Canonical true_neq.
+Canonical false_neq.
+Canonical eqType_neq.
+Canonical eq_op_pos.
+Canonical Prop_wType.
+Canonical proper_wType.
+Canonical forall_wType.
+Canonical inhabited_wType.
+Canonical void_wType.
+Canonical unit_wType.
+Canonical pair_wType.
+Canonical sum_wType.
+Canonical sumbool_wType.
+Canonical sumor_wType.
+Canonical sig1_wType.
+Canonical sig2_wType.
+Canonical sigT_wType.
+Canonical sigT2_wType.
+Canonical proper_wProp.
+Canonical forall_wProp.
+Canonical trivial_wProp.
+Canonical inhabited_wProp.
+Canonical nand_false_bool.
+Canonical nand_true_bool.
+Canonical and_wProp.
+Canonical or_wProp.
+Canonical exists_wProp.
+Canonical exists2_wProp.
 
 (******************************************************************************)
 (* Lemma and tactic assume_not: add a goal negation assumption. The tactic    *)