Skip to content

Commit

Permalink
Add contra tactics
Browse files Browse the repository at this point in the history
  • Loading branch information
Quentin Vermande authored and proux01 committed Jan 18, 2024
1 parent 8e4ae6d commit 501f221
Show file tree
Hide file tree
Showing 5 changed files with 900 additions and 0 deletions.
14 changes: 14 additions & 0 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,20 @@
- in `lebesgue_integral.v`:
+ `sigma_finite_measure` instance on product measure `\x`

- file `contra.v`
- in `contra.v`
+ lemma `assume_not`
+ tactic `assume_not`
+ lemma `absurd_not`
+ tactics `absurd_not`, `contrapose`
+ tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`,
`contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`,
`contra : { - } constr(H)`
+ lemma `absurd`
+ tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`,
`absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
`absurd : { hyp_list(Hs) } ident(H)`

- in `topology.v`:
+ lemma `filter_bigI_within`
+ lemma `near_powerset_map`
Expand Down
1 change: 1 addition & 0 deletions _CoqProject
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

classical/all_classical.v
classical/boolp.v
classical/contra.v
classical/classical_sets.v
classical/mathcomp_extra.v
classical/functions.v
Expand Down
1 change: 1 addition & 0 deletions classical/Make
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
-arg -w -arg -projection-no-head-constant

boolp.v
contra.v
classical_sets.v
mathcomp_extra.v
functions.v
Expand Down
1 change: 1 addition & 0 deletions classical/all_classical.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
From mathcomp Require Export boolp.
From mathcomp Require Export contra.
From mathcomp Require Export classical_sets.
From mathcomp Require Export mathcomp_extra.
From mathcomp Require Export functions.
Expand Down
Loading

0 comments on commit 501f221

Please sign in to comment.