Add proofs on truth value #2418
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mildsunrise
force-pushed
the
dec-properties
branch
from
03492f0 to
0ab729a
Compare
gallais
reviewed
Jun 24, 2024
MatthewDaggitt
approved these changes
Jun 25, 2024
gallais
approved these changes
Jun 25, 2024
|
(I've simplified the proofs, but the statements remain unchanged) |
jamesmckinna
reviewed
Jul 1, 2024
jamesmckinna
reviewed
Jul 1, 2024
JacquesCarette
requested changes
Jul 4, 2024
mildsunrise
force-pushed
the
dec-properties
branch
from
611898d to
1785813
Compare
Adds a handful of properties that prove the truth
value of a decidable:
- `Relation.Nullary.Decidable`:
- `does-≡`: decidables over the same type have the same truth value
- `does-⇔`: generalization of `does-≡` to mutually implied types
- `Relation.Unary.Properties`:
- `≐?`: generalization of `Decidable.map` to predicates
(if two predicates are equivalent, one is decidable if the other is)
- `does-≡`: generalization of `does-≡` to predicates
- `does-≐`: generalization of `does-⇔` to predicates
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
mildsunrise
force-pushed
the
dec-properties
branch
from
1785813 to
f4b88e3
Compare
|
@JacquesCarette are you willing to approve now? |
JacquesCarette
approved these changes
Aug 14, 2024
jamesmckinna
reviewed
Sep 3, 2024
| does-≡ : (a? b? : Dec A) → does a? ≡ does b? | ||
| ``` | ||
|
|
||
| * In `Relation.Nullary.Properties`: |
There was a problem hiding this comment.
We missed this (copy/paste error?) during review: should be Relation.Unary.Properties!
There was a problem hiding this comment.
Nice spot! Any chance of a quick PR?
jamesmckinna
added a commit
to jamesmckinna/agda-stdlib
that referenced
this pull request
Sep 5, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adds a handful of "congruence" proofs on the truth value of a decidable, and also
≐?:Relation.Nullary.Decidable:does-≡: decidables over the same type have the same truth valuedoes-⇔: generalization ofdoes-≡to mutually implied typesRelation.Unary.Properties:≐?: generalization ofDecidable.mapto predicates (if two predicates are equivalent, one is decidable if the other is)does-≡: generalization ofdoes-≡to predicatesdoes-≐: generalization ofdoes-⇔to predicatesUsing these, together with the definitions in
Decidable.Core, one can prove the effect of type operations on truth value. For example, proving thatDec (¬ A)andDec Ahave negated truth values can be done asdoes-≡ ¬a? (¬? a?). Same with×/∧and⊎/∨.