Wochoice

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,14 @@
 - in `lebesgue_integral.v`
   + lemma `ge0_integralZr`
 
+- in `contra.v`:
+  + in module `Internals`
+    * variant `equivT`, notation `<--->`
+    * definitions `equivT_refl`, `equivT_transl`, `equivT_sym`, `equivT_trans`,
+      `equivT_transr`, `equivT_Prop`, `equivT_LR` (hint view), `equivT_RL` (hint view)
+  + definition `notP`
+  + hint view for `move/` and `apply/` for `Internals.equivT_LR`, `Internals.equivT_RL`
+
 ### Changed
 
 - move from `kernel.v` to `measure.v`

_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

@@ -6,12 +6,13 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-(******************************************************************************)
-(*                              Contraposition                                *)
+(**md**************************************************************************)
+(* # Contraposition                                                           *)
 (*                                                                            *)
 (* This file provides tactics to reason by contraposition and contradiction.  *)
 (*                                                                            *)
-(* * Tactics                                                                  *)
+(* ## Tactics                                                                 *)
+(* ```                                                                        *)
 (* assume_not == add a goal negation assumption. The tactic also works for    *)
 (*               goals in Type, simplifies the added assumption, and          *)
 (*               exposes its top-level constructive content.                  *)
@@ -39,6 +40,7 @@ Unset Printing Implicit Defensive.
 (*               negation of the (single) <d-item> (as with contra:, a clear  *)
 (*               switch is also allowed.                                      *)
 (*               Finally the Ltac absurd term form is also supported.         *)
+(* ```                                                                        *)
 (******************************************************************************)
 
 (* Hiding module for the internal definitions and lemmas used by the tactics
@@ -61,6 +63,34 @@ 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.
+
+Definition equivT_refl S : equivT S S := EquivT id id.
+Definition equivT_transl {S T U} : equivT S T -> equivT S U -> equivT T U :=
+  fun (st : equivT S T) (su : equivT S U) =>
+    let: EquivT S_T T_S := st in
+    let: EquivT S_U U_S := su in
+    EquivT (S_U \o T_S) (S_T \o U_S).
+Definition equivT_sym {S T} : equivT S T -> equivT T S :=
+   equivT_transl^~ (equivT_refl S).
+Definition equivT_trans {S T U} : equivT S T -> equivT T U -> equivT S U :=
+   equivT_transl \o equivT_sym.
+Definition equivT_transr {S T U} eqST : equivT U S -> equivT U T :=
+   equivT_trans^~ eqST.
+Definition equivT_Prop (P Q : Prop) : (equivT P Q) <-> (equivT P Q).
+Proof. split; destruct 1; split; assumption. Defined.
+Definition equivT_LR {S T} (eq : equivT S T) : S -> T :=
+  let: EquivT S_T _ := eq in S_T.
+Definition equivT_RL {S T} (eq : equivT S T) : T -> S :=
+  let: EquivT _ T_S := eq in 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.                      *)
@@ -744,8 +774,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    *)