Skip to content

Commit

Permalink
test a few files
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Dec 8, 2023
1 parent 9119ba1 commit 2fc1a66
Show file tree
Hide file tree
Showing 37 changed files with 701 additions and 474 deletions.
26 changes: 16 additions & 10 deletions classical/boolp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,18 @@

From mathcomp Require Import all_ssreflect.

(******************************************************************************)
(* Classical Logic *)
(***markdown*******************************************************************)
(* # Classical Logic *)
(* *)
(* This file provides the axioms of classical logic and tools to perform *)
(* classical reasoning in the Mathematical Compnent framework. The three *)
(* axioms are taken from the standard library of Coq, more details can be *)
(* found in Section 5 of *)
(* Reynald Affeldt, Cyril Cohen, Damien Rouhling: *)
(* Formalization Techniques for Asymptotic Reasoning in Classical Analysis. *)
(* Journal of Formalized Reasoning, 2018 *)
(* - R. Affeldt, C. Cohen, D. Rouhling. Formalization Techniques for *)
(* Asymptotic Reasoning in Classical Analysis. JFR 2018 *)
(* *)
(* * Axioms *)
(* ## Axioms *)
(* ``` *)
(* functional_extensionality_dep == functional extensionality (on dependently *)
(* typed functions), i.e., functions that are pointwise *)
(* equal are equal *)
Expand All @@ -27,14 +27,19 @@ From mathcomp Require Import all_ssreflect.
(* constructive_indefinite_description == existential in Prop (ex) implies *)
(* existential in Type (sig) *)
(* cid := constructive_indefinite_description (shortcut) *)
(* --> A number of properties are derived below from these axioms and are *)
(* ``` *)
(* *)
(* A number of properties are derived below from these axioms and are *)
(* often more pratical to use than directly using the axioms. For instance *)
(* propext, funext, the excluded middle (EM),... *)
(* *)
(* * Boolean View of Prop *)
(* ## Boolean View of Prop *)
(* ``` *)
(* `[< P >] == boolean view of P : Prop, see all lemmas about asbool *)
(* ``` *)
(* *)
(* * Mathematical Components Structures *)
(* ## Mathematical Components Structures *)
(* ``` *)
(* {classic T} == Endow T : Type with a canonical eqType/choiceType. *)
(* This is intended for local use. *)
(* E.g., T : Type |- A : {fset {classic T}} *)
Expand All @@ -43,8 +48,9 @@ From mathcomp Require Import all_ssreflect.
(* {eclassic T} == Endow T : eqType with a canonical choiceType. *)
(* On the model of {classic _}. *)
(* See also the lemmas Peq and eqPchoice. *)
(* ``` *)
(* *)
(* --> Functions into a porderType (resp. latticeType) are equipped with *)
(* Functions into a porderType (resp. latticeType) are equipped with *)
(* a porderType (resp. latticeType), (f <= g)%O when f x <= g x for all x, *)
(* see lemma lefP. *)
(******************************************************************************)
Expand Down
6 changes: 4 additions & 2 deletions classical/cardinality.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ From HB Require Import structures.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.

(******************************************************************************)
(* Cardinality *)
(***markdown*******************************************************************)
(* # Cardinality *)
(* *)
(* This file provides an account of cardinality properties of classical sets. *)
(* This includes standard results of set theory such as the Pigeon Hole *)
Expand All @@ -16,6 +16,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
(* only relations A #<= B and A #= B to compare the cardinals of two sets *)
(* (on two possibly different types). *)
(* *)
(* ``` *)
(* A #<= B == the cardinal of A is smaller or equal to the one of B *)
(* A #>= B := B #<= A *)
(* A #= B == the cardinal of A is equal to the cardinal of B *)
Expand All @@ -32,6 +33,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
(* A.`1 := [fset x.1 | x in A] *)
(* A.`2 := [fset x.2 | x in A] *)
(* {fimfun aT >-> T} == type of functions with a finite image *)
(* ``` *)
(* *)
(******************************************************************************)

Expand Down
105 changes: 73 additions & 32 deletions classical/classical_sets.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,19 +3,62 @@ From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
From mathcomp Require Import ssrint interval.
From mathcomp Require Import mathcomp_extra boolp.

(******************************************************************************)
(***markdown*******************************************************************)
(* # Set Theory *)
(* *)
(* This file develops a basic theory of sets and types equipped with a *)
(* canonical inhabitant (pointed types). *)
(* canonical inhabitant (pointed types): *)
(* - A decidable equality is defined for any type. It is thus possible to *)
(* define an eqType structure for any type using the mixin gen_eqMixin. *)
(* - This file adds the possibility to define a choiceType structure for *)
(* any type thanks to an axiom gen_choiceMixin giving a choice mixin. *)
(* - We chose to have generic mixins and no global instances of the eqType *)
(* and choiceType structures to let the user choose which definition of *)
(* equality to use and to avoid conflict with already declared instances. *)
(* *)
(* Thanks to this basic set theory, we proved Zorn's Lemma, which states *)
(* that any ordered set such that every totally ordered subset admits an *)
(* upper bound has a maximal element. We also proved an analogous version *)
(* for preorders, where maximal is replaced with premaximal: $t$ is *)
(* premaximal if whenever $t < s$ we also have $s < t$. *)
(* *)
(* About the naming conventions in this file: *)
(* - use T, T', T1, T2, etc., aT (domain type), rT (return type) for names *)
(* of variables in Type (or choiceType/pointedType/porderType) *)
(* + use the same suffix or prefix for the sets as their containing type *)
(* (e.g., A1 in T1, etc.) *)
(* + as a consequence functions are rather of type aT -> rT *)
(* - use I, J when the type corresponds to an index *)
(* - sets are named A, B, C, D, etc., or Y when it is ostensibly an image *)
(* set (i.e., of type set rT) *)
(* - indexed sets are rather named F *)
(* *)
(* --> A decidable equality is defined for any type. It is thus possible to *)
(* define an eqType structure for any type using the mixin gen_eqMixin. *)
(* --> This file adds the possibility to define a choiceType structure for *)
(* any type thanks to an axiom gen_choiceMixin giving a choice mixin. *)
(* --> We chose to have generic mixins and no global instances of the eqType *)
(* and choiceType structures to let the user choose which definition of *)
(* equality to use and to avoid conflict with already declared instances. *)
(* Sample notations: *)
(* | Coq notations | Meaning | *)
(* |-------------------------------------|----------------------------------| *)
(* | set0 | $\emptyset$ | *)
(* | [set: A] | the full set of elements | *)
(* | | of type A | *)
(* | `` `\|` `` | $\cup$ | *)
(* | `` `&` `` | $\cap$ | *)
(* | `` `\` `` | set difference | *)
(* | `` ~` `` | set complement | *)
(* | `` `<=` `` | $\subseteq$ | *)
(* | `` f @` A `` | image by f of A | *)
(* | `` f @^-1` A `` | preimage by f of A | *)
(* | [set x] | The singleton set $\{x\}$ | *)
(* | [set~ x] | The complement of $\{x\}$ | *)
(* | [set E \| x in P] | the set of E with x ranging in P | *)
(* | range f | image by f of the full set | *)
(* | \big[setU/set0]_(i <- s \| P i) f i | finite union | *)
(* | \bigcup_(k in P) F k | countable union | *)
(* | \bigcap_(k in P) F k | countable intersection | *)
(* | trivIset D F | F is a sequence of pairwise | *)
(* | | disjoint sets indexed over | *)
(* | | the domain D | *)
(* *)
(* * Sets: *)
(* ## Sets *)
(* ``` *)
(* set T == type of sets on T. *)
(* (x \in P) == boolean membership predicate from ssrbool *)
(* for set P, available thanks to a canonical *)
Expand Down Expand Up @@ -86,8 +129,10 @@ From mathcomp Require Import mathcomp_extra boolp.
(* if there is one, to f0 x otherwise. *)
(* F `#` G <-> intersections beween elements of F an G are *)
(* all non empty. *)
(* ``` *)
(* *)
(* * Pointed types: *)
(* ## Pointed types *)
(* ``` *)
(* pointedType == interface type for types equipped with a *)
(* canonical inhabitant. *)
(* PointedType T m == packs the term m : T to build a *)
Expand All @@ -99,20 +144,19 @@ From mathcomp Require Import mathcomp_extra boolp.
(* point == canonical inhabitant of a pointedType. *)
(* get P == point x in P if it exists, point otherwise; *)
(* P must be a set on a pointedType. *)
(* ``` *)
(* *)
(* --> Thanks to this basic set theory, we proved Zorn's Lemma, which states *)
(* that any ordered set such that every totally ordered subset admits an *)
(* upper bound has a maximal element. We also proved an analogous version *)
(* for preorders, where maximal is replaced with premaximal: t is *)
(* premaximal if whenever t < s we also have s < t. *)
(* *)
(* ``` *)
(* $| T | == T : Type is inhabited *)
(* squash x == proof of $| T | (with x : T) *)
(* unsquash s == extract a witness from s : $| T | *)
(* --> Tactic: *)
(* ``` *)
(* *)
(* ## Tactic *)
(* - squash x: *)
(* solves a goal $| T | by instantiating with x or [the T of x] *)
(* *)
(* ``` *)
(* trivIset D F == the sets F i, where i ranges over D : set I,*)
(* are pairwise-disjoint *)
(* cover D F := \bigcup_(i in D) F i *)
Expand All @@ -124,12 +168,17 @@ From mathcomp Require Import mathcomp_extra boolp.
(* maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) *)
(* disjoint subcollection of the collection *)
(* B of elements in F : I -> set T *)
(* ``` *)
(* *)
(* * Upper and lower bounds: *)
(* ## Upper and lower bounds *)
(* ``` *)
(* ubound A == the set of upper bounds of the set A *)
(* lbound A == the set of lower bounds of the set A *)
(* ``` *)
(* *)
(* Predicates to express existence conditions of supremum and infimum of *)
(* sets of real numbers: *)
(* ``` *)
(* has_ubound A := ubound A != set0 *)
(* has_sup A := A != set0 /\ has_ubound A *)
(* has_lbound A := lbound A != set0 *)
Expand All @@ -142,26 +191,18 @@ From mathcomp Require Import mathcomp_extra boolp.
(* infimum x0 A == infimum of A or x0 if A is empty *)
(* *)
(* F `#` G := the classes of sets F and G intersect *)
(* ``` *)
(* *)
(* * sections: *)
(* ## Sections *)
(* xsection A x == with A : set (T1 * T2) and x : T1 is the *)
(* x-section of A *)
(* ysection A y == with A : set (T1 * T2) and y : T2 is the *)
(* y-section of A *)
(* *)
(* * About the naming conventions in this file: *)
(* - use T, T', T1, T2, etc., aT (domain type), rT (return type) for names of *)
(* variables in Type (or choiceType/pointedType/porderType) *)
(* + use the same suffix or prefix for the sets as their containing type *)
(* (e.g., A1 in T1, etc.) *)
(* + as a consequence functions are rather of type aT -> rT *)
(* - use I, J when the type corresponds to an index *)
(* - sets are named A, B, C, D, etc., or Y when it is ostensibly an image set *)
(* (i.e., of type set rT) *)
(* - indexed sets are rather named F *)
(* *)
(* * Composition of relations: *)
(* ## Composition of relations *)
(* ``` *)
(* A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)] *)
(* ``` *)
(* *)
(******************************************************************************)

Expand Down
Loading

0 comments on commit 2fc1a66

Please sign in to comment.