From 796c806bdf64490e6ef04df7e2c01e7aa94ccb86 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:46:25 -0400 Subject: add sigma type proof irrelevance wisdom from ssreflect --- folkwisdom.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'folkwisdom.md') 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 -- cgit v1.2.3