diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:46:25 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:46:25 -0400 |
commit | 796c806bdf64490e6ef04df7e2c01e7aa94ccb86 (patch) | |
tree | 683b005b762ba4287b16fc0c4e8799c73c58012c | |
parent | 3c36b589a01bce19063872544bca132f3daf947d (diff) |
add sigma type proof irrelevance wisdom from ssreflect
-rw-r--r-- | folkwisdom.md | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index c6190a460..c53ad5160 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -100,10 +100,13 @@ Leibniz equality, showing that two points with equal coordinates are equal requires showing that the invariant preservation proofs are equal. This can be done using the `UIP_dec` lemma if the invariant itself is an equality and that for all values of coordinates it is decidable to compute whether the invariant -holds on them or or not. These conditions tend to be met for the invariants this -project uses. Otherwise, two points can be defined to be equivalent (not equal) -if they have the same coordinates (working with custom equivalence relations -involves nontrivial considerations of its own). +holds on them or or not. A principled way of representing an invariant `P : T -> +Prop` as an equality is to define `check_P : T -> bool` s.t. `check_P x = true +<-> P x` and use `{x | is_true (check_P x) }` as the type of valid values^[This +technique is used extensively in `ssreflect`.]. Alternatively, two points can be +defined to be equivalent (not equal) if they have the same coordinates (working +with custom equivalence relations involves nontrivial considerations of its +own). #### Note on defining values |